# HG changeset patch
# User wenzelm
# Date 1394708983 -3600
# Node ID 81c66d9e274ba6e6dc07af29e96d75a11ff1f810
# Parent  efa24d31e59537dc9e444342720001ff5ae4db51
even smarter Path.smart_implode;

diff -r efa24d31e595 -r 81c66d9e274b src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Thu Mar 13 11:34:05 2014 +0100
+++ b/src/Pure/General/path.ML	Thu Mar 13 12:09:43 2014 +0100
@@ -195,18 +195,23 @@
 val expand = rep #> maps eval #> norm #> Path;
 
 
-(* smart replacement of $ISABELLE_HOME *)
+(* smart implode *)
 
 fun smart_implode path =
   let
     val full_name = implode_path (expand path);
-    val isabelle_home = implode_path (expand (explode_path "~~"));
+    fun fold_path a =
+      let val b = implode_path (expand (explode_path a)) in
+        if full_name = b then SOME a
+        else
+          (case try (unprefix (b ^ "/")) full_name of
+            SOME name => SOME (a ^ "/" ^ name)
+          | NONE => NONE)
+      end;
   in
-    if full_name = isabelle_home then "~~"
-    else
-      (case try (unprefix (isabelle_home ^ "/")) full_name of
-        SOME name => "~~/" ^ name
-      | NONE => implode_path path)
+    (case get_first fold_path ["~~", "$ISABELLE_HOME_USER", "~"] of
+      SOME name => name
+    | NONE => implode_path path)
   end;
 
 val position = Position.file o smart_implode;