more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;
--- a/Admin/CHECKLIST Sat Sep 10 13:43:09 2011 +0200
+++ b/Admin/CHECKLIST Sat Sep 10 14:28:07 2011 +0200
@@ -11,6 +11,8 @@
- check persistent sessions with PG and Poly/ML 5.x;
+- check file positions within logic images (hyperlinks etc.);
+
- Admin/update-keywords;
- check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
--- 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!*)