/*  Title:      Tools/jEdit/src/isabelle_hyperlinks.scala

    Author:     Fabian Immler, TU Munich

Hyperlink setup for Isabelle proof documents.

*/

package isabelle.jedit

import isabelle._

import java.io.{File => JFile}

import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}

import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}

private class Internal_Hyperlink(name: String, start: Int, end: Int, line: Int, offset: Int)

  extends AbstractHyperlink(start, end, line, "")

{

  override def click(view: View)

  {

    val text_area = view.getTextArea

    if (Isabelle.buffer_name(view.getBuffer) == name)

      text_area.moveCaretPosition(offset)

    else

      Isabelle.jedit_buffer(name) match {

        case Some(buffer) =>

          view.setBuffer(buffer)

          text_area.moveCaretPosition(offset)

        case None =>

      }

  }

}

class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int)

  extends AbstractHyperlink(start, end, line, "")

{

  override def click(view: View) = {

    Isabelle_System.source_file(Path.explode(def_file)) match {

      case None =>

        Library.error_dialog(view, "File not found",

          Library.scrollable_text("Could not find source file " + def_file))

      case Some(file) =>

        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))

    }

  }

}

class Isabelle_Hyperlinks extends HyperlinkSource

{

  def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =

  {

    Swing_Thread.assert()

    Isabelle.buffer_lock(buffer) {

      Document_Model(buffer) match {

        case Some(model) =>

          val snapshot = model.snapshot()

          val markup =

            snapshot.select_markup[Hyperlink](

              Text.Range(buffer_offset, buffer_offset + 1),

              Some(Set(Isabelle_Markup.ENTITY)),

              {

                // FIXME Isabelle_Rendering.hyperlink

                case Text.Info(info_range,

                    XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))

                  if (props.find(

                    { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true

                      case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true

                      case _ => false }).isEmpty) =>

                  val Text.Range(begin, end) = info_range

                  val line = buffer.getLineOfOffset(begin)

                  (Position.File.unapply(props), Position.Line.unapply(props)) match {

                    case (Some(def_file), def_line) =>

                      new External_Hyperlink(begin, end, line, def_file, def_line.getOrElse(1))

                    case _ if !snapshot.is_outdated =>

                      (props, props) match {

                        case (Position.Id(def_id), Position.Offset(def_offset)) =>

                          snapshot.state.find_command(snapshot.version, def_id) match {

                            case Some((def_node, def_cmd)) =>

                              def_node.command_start(def_cmd) match {

                                case Some(def_cmd_start) =>

                                  new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,

                                    def_cmd_start + def_cmd.decode(def_offset))

                                case None => null

                              }

                            case None => null

                          }

                        case _ => null

                      }

                    case _ => null

                  }

              })

          markup match {

            case Text.Info(_, link) #:: _ => link

            case _ => null

          }

        case None => null

      }

    }

  }

}