manage hyperlinks via PIDE editor interface;
authorwenzelm
Mon Aug 12 17:11:27 2013 +0200 (2013-08-12)
changeset 5298028f59ca8ce78
parent 52979 575be709c83e
child 52981 c7afd884dfb2
manage hyperlinks via PIDE editor interface;
src/Pure/PIDE/editor.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/documentation_dockable.scala
src/Tools/jEdit/src/hyperlink.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/query_operation.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
     1.1 --- a/src/Pure/PIDE/editor.scala	Mon Aug 12 15:09:13 2013 +0200
     1.2 +++ b/src/Pure/PIDE/editor.scala	Mon Aug 12 17:11:27 2013 +0200
     1.3 @@ -20,5 +20,10 @@
     1.4    def node_overlays(name: Document.Node.Name): Document.Node.Overlays
     1.5    def insert_overlay(command: Command, fn: String, args: List[String]): Unit
     1.6    def remove_overlay(command: Command, fn: String, args: List[String]): Unit
     1.7 +
     1.8 +  abstract class Hyperlink { def follow(context: Context): Unit }
     1.9 +  def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink
    1.10 +  def hyperlink_command(
    1.11 +    snapshot: Document.Snapshot, command: Command, offset: Text.Offset = 0): Option[Hyperlink]
    1.12  }
    1.13  
     2.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Mon Aug 12 15:09:13 2013 +0200
     2.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Aug 12 17:11:27 2013 +0200
     2.3 @@ -17,7 +17,6 @@
     2.4    "src/fold_handling.scala"
     2.5    "src/graphview_dockable.scala"
     2.6    "src/html_panel.scala"
     2.7 -  "src/hyperlink.scala"
     2.8    "src/info_dockable.scala"
     2.9    "src/isabelle.scala"
    2.10    "src/isabelle_encoding.scala"
     3.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Mon Aug 12 15:09:13 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Mon Aug 12 17:11:27 2013 +0200
     3.3 @@ -66,7 +66,7 @@
     3.4                          "Documentation error", GUI.scrollable_text(Exn.message(exn)))
     3.5                    })
     3.6                case Text_File(_, path) =>
     3.7 -                Hyperlink(Isabelle_System.platform_path(path)).follow(view)
     3.8 +                PIDE.editor.goto(view, Isabelle_System.platform_path(path))
     3.9                case _ =>
    3.10              }
    3.11            case _ =>
     4.1 --- a/src/Tools/jEdit/src/hyperlink.scala	Mon Aug 12 15:09:13 2013 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,58 +0,0 @@
     4.4 -/*  Title:      Tools/jEdit/src/hyperlink.scala
     4.5 -    Author:     Fabian Immler, TU Munich
     4.6 -    Author:     Makarius
     4.7 -
     4.8 -Hyperlinks within jEdit buffers for PIDE proof documents.
     4.9 -*/
    4.10 -
    4.11 -package isabelle.jedit
    4.12 -
    4.13 -
    4.14 -import isabelle._
    4.15 -
    4.16 -import org.gjt.sp.jedit.{View, jEdit}
    4.17 -import org.gjt.sp.jedit.textarea.JEditTextArea
    4.18 -
    4.19 -
    4.20 -object Hyperlink
    4.21 -{
    4.22 -  def apply(jedit_file: String, line: Int = 0, column: Int = 0): Hyperlink =
    4.23 -    File_Link(jedit_file, line, column)
    4.24 -}
    4.25 -
    4.26 -abstract class Hyperlink
    4.27 -{
    4.28 -  def follow(view: View): Unit
    4.29 -}
    4.30 -
    4.31 -private case class File_Link(jedit_file: String, line: Int, column: Int) extends Hyperlink
    4.32 -{
    4.33 -  override def follow(view: View)
    4.34 -  {
    4.35 -    Swing_Thread.require()
    4.36 -
    4.37 -    JEdit_Lib.jedit_buffer(jedit_file) match {
    4.38 -      case Some(buffer) =>
    4.39 -        view.goToBuffer(buffer)
    4.40 -        val text_area = view.getTextArea
    4.41 -
    4.42 -        try {
    4.43 -          val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
    4.44 -          text_area.moveCaretPosition(line_start)
    4.45 -          if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
    4.46 -        }
    4.47 -        catch {
    4.48 -          case _: ArrayIndexOutOfBoundsException =>
    4.49 -          case _: IllegalArgumentException =>
    4.50 -        }
    4.51 -
    4.52 -      case None =>
    4.53 -        val args =
    4.54 -          if (line <= 0) Array(jedit_file)
    4.55 -          else if (column <= 0) Array(jedit_file, "+line:" + line.toInt)
    4.56 -          else Array(jedit_file, "+line:" + line.toInt + "," + column.toInt)
    4.57 -        jEdit.openFiles(view, null, args)
    4.58 -    }
    4.59 -  }
    4.60 -}
    4.61 -
     5.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 15:09:13 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 17:11:27 2013 +0200
     5.3 @@ -17,9 +17,9 @@
     5.4  {
     5.5    /* session */
     5.6  
     5.7 -  def session: Session = PIDE.session
     5.8 +  override def session: Session = PIDE.session
     5.9  
    5.10 -  def flush()
    5.11 +  override def flush()
    5.12    {
    5.13      Swing_Thread.require()
    5.14  
    5.15 @@ -39,16 +39,16 @@
    5.16  
    5.17    /* current situation */
    5.18  
    5.19 -  def current_context: View =
    5.20 +  override def current_context: View =
    5.21      Swing_Thread.require { jEdit.getActiveView() }
    5.22  
    5.23 -  def current_node(view: View): Option[Document.Node.Name] =
    5.24 +  override def current_node(view: View): Option[Document.Node.Name] =
    5.25      Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
    5.26  
    5.27 -  def current_node_snapshot(view: View): Option[Document.Snapshot] =
    5.28 +  override def current_node_snapshot(view: View): Option[Document.Snapshot] =
    5.29      Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    5.30  
    5.31 -  def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    5.32 +  override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    5.33    {
    5.34      Swing_Thread.require()
    5.35  
    5.36 @@ -62,7 +62,8 @@
    5.37      }
    5.38    }
    5.39  
    5.40 -  def current_command(view: View, snapshot: Document.Snapshot): Option[(Command, Text.Offset)] =
    5.41 +  override def current_command(view: View, snapshot: Document.Snapshot)
    5.42 +    : Option[(Command, Text.Offset)] =
    5.43    {
    5.44      Swing_Thread.require()
    5.45  
    5.46 @@ -84,12 +85,65 @@
    5.47  
    5.48    private var overlays = Document.Overlays.empty
    5.49  
    5.50 -  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
    5.51 +  override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
    5.52      synchronized { overlays(name) }
    5.53  
    5.54 -  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
    5.55 +  override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
    5.56      synchronized { overlays = overlays.insert(command, fn, args) }
    5.57  
    5.58 -  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
    5.59 +  override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
    5.60      synchronized { overlays = overlays.remove(command, fn, args) }
    5.61 +
    5.62 +
    5.63 +  /* hyperlinks */
    5.64 +
    5.65 +  def goto(view: View, file_name: String, line: Int = 0, column: Int = 0)
    5.66 +  {
    5.67 +    Swing_Thread.require()
    5.68 +
    5.69 +    JEdit_Lib.jedit_buffer(file_name) match {
    5.70 +      case Some(buffer) =>
    5.71 +        view.goToBuffer(buffer)
    5.72 +        val text_area = view.getTextArea
    5.73 +
    5.74 +        try {
    5.75 +          val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
    5.76 +          text_area.moveCaretPosition(line_start)
    5.77 +          if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
    5.78 +        }
    5.79 +        catch {
    5.80 +          case _: ArrayIndexOutOfBoundsException =>
    5.81 +          case _: IllegalArgumentException =>
    5.82 +        }
    5.83 +
    5.84 +      case None =>
    5.85 +        val args =
    5.86 +          if (line <= 0) Array(file_name)
    5.87 +          else if (column <= 0) Array(file_name, "+line:" + line.toInt)
    5.88 +          else Array(file_name, "+line:" + line.toInt + "," + column.toInt)
    5.89 +        jEdit.openFiles(view, null, args)
    5.90 +    }
    5.91 +  }
    5.92 +
    5.93 +  override def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink =
    5.94 +    new Hyperlink { def follow(view: View) = goto(view, file_name, line, column) }
    5.95 +
    5.96 +  override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0)
    5.97 +    : Option[Hyperlink] =
    5.98 +  {
    5.99 +    if (snapshot.is_outdated) None
   5.100 +    else {
   5.101 +      snapshot.state.find_command(snapshot.version, command.id) match {
   5.102 +        case None => None
   5.103 +        case Some((node, _)) =>
   5.104 +          val file_name = command.node_name.node
   5.105 +          val sources =
   5.106 +            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
   5.107 +              (if (offset == 0) Iterator.empty
   5.108 +               else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
   5.109 +          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
   5.110 +          Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
   5.111 +      }
   5.112 +    }
   5.113 +  }
   5.114  }
     6.1 --- a/src/Tools/jEdit/src/query_operation.scala	Mon Aug 12 15:09:13 2013 +0200
     6.2 +++ b/src/Tools/jEdit/src/query_operation.scala	Mon Aug 12 17:11:27 2013 +0200
     6.3 @@ -12,8 +12,6 @@
     6.4  
     6.5  import scala.actors.Actor._
     6.6  
     6.7 -import org.gjt.sp.jedit.View
     6.8 -
     6.9  
    6.10  object Query_Operation
    6.11  {
    6.12 @@ -25,9 +23,9 @@
    6.13    }
    6.14  }
    6.15  
    6.16 -class Query_Operation(
    6.17 -  editor: Editor[View],
    6.18 -  view: View,
    6.19 +class Query_Operation[Editor_Context](
    6.20 +  editor: Editor[Editor_Context],
    6.21 +  editor_context: Editor_Context,
    6.22    operation_name: String,
    6.23    consume_status: Query_Operation.Status.Value => Unit,
    6.24    consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
    6.25 @@ -151,12 +149,12 @@
    6.26    {
    6.27      Swing_Thread.require()
    6.28  
    6.29 -    editor.current_node_snapshot(view) match {
    6.30 +    editor.current_node_snapshot(editor_context) match {
    6.31        case Some(snapshot) =>
    6.32          remove_overlay()
    6.33          reset_state()
    6.34          consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
    6.35 -        editor.current_command(view, snapshot) match {
    6.36 +        editor.current_command(editor_context, snapshot) match {
    6.37            case Some((command, _)) =>
    6.38              current_location = Some(command)
    6.39              current_query = query
    6.40 @@ -174,18 +172,11 @@
    6.41    {
    6.42      Swing_Thread.require()
    6.43  
    6.44 -    current_location match {
    6.45 -      case Some(command) =>
    6.46 -        val snapshot = editor.node_snapshot(command.node_name)
    6.47 -        val commands = snapshot.node.commands
    6.48 -        if (commands.contains(command)) {
    6.49 -          // FIXME revert offset (!?)
    6.50 -          val sources = commands.iterator.takeWhile(_ != command).map(_.source)
    6.51 -          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
    6.52 -          Hyperlink(command.node_name.node, line, column).follow(view)
    6.53 -        }
    6.54 -      case None =>
    6.55 -    }
    6.56 +    for {
    6.57 +      command <- current_location
    6.58 +      snapshot = editor.node_snapshot(command.node_name)
    6.59 +      link <- editor.hyperlink_command(snapshot, command)
    6.60 +    } link.follow(editor_context)
    6.61    }
    6.62  
    6.63  
     7.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 12 15:09:13 2013 +0200
     7.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 12 17:11:27 2013 +0200
     7.3 @@ -199,15 +199,16 @@
     7.4  
     7.5    private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH)
     7.6  
     7.7 -  def hyperlink(range: Text.Range): Option[Text.Info[Hyperlink]] =
     7.8 +  def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
     7.9    {
    7.10 -    snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include), _ =>
    7.11 +    snapshot.cumulate_markup[List[Text.Info[PIDE.editor.Hyperlink]]](
    7.12 +      range, Nil, Some(hyperlink_include), _ =>
    7.13          {
    7.14            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
    7.15            if Path.is_ok(name) =>
    7.16              val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
    7.17 -            val link = Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0))
    7.18 -            Some(link :: links)
    7.19 +            val link = PIDE.editor.hyperlink_file(jedit_file)
    7.20 +            Some(Text.Info(snapshot.convert(info_range), link) :: links)
    7.21  
    7.22            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
    7.23            if !props.exists(
    7.24 @@ -220,23 +221,16 @@
    7.25                  Isabelle_System.source_file(Path.explode(name)) match {
    7.26                    case Some(path) =>
    7.27                      val jedit_file = Isabelle_System.platform_path(path)
    7.28 -                    val link =
    7.29 -                      Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0))
    7.30 -                    Some(link :: links)
    7.31 +                    val link = PIDE.editor.hyperlink_file(jedit_file, line)
    7.32 +                    Some(Text.Info(snapshot.convert(info_range), link) :: links)
    7.33                    case None => None
    7.34                  }
    7.35  
    7.36                case Position.Def_Id_Offset(id, offset) =>
    7.37                  snapshot.state.find_command(snapshot.version, id) match {
    7.38                    case Some((node, command)) =>
    7.39 -                    val sources =
    7.40 -                      node.commands.iterator.takeWhile(_ != command).map(_.source) ++
    7.41 -                        Iterator.single(command.source(Text.Range(0, command.decode(offset))))
    7.42 -                    val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
    7.43 -                    val link =
    7.44 -                      Text.Info(snapshot.convert(info_range),
    7.45 -                        Hyperlink(command.node_name.node, line, column))
    7.46 -                    Some(link :: links)
    7.47 +                    PIDE.editor.hyperlink_command(snapshot, command, offset)
    7.48 +                      .map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
    7.49                    case None => None
    7.50                  }
    7.51  
     8.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Aug 12 15:09:13 2013 +0200
     8.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Aug 12 17:11:27 2013 +0200
     8.3 @@ -135,7 +135,8 @@
     8.4    private var control: Boolean = false
     8.5  
     8.6    private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
     8.7 -  private val hyperlink_area = new Active_Area[Hyperlink]((r: Rendering) => r.hyperlink _)
     8.8 +  private val hyperlink_area =
     8.9 +    new Active_Area[PIDE.editor.Hyperlink]((r: Rendering) => r.hyperlink _)
    8.10    private val active_area = new Active_Area[XML.Elem]((r: Rendering) => r.active _)
    8.11  
    8.12    private val active_areas =
     9.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 12 15:09:13 2013 +0200
     9.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 12 17:11:27 2013 +0200
     9.3 @@ -41,7 +41,7 @@
     9.4                } model.node_required = !model.node_required
     9.5              }
     9.6            }
     9.7 -          else if (clicks == 2) Hyperlink(listData(index).node).follow(view)
     9.8 +          else if (clicks == 2) PIDE.editor.goto(view, listData(index).node)
     9.9          }
    9.10        case MouseMoved(_, point, _) =>
    9.11          val index = peer.locationToIndex(point)
    10.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Mon Aug 12 15:09:13 2013 +0200
    10.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Aug 12 17:11:27 2013 +0200
    10.3 @@ -89,22 +89,14 @@
    10.4      extends Entry
    10.5    {
    10.6      def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory)
    10.7 -    def follow(snapshot: Document.Snapshot): Unit = Hyperlink(name.node).follow(view)
    10.8 +    def follow(snapshot: Document.Snapshot) { PIDE.editor.goto(view, name.node) }
    10.9    }
   10.10  
   10.11    private case class Command_Entry(command: Command, timing: Double) extends Entry
   10.12    {
   10.13      def print: String = "  " + Time.print_seconds(timing) + "s command " + quote(command.name)
   10.14 -
   10.15      def follow(snapshot: Document.Snapshot)
   10.16 -    {
   10.17 -      val node = snapshot.version.nodes(command.node_name)
   10.18 -      if (node.commands.contains(command)) {
   10.19 -        val sources = node.commands.iterator.takeWhile(_ != command).map(_.source)
   10.20 -        val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
   10.21 -        Hyperlink(command.node_name.node, line, column).follow(view)
   10.22 -      }
   10.23 -    }
   10.24 +    { PIDE.editor.hyperlink_command(snapshot, command).foreach(_.follow(view)) }
   10.25    }
   10.26  
   10.27