# HG changeset patch
# User wenzelm
# Date 1394703288 -3600
# Node ID 4a7a07c018570db3e2d760c49d1a6ff650213650
# Parent  31e427387ab5c551518367291ac2df655ecea43c
clarified Path.smart_implode;
more informative report and rendering;

diff -r 31e427387ab5 -r 4a7a07c01857 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/Pure/General/path.ML	Thu Mar 13 10:34:48 2014 +0100
@@ -30,6 +30,7 @@
   val ext: string -> T -> T
   val split_ext: T -> T * string
   val expand: T -> T
+  val smart_implode: T -> string
   val position: T -> Position.T
 end;
 
@@ -194,21 +195,21 @@
 val expand = rep #> maps eval #> norm #> Path;
 
 
-(* source position -- with smart replacement of ISABELLE_HOME *)
+(* smart replacement of $ISABELLE_HOME *)
 
-val isabelle_home = explode_path "~~";
-
-fun position path =
+fun smart_implode path =
   let
-    val s = implode_path path;
-    val prfx = implode_path (expand isabelle_home) ^ "/";
+    val full_name = implode_path (expand path);
+    val isabelle_home = implode_path (expand (explode_path "~~"));
   in
-    Position.file
-      (case try (unprefix prfx) s of
-        NONE => s
-      | SOME s' => "~~/" ^ s')
+    if full_name = isabelle_home then "~~"
+    else
+      (case try (unprefix (isabelle_home ^ "/")) full_name of
+        SOME name => "~~/" ^ name
+      | NONE => implode_path path)
   end;
 
+val position = Position.file o smart_implode;
 
 (*final declarations of this structure!*)
 val implode = implode_path;
diff -r 31e427387ab5 -r 4a7a07c01857 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/Pure/Thy/thy_load.ML	Thu Mar 13 10:34:48 2014 +0100
@@ -200,7 +200,7 @@
     val path = Path.append dir (Path.explode name)
       handle ERROR msg => error (msg ^ Position.here pos);
 
-    val _ = Context_Position.report ctxt pos (Markup.path name);
+    val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
     val _ =
       if can Path.expand path andalso File.exists path then ()
       else
diff -r 31e427387ab5 -r 4a7a07c01857 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Mar 12 22:57:50 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Mar 13 10:34:48 2014 +0100
@@ -471,7 +471,8 @@
           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
           if Path.is_valid(name) =>
             val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
-            Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
+            val text = "path " + quote(name) + "\nfile " + quote(jedit_file)
+            Some(add(prev, r, (true, XML.Text(text))))
           case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
             Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))