# HG changeset patch
# User wenzelm
# Date 1346856826 -7200
# Node ID 5d0cd770828e142d823535a060bb561c13763d66
# Parent  bd6a18a1a5afe443c5c879989195f25ec52a7120
added tooltip to reveal jEdit platform file name;

diff -r bd6a18a1a5af -r 5d0cd770828e src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Sep 05 15:53:31 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Sep 05 16:53:46 2012 +0200
@@ -190,8 +190,8 @@
       Isabelle_Markup.DOC_SOURCE -> "document source")
 
   private val tooltip_elements =
-    Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING) ++
-    tooltips.keys
+    Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
+      Isabelle_Markup.PATH) ++ tooltips.keys
 
   private def string_of_typing(kind: String, body: XML.Body): String =
     Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
@@ -208,6 +208,10 @@
         {
           case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
             add(prev, r, (true, kind + " " + quote(name)))
+          case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
+          if Path.is_ok(name) =>
+            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
+            add(prev, r, (true, "file " + quote(jedit_file)))
           case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) =>
             add(prev, r, (true, string_of_typing("::", body)))
           case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>