# HG changeset patch
# User wenzelm
# Date 1439305216 -7200
# Node ID 3c8b9b4b577cb30795fb65ace3560616916430f1
# Parent  cc7a1285693f7aa86d2628277e420a510b63025f
support hyperlinks with optional focus change;
no change of focus for debuffer position, to avoid visual glitches and keep panel active;

diff -r cc7a1285693f -r 3c8b9b4b577c src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Tue Aug 11 15:24:49 2015 +0200
+++ b/src/Pure/PIDE/editor.scala	Tue Aug 11 17:00:16 2015 +0200
@@ -27,6 +27,7 @@
     def follow(context: Context): Unit
   }
   def hyperlink_command(
-    snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink]
+    focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
+      : Option[Hyperlink]
 }
 
diff -r cc7a1285693f -r 3c8b9b4b577c src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Tue Aug 11 15:24:49 2015 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Tue Aug 11 17:00:16 2015 +0200
@@ -201,7 +201,7 @@
     for {
       command <- current_location
       snapshot = editor.node_snapshot(command.node_name)
-      link <- editor.hyperlink_command(snapshot, command)
+      link <- editor.hyperlink_command(true, snapshot, command)
     } link.follow(editor_context)
   }
 
diff -r cc7a1285693f -r 3c8b9b4b577c src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Tue Aug 11 15:24:49 2015 +0200
+++ b/src/Tools/jEdit/src/active.scala	Tue Aug 11 17:00:16 2015 +0200
@@ -48,7 +48,7 @@
               case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
                 val link =
                   props match {
-                    case Position.Id(id) => PIDE.editor.hyperlink_command_id(snapshot, id)
+                    case Position.Id(id) => PIDE.editor.hyperlink_command_id(true, snapshot, id)
                     case _ => None
                   }
                 GUI_Thread.later {
diff -r cc7a1285693f -r 3c8b9b4b577c src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 15:24:49 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 17:00:16 2015 +0200
@@ -321,7 +321,7 @@
   private def update_focus(focus: Option[Position.T])
   {
     if (Debugger.focus(focus) && focus.isDefined)
-      PIDE.editor.hyperlink_position(current_snapshot, focus.get).foreach(_.follow(view))
+      PIDE.editor.hyperlink_position(false, current_snapshot, focus.get).foreach(_.follow(view))
   }
 
 
diff -r cc7a1285693f -r 3c8b9b4b577c src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Tue Aug 11 15:24:49 2015 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Tue Aug 11 17:00:16 2015 +0200
@@ -54,10 +54,10 @@
   {
     node.getUserObject match {
       case Text_File(_, path) =>
-        PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
+        PIDE.editor.goto_file(true, view, Isabelle_System.platform_path(path))
       case Documentation(_, _, path) =>
         if (path.is_file)
-          PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
+          PIDE.editor.goto_file(true, view, Isabelle_System.platform_path(path))
         else {
           Future.fork {
             try { Doc.view(path) }
diff -r cc7a1285693f -r 3c8b9b4b577c src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Aug 11 15:24:49 2015 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Aug 11 17:00:16 2015 +0200
@@ -133,13 +133,13 @@
     }
   }
 
-  def goto_buffer(view: View, buffer: Buffer, offset: Text.Offset)
+  def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset)
   {
     GUI_Thread.require {}
 
     push_position(view)
 
-    view.goToBuffer(buffer)
+    if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
     try { view.getTextArea.moveCaretPosition(offset) }
     catch {
       case _: ArrayIndexOutOfBoundsException =>
@@ -147,7 +147,7 @@
     }
   }
 
-  def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
+  def goto_file(focus: Boolean, view: View, name: String, line: Int = 0, column: Int = 0)
   {
     GUI_Thread.require {}
 
@@ -155,7 +155,7 @@
 
     JEdit_Lib.jedit_buffer(name) match {
       case Some(buffer) =>
-        view.goToBuffer(buffer)
+        if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
         val text_area = view.getTextArea
 
         try {
@@ -197,21 +197,21 @@
       override def toString: String = "URL " + quote(name)
     }
 
-  def hyperlink_buffer(buffer: Buffer, offset: Text.Offset): Hyperlink =
+  def hyperlink_buffer(focus: Boolean, buffer: Buffer, offset: Text.Offset): Hyperlink =
     new Hyperlink {
       val external = false
-      def follow(view: View): Unit = goto_buffer(view, buffer, offset)
+      def follow(view: View): Unit = goto_buffer(focus, view, buffer, offset)
       override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
     }
 
-  def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
+  def hyperlink_file(focus: Boolean, name: String, line: Int = 0, column: Int = 0): Hyperlink =
     new Hyperlink {
       val external = false
-      def follow(view: View): Unit = goto_file(view, name, line, column)
+      def follow(view: View): Unit = goto_file(focus, view, name, line, column)
       override def toString: String = "file " + quote(name)
     }
 
-  def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
+  def hyperlink_source_file(focus: Boolean, source_name: String, line: Int, offset: Symbol.Offset)
     : Option[Hyperlink] =
   {
     val opt_name =
@@ -235,15 +235,16 @@
                     zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
                       Symbol.advance_line_column)
               }
-            Some(hyperlink_file(name, line, column))
-          case _ => Some(hyperlink_file(name, line))
+            Some(hyperlink_file(focus, name, line, column))
+          case _ => Some(hyperlink_file(focus, name, line))
         }
       case None => None
     }
   }
 
   override def hyperlink_command(
-    snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink] =
+    focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
+      : Option[Hyperlink] =
   {
     if (snapshot.is_outdated) None
     else {
@@ -256,39 +257,40 @@
               (if (offset == 0) Iterator.empty
                else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
           val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
-          Some(hyperlink_file(file_name, line, column))
+          Some(hyperlink_file(focus, file_name, line, column))
       }
     }
   }
 
   def hyperlink_command_id(
-    snapshot: Document.Snapshot,
-    id: Document_ID.Generic,
-    offset: Symbol.Offset = 0): Option[Hyperlink] =
+    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
+      : Option[Hyperlink] =
   {
     snapshot.state.find_command(snapshot.version, id) match {
-      case Some((node, command)) => hyperlink_command(snapshot, command, offset)
+      case Some((node, command)) => hyperlink_command(focus, snapshot, command, offset)
       case None => None
     }
   }
 
-  def hyperlink_position(snapshot: Document.Snapshot, pos: Position.T): Option[Hyperlink] =
+  def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
+      : Option[Hyperlink] =
     pos match {
       case Position.Line_File(line, name) =>
         val offset = Position.Offset.unapply(pos) getOrElse 0
-        hyperlink_source_file(name, line, offset)
+        hyperlink_source_file(focus, name, line, offset)
       case Position.Id_Offset0(id, offset) =>
-        hyperlink_command_id(snapshot, id, offset)
+        hyperlink_command_id(focus, snapshot, id, offset)
       case _ => None
     }
 
-  def hyperlink_def_position(snapshot: Document.Snapshot, pos: Position.T): Option[Hyperlink] =
+  def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
+      : Option[Hyperlink] =
     pos match {
       case Position.Def_Line_File(line, name) =>
         val offset = Position.Def_Offset.unapply(pos) getOrElse 0
-        hyperlink_source_file(name, line, offset)
+        hyperlink_source_file(focus, name, line, offset)
       case Position.Def_Id_Offset0(id, offset) =>
-        hyperlink_command_id(snapshot, id, offset)
+        hyperlink_command_id(focus, snapshot, id, offset)
       case _ => None
     }
 }
diff -r cc7a1285693f -r 3c8b9b4b577c src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Tue Aug 11 15:24:49 2015 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Tue Aug 11 17:00:16 2015 +0200
@@ -406,7 +406,7 @@
       range, Vector.empty, Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
-            val link = PIDE.editor.hyperlink_file(jedit_file(name))
+            val link = PIDE.editor.hyperlink_file(true, jedit_file(name))
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
@@ -418,18 +418,18 @@
             { case (Markup.KIND, Markup.ML_OPEN) => true
               case (Markup.KIND, Markup.ML_STRUCTURE) => true
               case _ => false }) =>
-            val opt_link = PIDE.editor.hyperlink_def_position(snapshot, props)
+            val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
-            val opt_link = PIDE.editor.hyperlink_position(snapshot, props)
+            val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props)
             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
             val opt_link =
               Bibtex_JEdit.entries_iterator.collectFirst(
                 { case (a, buffer, offset) if a == name =>
-                    PIDE.editor.hyperlink_buffer(buffer, offset) })
+                    PIDE.editor.hyperlink_buffer(true, buffer, offset) })
             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
 
           case _ => None
diff -r cc7a1285693f -r 3c8b9b4b577c src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Aug 11 15:24:49 2015 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Aug 11 17:00:16 2015 +0200
@@ -45,7 +45,7 @@
               } model.node_required = !model.node_required
             }
           }
-          else if (clicks == 2) PIDE.editor.goto_file(view, listData(index).node)
+          else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node)
         }
       case MouseMoved(_, point, _) =>
         val index = peer.locationToIndex(point)
diff -r cc7a1285693f -r 3c8b9b4b577c src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Aug 11 15:24:49 2015 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Aug 11 17:00:16 2015 +0200
@@ -88,7 +88,7 @@
   {
     def print: String =
       Time.print_seconds(timing) + "s theory " + quote(name.theory)
-    def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(view, name.node) }
+    def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(true, view, name.node) }
   }
 
   private case class Command_Entry(command: Command, timing: Double) extends Entry
@@ -96,7 +96,7 @@
     def print: String =
       "  " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
     def follow(snapshot: Document.Snapshot)
-    { PIDE.editor.hyperlink_command(snapshot, command).foreach(_.follow(view)) }
+    { PIDE.editor.hyperlink_command(true, snapshot, command).foreach(_.follow(view)) }
   }