1.1 --- a/src/Tools/jEdit/plugin/Isabelle.props	Fri May 22 13:43:35 2009 +0200
     1.2 +++ b/src/Tools/jEdit/plugin/Isabelle.props	Fri May 22 14:47:57 2009 +0200
     1.3 @@ -50,3 +50,6 @@
     1.4  sidekick.parser.isabelle.label=Isabelle
     1.5  mode.isabelle.sidekick.parser=isabelle
     1.6  mode.ml.sidekick.parser=isabelle
     1.7 +
     1.8 +#Hyperlinks
     1.9 +mode.isabelle.hyperlink.source=isabelle

     2.1 --- a/src/Tools/jEdit/plugin/services.xml	Fri May 22 13:43:35 2009 +0200
     2.2 +++ b/src/Tools/jEdit/plugin/services.xml	Fri May 22 14:47:57 2009 +0200
     2.3 @@ -7,4 +7,7 @@
     2.4  	<SERVICE NAME="isabelle" CLASS="org.gjt.sp.jedit.io.VFS">
     2.5  		new isabelle.jedit.VFS();
     2.6  	</SERVICE>
     2.7 +  <SERVICE NAME="isabelle" CLASS="gatchan.jedit.hyperlinks.HyperlinkSource">
     2.8 +    new isabelle.jedit.IsabelleHyperlinkSource();
     2.9 +  </SERVICE>
    2.10  </SERVICES>

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Fri May 22 14:47:57 2009 +0200
     3.3 @@ -0,0 +1,64 @@
     3.4 +/*
     3.5 + * IsabelleHyperlinkSource.scala
     3.6 + *
     3.7 + * To change this template, choose Tools | Template Manager
     3.8 + * and open the template in the editor.
     3.9 + */
    3.10 +
    3.11 +package isabelle.jedit
    3.12 +import gatchan.jedit.hyperlinks.Hyperlink
    3.13 +import gatchan.jedit.hyperlinks.HyperlinkSource
    3.14 +import gatchan.jedit.hyperlinks.AbstractHyperlink
    3.15 +
    3.16 +import org.gjt.sp.jedit.View
    3.17 +import org.gjt.sp.jedit.jEdit
    3.18 +import org.gjt.sp.jedit.Buffer
    3.19 +import org.gjt.sp.jedit.TextUtilities
    3.20 +
    3.21 +import isabelle.prover.RefInfo
    3.22 +
    3.23 +class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
    3.24 +  extends AbstractHyperlink(start, end, line, "tooltip")
    3.25 +{
    3.26 +  override def click(view: View) = {
    3.27 +    view.getTextArea.moveCaretPosition(ref_offset)
    3.28 +  }
    3.29 +}
    3.30 +
    3.31 +class IsabelleHyperlinkSource extends HyperlinkSource
    3.32 +{
    3.33 +	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = {
    3.34 +    val prover = Isabelle.prover_setup(buffer).map(_.prover)
    3.35 +    val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)
    3.36 +    if (!prover.isDefined || !theory_view_opt.isDefined) null
    3.37 +    else if (prover.get == null || theory_view_opt.get == null) null
    3.38 +    else {
    3.39 +      val document = prover.get.document
    3.40 +      val theory_view = theory_view_opt.get
    3.41 +      val offset = theory_view.from_current(document, original_offset)
    3.42 +      val cmd = document.find_command_at(offset)
    3.43 +      if (cmd != null) {
    3.44 +        val ref_o = cmd.ref_at(offset - cmd.start(document))
    3.45 +        if (!ref_o.isDefined) null
    3.46 +        else {
    3.47 +          val ref = ref_o.get
    3.48 +          val start = theory_view.to_current(document, ref.abs_start(document))
    3.49 +          val line = buffer.getLineOfOffset(start)
    3.50 +          val end = theory_view.to_current(document, ref.abs_stop(document))
    3.51 +          ref.info match {
    3.52 +            case RefInfo(Some(file), Some(ref_line), _, _) =>
    3.53 +              null
    3.54 +            case RefInfo(_, _, Some(id), Some(offset)) =>
    3.55 +              prover.get.command(id) match {
    3.56 +                case Some(ref_cmd) =>
    3.57 +                  new InternalHyperlink(start, end, line,
    3.58 +                    theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
    3.59 +                case _ => null
    3.60 +              }
    3.61 +            case _ => null
    3.62 +          }
    3.63 +        }
    3.64 +      } else null
    3.65 +    }
    3.66 +  }
    3.67 +}

     4.1 --- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri May 22 13:43:35 2009 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri May 22 14:47:57 2009 +0200
     4.3 @@ -135,6 +135,10 @@
     4.4      _to_current(from_id, if (col == null) changes else col :: changes, pos)
     4.5    def from_current(to_id: String, pos : Int) =
     4.6      _from_current(to_id, if (col == null) changes else col :: changes, pos)
     4.7 +  def to_current(document: isabelle.proofdocument.ProofDocument, pos: Int): Int =
     4.8 +    to_current(document.id, pos)
     4.9 +  def from_current(document: isabelle.proofdocument.ProofDocument, pos: Int): Int =
    4.10 +    from_current(document.id, pos)
    4.11  
    4.12    def repaint(cmd: Command) =
    4.13    {

     5.1 --- a/src/Tools/jEdit/src/prover/Command.scala	Fri May 22 13:43:35 2009 +0200
     5.2 +++ b/src/Tools/jEdit/src/prover/Command.scala	Fri May 22 14:47:57 2009 +0200
     5.3 @@ -106,4 +106,9 @@
     5.4        map(t => "\"" + t.content + "\" : " + (t.info match {case TypeInfo(i) => i case _ => ""})).
     5.5        getOrElse(null)
     5.6    }
     5.7 +
     5.8 +  def ref_at(pos: Int): Option[MarkupNode] =
     5.9 +    markup_root.filter(_.info match {case RefInfo(_,_,_,_) => true case _ => false}).
    5.10 +      flatten(_.flatten).
    5.11 +      find(t => t.start <= pos && t.stop > pos)
    5.12  }

     6.1 --- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 13:43:35 2009 +0200
     6.2 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 14:47:57 2009 +0200
     6.3 @@ -18,7 +18,10 @@
     6.4  case class OuterInfo(highlight: String) extends MarkupInfo {override def toString = highlight}
     6.5  case class HighlightInfo(highlight: String) extends MarkupInfo {override def toString = highlight}
     6.6  case class TypeInfo(type_kind: String) extends MarkupInfo {override def toString = type_kind}
     6.7 -case class RefInfo(info: Any) extends MarkupInfo {override def toString = info.toString}
     6.8 +case class RefInfo(file: Option[String], line: Option[Int],
     6.9 +                   command_id: Option[String], offset: Option[Int]) extends MarkupInfo {
    6.10 +  override def toString = (file, line, command_id, offset).toString
    6.11 +}
    6.12  
    6.13  object MarkupNode {
    6.14  
    6.15 @@ -46,7 +49,7 @@
    6.16  
    6.17  class MarkupNode (val base: Command, val start: Int, val stop: Int,
    6.18                    val children: List[MarkupNode],
    6.19 -                  val id: String, val content: String, val info: Any) {
    6.20 +                  val id: String, val content: String, val info: MarkupInfo) {
    6.21  
    6.22    def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = {
    6.23      val node = MarkupNode.markup2default_node (this, base, doc)

     7.1 --- a/src/Tools/jEdit/src/prover/Prover.scala	Fri May 22 13:43:35 2009 +0200
     7.2 +++ b/src/Tools/jEdit/src/prover/Prover.scala	Fri May 22 14:47:57 2009 +0200
     7.3 @@ -51,6 +51,7 @@
     7.4    private var document_versions = List(ProofDocument.empty)
     7.5    private val document_id0 = ProofDocument.empty.id
     7.6  
     7.7 +  def command(id: IsarDocument.Command_ID): Option[Command] = commands.get(id)
     7.8    def document = document_versions.head
     7.9  
    7.10    private var initialized = false
    7.11 @@ -190,7 +191,15 @@
    7.12                          val info = body.first.asInstanceOf[XML.Text].content
    7.13                          command.markup_root += command.markup_node(begin, end, TypeInfo(info))
    7.14                        case Markup.ML_REF =>
    7.15 -                        command.markup_root += command.markup_node(begin, end, RefInfo(body))
    7.16 +                        body match {
    7.17 +                          case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
    7.18 +                            command.markup_root += command.markup_node(begin, end,
    7.19 +                              RefInfo(get_attr(attr, Markup.FILE),
    7.20 +                                      get_attr(attr, Markup.LINE).map(Integer.parseInt),
    7.21 +                                      get_attr(attr, Markup.ID),
    7.22 +                                      get_attr(attr, Markup.OFFSET).map(Integer.parseInt)))
    7.23 +                          case _ =>
    7.24 +                        }
    7.25                        case kind =>
    7.26                          if (!running)
    7.27                            commands.get(markup_id).map (cmd =>