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