wneuper/isa: src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala@15abc5f5f40a

     1 /*

     2  * IsabelleHyperlinkSource.scala

     3  *

     4  * To change this template, choose Tools | Template Manager

     5  * and open the template in the editor.

     6  */

     8 package isabelle.jedit

    10 import java.io.File

    12 import gatchan.jedit.hyperlinks.Hyperlink

    13 import gatchan.jedit.hyperlinks.HyperlinkSource

    14 import gatchan.jedit.hyperlinks.AbstractHyperlink

    16 import org.gjt.sp.jedit.View

    17 import org.gjt.sp.jedit.jEdit

    18 import org.gjt.sp.jedit.Buffer

    19 import org.gjt.sp.jedit.TextUtilities

    21 import isabelle.prover.RefInfo

    23 class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)

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

    25 {

    26   override def click(view: View) = {

    27     view.getTextArea.moveCaretPosition(ref_offset)

    28   }

    29 }

    31 class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)

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

    33 {

    34   val srcs = List(new File(Isabelle.system.getenv("ISABELLE_HOME"), "src"),

    35                   new File(Isabelle.system.getenv("ML_SOURCES")))

    37   def find_file(file: File, filename: String): Option[File] =

    38   {

    39     if (file.getName == new File(filename).getName) Some(file)

    40     else if (file.isDirectory) file.listFiles.map(find_file(_, filename)).find(_.isDefined).getOrElse(None)

    41     else None

    42   }

    44   override def click(view: View) = {

    45     srcs.find(src =>

    46       find_file(src, ref_file) match {

    47         case None => false

    48         case Some(file) =>

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

    50           true})

    51       match {

    52         case None => System.err.println("Could not find file " + ref_file)

    53         case _ =>

    54       }

    55   }

    56 }

    58 class IsabelleHyperlinkSource extends HyperlinkSource

    59 {

    60 	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = {

    61     val prover = Isabelle.prover_setup(buffer).map(_.prover)

    62     val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)

    63     if (!prover.isDefined || !theory_view_opt.isDefined) null

    64     else if (prover.get == null || theory_view_opt.get == null) null

    65     else {

    66       val document = prover.get.document

    67       val theory_view = theory_view_opt.get

    68       val offset = theory_view.from_current(document, original_offset)

    69       val cmd = document.find_command_at(offset)

    70       if (cmd != null) {

    71         val ref_o = cmd.ref_at(offset - cmd.start(document))

    72         if (!ref_o.isDefined) null

    73         else {

    74           val ref = ref_o.get

    75           val start = theory_view.to_current(document, ref.abs_start(document))

    76           val line = buffer.getLineOfOffset(start)

    77           val end = theory_view.to_current(document, ref.abs_stop(document))

    78           ref.info match {

    79             case RefInfo(Some(ref_file), Some(ref_line), _, _) =>

    80               new ExternalHyperlink(start, end, line, ref_file, ref_line)

    81             case RefInfo(_, _, Some(id), Some(offset)) =>

    82               prover.get.command(id) match {

    83                 case Some(ref_cmd) =>

    84                   new InternalHyperlink(start, end, line,

    85                     theory_view.to_current(document, ref_cmd.start(document) + offset - 1))

    86                 case _ => null

    87               }

    88             case _ => null

    89           }

    90         }

    91       } else null

    92     }

    93   }

    94 }

author	immler@in.tum.de
	Fri, 22 May 2009 16:47:11 +0200
changeset 34572	15abc5f5f40a
parent 34571	b517d0607297
child 34576	daa397b6401c
permissions	-rw-r--r--