--- 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))) =>