# 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!*)