# HG changeset patch
# User wenzelm
# Date 1393840773 -3600
# Node ID 65c9968286d54a0be9456fcf96f484c5d345ec78
# Parent  1421394576536ec9cac2f9bf1af749a17436bd42
tuned signature;

diff -r 142139457653 -r 65c9968286d5 src/Tools/jEdit/src/documentation_dockable.scala
--- a/src/Tools/jEdit/src/documentation_dockable.scala	Mon Mar 03 10:41:58 2014 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala	Mon Mar 03 10:59:33 2014 +0100
@@ -71,7 +71,7 @@
                         "Documentation error", GUI.scrollable_text(Exn.message(exn)))
                   })
               case Text_File(_, path) =>
-                PIDE.editor.goto(view, Isabelle_System.platform_path(path))
+                PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
               case _ =>
             }
           case _ =>
diff -r 142139457653 -r 65c9968286d5 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 10:41:58 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Mar 03 10:59:33 2014 +0100
@@ -109,9 +109,9 @@
     synchronized { overlays = overlays.remove(command, fn, args) }
 
 
-  /* hyperlinks */
+  /* navigation */
 
-  def goto(view: View, name: String, line: Int = 0, column: Int = 0)
+  def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
   {
     Swing_Thread.require()
 
@@ -142,6 +142,9 @@
     }
   }
 
+
+  /* hyperlinks */
+
   override def hyperlink_command(snapshot: Document.Snapshot, command: Command, raw_offset: Int = 0)
     : Option[Hyperlink] =
   {
@@ -156,7 +159,7 @@
               (if (raw_offset == 0) Iterator.empty
                else Iterator.single(command.source(Text.Range(0, command.decode(raw_offset)))))
           val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
-          Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
+          Some(new Hyperlink { def follow(view: View) { goto_file(view, file_name, line, column) } })
       }
     }
   }
@@ -173,7 +176,7 @@
   }
 
   def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
-    new Hyperlink { def follow(view: View) = goto(view, name, line, column) }
+    new Hyperlink { def follow(view: View) = goto_file(view, name, line, column) }
 
   def hyperlink_source_file(name: String, line: Int): Option[Hyperlink] =
     if (Path.is_ok(name))
diff -r 142139457653 -r 65c9968286d5 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 10:41:58 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 10:59:33 2014 +0100
@@ -327,6 +327,15 @@
 
   /* hyperlinks */
 
+  private def hyperlink_file(props: Properties.T): Option[PIDE.editor.Hyperlink] =
+    props match {
+      case Position.Def_Line_File(line, name) =>
+        PIDE.editor.hyperlink_source_file(name, line)
+      case Position.Def_Id_Offset(id, offset) =>
+        PIDE.editor.hyperlink_command_id(snapshot, id, offset)
+      case _ => None
+    }
+
   def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   {
     snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
@@ -347,27 +356,12 @@
             { case (Markup.KIND, Markup.ML_OPEN) => true
               case (Markup.KIND, Markup.ML_STRUCTURE) => true
               case _ => false }) =>
-
-            val opt_link =
-              props match {
-                case Position.Def_Line_File(line, name) =>
-                  PIDE.editor.hyperlink_source_file(name, line)
-                case Position.Def_Id_Offset(id, offset) =>
-                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
-                case _ => None
-              }
-            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
+            hyperlink_file(props).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 =
-              props match {
-                case Position.Line_File(line, name) =>
-                  PIDE.editor.hyperlink_source_file(name, line)
-                case Position.Id_Offset(id, offset) =>
-                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
-                case _ => None
-              }
-            opt_link.map(link => links :+ (Text.Info(snapshot.convert(info_range), link)))
+            hyperlink_file(props).map(link =>
+              (links :+ Text.Info(snapshot.convert(info_range), link)))
 
           case _ => None
         }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
diff -r 142139457653 -r 65c9968286d5 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Mar 03 10:41:58 2014 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Mar 03 10:59:33 2014 +0100
@@ -40,7 +40,7 @@
               } model.node_required = !model.node_required
             }
           }
-          else if (clicks == 2) PIDE.editor.goto(view, listData(index).node)
+          else if (clicks == 2) PIDE.editor.goto_file(view, listData(index).node)
         }
       case MouseMoved(_, point, _) =>
         val index = peer.locationToIndex(point)
diff -r 142139457653 -r 65c9968286d5 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Mon Mar 03 10:41:58 2014 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Mon Mar 03 10:59:33 2014 +0100
@@ -88,7 +88,7 @@
     extends Entry
   {
     def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory)
-    def follow(snapshot: Document.Snapshot) { PIDE.editor.goto(view, name.node) }
+    def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(view, name.node) }
   }
 
   private case class Command_Entry(command: Command, timing: Double) extends Entry