# HG changeset patch
# User wenzelm
# Date 1315657687 -7200
# Node ID 49ea566cb3b4587f9347857101e9ad7e83191b11
# Parent  fe711df09fd92e81c95a481a1e79a6127b31aa0b
more symbolic file positions via smart replacement of ISABELLE_HOME -- allows Isabelle distribution to be moved later on;

diff -r fe711df09fd9 -r 49ea566cb3b4 Admin/CHECKLIST
--- 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;
diff -r fe711df09fd9 -r 49ea566cb3b4 src/Pure/General/path.ML
--- 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!*)