src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34777 91d6089cef88
     1.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Dec 08 14:49:01 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Dec 08 16:30:20 2009 +0100
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  package isabelle.jedit
     1.6  
     1.7 +
     1.8  import java.io.File
     1.9  
    1.10  import gatchan.jedit.hyperlinks.Hyperlink
    1.11 @@ -17,10 +18,10 @@
    1.12  import org.gjt.sp.jedit.Buffer
    1.13  import org.gjt.sp.jedit.TextUtilities
    1.14  
    1.15 -import isabelle.prover.Command
    1.16 +import isabelle.proofdocument.Command
    1.17  
    1.18  
    1.19 -class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
    1.20 +private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
    1.21    extends AbstractHyperlink(start, end, line, "")
    1.22  {
    1.23    override def click(view: View) {
    1.24 @@ -28,21 +29,22 @@
    1.25    }
    1.26  }
    1.27  
    1.28 -class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
    1.29 +class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
    1.30    extends AbstractHyperlink(start, end, line, "")
    1.31  {
    1.32    override def click(view: View) = {
    1.33      Isabelle.system.source_file(ref_file) match {
    1.34 -      case None => System.err.println("Could not find source file " + ref_file)
    1.35 +      case None => System.err.println("Could not find source file " + ref_file)  // FIXME ??
    1.36        case Some(file) =>
    1.37          jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
    1.38      }
    1.39    }
    1.40  }
    1.41  
    1.42 -class IsabelleHyperlinkSource extends HyperlinkSource
    1.43 +class Isabelle_Hyperlinks extends HyperlinkSource
    1.44  {
    1.45 -	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = {
    1.46 +	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
    1.47 +	{
    1.48      val prover = Isabelle.prover_setup(buffer).map(_.prover)
    1.49      val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)
    1.50      if (prover.isEmpty || theory_view_opt.isEmpty) null
    1.51 @@ -61,11 +63,11 @@
    1.52                val end = theory_view.to_current(document, command_start + ref.stop)
    1.53                ref.info match {
    1.54                  case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
    1.55 -                  new ExternalHyperlink(begin, end, line, ref_file, ref_line)
    1.56 +                  new External_Hyperlink(begin, end, line, ref_file, ref_line)
    1.57                  case Command.RefInfo(_, _, Some(id), Some(offset)) =>
    1.58                    prover.get.command(id) match {
    1.59                      case Some(ref_cmd) =>
    1.60 -                      new InternalHyperlink(begin, end, line,
    1.61 +                      new Internal_Hyperlink(begin, end, line,
    1.62                          theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
    1.63                      case None => null
    1.64                    }