# HG changeset patch
# User immler@in.tum.de
# Date 1242996477 -7200
# Node ID b517d06072977b7820625243f395d13ef1e9e50e
# Parent  d9e4b940cf7efcdb64eed36092da82953a4e095b
implemented IsabelleHyperlinkSource (only links inside the current buffer)

diff -r d9e4b940cf7e -r b517d0607297 src/Tools/jEdit/plugin/Isabelle.props
--- a/src/Tools/jEdit/plugin/Isabelle.props	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Fri May 22 14:47:57 2009 +0200
@@ -50,3 +50,6 @@
 sidekick.parser.isabelle.label=Isabelle
 mode.isabelle.sidekick.parser=isabelle
 mode.ml.sidekick.parser=isabelle
+
+#Hyperlinks
+mode.isabelle.hyperlink.source=isabelle
diff -r d9e4b940cf7e -r b517d0607297 src/Tools/jEdit/plugin/services.xml
--- a/src/Tools/jEdit/plugin/services.xml	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/plugin/services.xml	Fri May 22 14:47:57 2009 +0200
@@ -7,4 +7,7 @@
 	<SERVICE NAME="isabelle" CLASS="org.gjt.sp.jedit.io.VFS">
 		new isabelle.jedit.VFS();
 	</SERVICE>
+  <SERVICE NAME="isabelle" CLASS="gatchan.jedit.hyperlinks.HyperlinkSource">
+    new isabelle.jedit.IsabelleHyperlinkSource();
+  </SERVICE>
 </SERVICES>
diff -r d9e4b940cf7e -r b517d0607297 src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Fri May 22 14:47:57 2009 +0200
@@ -0,0 +1,64 @@
+/*
+ * IsabelleHyperlinkSource.scala
+ *
+ * To change this template, choose Tools | Template Manager
+ * and open the template in the editor.
+ */
+
+package isabelle.jedit
+import gatchan.jedit.hyperlinks.Hyperlink
+import gatchan.jedit.hyperlinks.HyperlinkSource
+import gatchan.jedit.hyperlinks.AbstractHyperlink
+
+import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.jEdit
+import org.gjt.sp.jedit.Buffer
+import org.gjt.sp.jedit.TextUtilities
+
+import isabelle.prover.RefInfo
+
+class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
+  extends AbstractHyperlink(start, end, line, "tooltip")
+{
+  override def click(view: View) = {
+    view.getTextArea.moveCaretPosition(ref_offset)
+  }
+}
+
+class IsabelleHyperlinkSource extends HyperlinkSource
+{
+	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = {
+    val prover = Isabelle.prover_setup(buffer).map(_.prover)
+    val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)
+    if (!prover.isDefined || !theory_view_opt.isDefined) null
+    else if (prover.get == null || theory_view_opt.get == null) null
+    else {
+      val document = prover.get.document
+      val theory_view = theory_view_opt.get
+      val offset = theory_view.from_current(document, original_offset)
+      val cmd = document.find_command_at(offset)
+      if (cmd != null) {
+        val ref_o = cmd.ref_at(offset - cmd.start(document))
+        if (!ref_o.isDefined) null
+        else {
+          val ref = ref_o.get
+          val start = theory_view.to_current(document, ref.abs_start(document))
+          val line = buffer.getLineOfOffset(start)
+          val end = theory_view.to_current(document, ref.abs_stop(document))
+          ref.info match {
+            case RefInfo(Some(file), Some(ref_line), _, _) =>
+              null
+            case RefInfo(_, _, Some(id), Some(offset)) =>
+              prover.get.command(id) match {
+                case Some(ref_cmd) =>
+                  new InternalHyperlink(start, end, line,
+                    theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
+                case _ => null
+              }
+            case _ => null
+          }
+        }
+      } else null
+    }
+  }
+}
diff -r d9e4b940cf7e -r b517d0607297 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri May 22 14:47:57 2009 +0200
@@ -135,6 +135,10 @@
     _to_current(from_id, if (col == null) changes else col :: changes, pos)
   def from_current(to_id: String, pos : Int) =
     _from_current(to_id, if (col == null) changes else col :: changes, pos)
+  def to_current(document: isabelle.proofdocument.ProofDocument, pos: Int): Int =
+    to_current(document.id, pos)
+  def from_current(document: isabelle.proofdocument.ProofDocument, pos: Int): Int =
+    from_current(document.id, pos)
 
   def repaint(cmd: Command) =
   {
diff -r d9e4b940cf7e -r b517d0607297 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Fri May 22 14:47:57 2009 +0200
@@ -106,4 +106,9 @@
       map(t => "\"" + t.content + "\" : " + (t.info match {case TypeInfo(i) => i case _ => ""})).
       getOrElse(null)
   }
+
+  def ref_at(pos: Int): Option[MarkupNode] =
+    markup_root.filter(_.info match {case RefInfo(_,_,_,_) => true case _ => false}).
+      flatten(_.flatten).
+      find(t => t.start <= pos && t.stop > pos)
 }
diff -r d9e4b940cf7e -r b517d0607297 src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 14:47:57 2009 +0200
@@ -18,7 +18,10 @@
 case class OuterInfo(highlight: String) extends MarkupInfo {override def toString = highlight}
 case class HighlightInfo(highlight: String) extends MarkupInfo {override def toString = highlight}
 case class TypeInfo(type_kind: String) extends MarkupInfo {override def toString = type_kind}
-case class RefInfo(info: Any) extends MarkupInfo {override def toString = info.toString}
+case class RefInfo(file: Option[String], line: Option[Int],
+                   command_id: Option[String], offset: Option[Int]) extends MarkupInfo {
+  override def toString = (file, line, command_id, offset).toString
+}
 
 object MarkupNode {
 
@@ -46,7 +49,7 @@
 
 class MarkupNode (val base: Command, val start: Int, val stop: Int,
                   val children: List[MarkupNode],
-                  val id: String, val content: String, val info: Any) {
+                  val id: String, val content: String, val info: MarkupInfo) {
 
   def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = {
     val node = MarkupNode.markup2default_node (this, base, doc)
diff -r d9e4b940cf7e -r b517d0607297 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Fri May 22 14:47:57 2009 +0200
@@ -51,6 +51,7 @@
   private var document_versions = List(ProofDocument.empty)
   private val document_id0 = ProofDocument.empty.id
 
+  def command(id: IsarDocument.Command_ID): Option[Command] = commands.get(id)
   def document = document_versions.head
 
   private var initialized = false
@@ -190,7 +191,15 @@
                         val info = body.first.asInstanceOf[XML.Text].content
                         command.markup_root += command.markup_node(begin, end, TypeInfo(info))
                       case Markup.ML_REF =>
-                        command.markup_root += command.markup_node(begin, end, RefInfo(body))
+                        body match {
+                          case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
+                            command.markup_root += command.markup_node(begin, end,
+                              RefInfo(get_attr(attr, Markup.FILE),
+                                      get_attr(attr, Markup.LINE).map(Integer.parseInt),
+                                      get_attr(attr, Markup.ID),
+                                      get_attr(attr, Markup.OFFSET).map(Integer.parseInt)))
+                          case _ =>
+                        }
                       case kind =>
                         if (!running)
                           commands.get(markup_id).map (cmd =>