--- a/src/Pure/General/path.ML Sat Sep 10 13:43:09 2011 +0200
+++ b/src/Pure/General/path.ML Sat Sep 10 14:28:07 2011 +0200
@@ -185,9 +185,20 @@
val expand = rep #> maps eval #> norm #> Path;
-(* source position *)
+(* source position -- with smart replacement ISABELLE_HOME *)
+
+val isabelle_home = explode_path "~~";
-val position = Position.file o implode_path o expand;
+fun position path =
+ let
+ val s = implode_path path;
+ val prfx = implode_path (expand isabelle_home) ^ "/";
+ in
+ Position.file
+ (case try (unprefix prfx) s of
+ NONE => s
+ | SOME s' => "~~/" ^ s')
+ end;
(*final declarations of this structure!*)