some support for hyperlinks between different buffers;
authorwenzelm
Tue Aug 30 15:43:27 2011 +0200 (2011-08-30 ago)
changeset 445803bc9a215a56d
parent 44579 a9cf2380377d
child 44581 7daef43592d0
some support for hyperlinks between different buffers;
tuned signature;
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/isabelle_hyperlinks.scala
src/Tools/jEdit/src/jedit_thy_load.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 30 12:24:55 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 30 15:43:27 2011 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4      val version: Version
     1.5      val node: Node
     1.6      val is_outdated: Boolean
     1.7 -    def lookup_command(id: Command_ID): Option[Command]
     1.8 +    def find_command(id: Command_ID): Option[(String, Node, Command)]
     1.9      def state(command: Command): Command.State
    1.10      def convert(i: Text.Offset): Text.Offset
    1.11      def convert(range: Text.Range): Text.Range
    1.12 @@ -370,7 +370,13 @@
    1.13          val node = version.nodes(name)
    1.14          val is_outdated = !(pending_edits.isEmpty && latest == stable)
    1.15  
    1.16 -        def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
    1.17 +        def find_command(id: Command_ID): Option[(String, Node, Command)] =
    1.18 +          State.this.lookup_command(id) match {
    1.19 +            case None => None
    1.20 +            case Some(command) =>
    1.21 +              version.nodes.find({ case (_, node) => node.commands(command) })
    1.22 +                .map({ case (name, node) => (name, node, command) })
    1.23 +          }
    1.24  
    1.25          def state(command: Command): Command.State =
    1.26            try {
     2.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Tue Aug 30 12:24:55 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Tue Aug 30 15:43:27 2011 +0200
     2.3 @@ -16,11 +16,21 @@
     2.4  import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
     2.5  
     2.6  
     2.7 -private class Internal_Hyperlink(start: Int, end: Int, line: Int, def_offset: Int)
     2.8 +private class Internal_Hyperlink(name: String, start: Int, end: Int, line: Int, offset: Int)
     2.9    extends AbstractHyperlink(start, end, line, "")
    2.10  {
    2.11 -  override def click(view: View) {
    2.12 -    view.getTextArea.moveCaretPosition(def_offset)
    2.13 +  override def click(view: View)
    2.14 +  {
    2.15 +    val text_area = view.getTextArea
    2.16 +    if (Isabelle.buffer_name(view.getBuffer) == name)
    2.17 +      text_area.moveCaretPosition(offset)
    2.18 +    else
    2.19 +      Isabelle.jedit_buffer(name) match {
    2.20 +        case Some(buffer) =>
    2.21 +          view.setBuffer(buffer)
    2.22 +          text_area.moveCaretPosition(offset)
    2.23 +        case None =>
    2.24 +      }
    2.25    }
    2.26  }
    2.27  
    2.28 @@ -60,21 +70,22 @@
    2.29                  (Position.File.unapply(props), Position.Line.unapply(props)) match {
    2.30                    case (Some(def_file), Some(def_line)) =>
    2.31                      new External_Hyperlink(begin, end, line, def_file, def_line)
    2.32 -                  case _ =>
    2.33 +                  case _ if !snapshot.is_outdated =>
    2.34                      (props, props) match {
    2.35                        case (Position.Id(def_id), Position.Offset(def_offset)) =>
    2.36 -                        snapshot.lookup_command(def_id) match {
    2.37 -                          case Some(def_cmd) =>
    2.38 -                            snapshot.node.command_start(def_cmd) match {
    2.39 +                        snapshot.find_command(def_id) match {
    2.40 +                          case Some((def_name, def_node, def_cmd)) =>
    2.41 +                            def_node.command_start(def_cmd) match {
    2.42                                case Some(def_cmd_start) =>
    2.43 -                                new Internal_Hyperlink(begin, end, line,
    2.44 -                                  snapshot.convert(def_cmd_start + def_cmd.decode(def_offset)))
    2.45 +                                new Internal_Hyperlink(def_name, begin, end, line,
    2.46 +                                  def_cmd_start + def_cmd.decode(def_offset))
    2.47                                case None => null
    2.48                              }
    2.49                            case None => null
    2.50                          }
    2.51                        case _ => null
    2.52                      }
    2.53 +                  case _ => null
    2.54                  }
    2.55              }
    2.56            markup match {
     3.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Aug 30 12:24:55 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Aug 30 15:43:27 2011 +0200
     3.3 @@ -49,7 +49,7 @@
     3.4    override def check_thy(node_name: String): Thy_Header =
     3.5    {
     3.6      Swing_Thread.now {
     3.7 -      Isabelle.jedit_buffers().find(buffer => Isabelle.buffer_name(buffer) == node_name) match {
     3.8 +      Isabelle.jedit_buffer(node_name) match {
     3.9          case Some(buffer) =>
    3.10            Isabelle.buffer_lock(buffer) {
    3.11              val text = new Segment
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 30 12:24:55 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 30 15:43:27 2011 +0200
     4.3 @@ -159,10 +159,27 @@
     4.4    }
     4.5  
     4.6  
     4.7 +  /* buffers */
     4.8 +
     4.9 +  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    4.10 +    Swing_Thread.now { buffer_lock(buffer) { body } }
    4.11 +
    4.12 +  def buffer_text(buffer: JEditBuffer): String =
    4.13 +    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    4.14 +
    4.15 +  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    4.16 +
    4.17 +  def buffer_path(buffer: Buffer): (String, String) =
    4.18 +    (buffer.getDirectory, buffer_name(buffer))
    4.19 +
    4.20 +
    4.21    /* main jEdit components */
    4.22  
    4.23    def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
    4.24  
    4.25 +  def jedit_buffer(name: String): Option[Buffer] =
    4.26 +    jedit_buffers().find(buffer => buffer_name(buffer) == name)
    4.27 +
    4.28    def jedit_views(): Iterator[View] = jEdit.getViews().iterator
    4.29  
    4.30    def jedit_text_areas(view: View): Iterator[JEditTextArea] =
    4.31 @@ -180,17 +197,6 @@
    4.32      finally { buffer.readUnlock() }
    4.33    }
    4.34  
    4.35 -  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    4.36 -    Swing_Thread.now { buffer_lock(buffer) { body } }
    4.37 -
    4.38 -  def buffer_text(buffer: JEditBuffer): String =
    4.39 -    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    4.40 -
    4.41 -  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    4.42 -
    4.43 -  def buffer_path(buffer: Buffer): (String, String) =
    4.44 -    (buffer.getDirectory, buffer_name(buffer))
    4.45 -
    4.46  
    4.47    /* document model and view */
    4.48