# HG changeset patch
# User wenzelm
# Date 1369163110 -7200
# Node ID 090a519982e9568672590787f629f8ab92da3158
# Parent  88b423034d4f144b07a91abb575b556dc16af9fd
tuned messages;

diff -r 88b423034d4f -r 090a519982e9 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Tue May 21 18:03:36 2013 +0200
+++ b/src/Pure/General/path.ML	Tue May 21 21:05:10 2013 +0200
@@ -45,21 +45,24 @@
 
 local
 
-fun err_elem msg chs = error (msg ^ " path element specification: " ^ quote (implode chs));
+fun err_elem msg s = error (msg ^ " path element specification " ^ quote s);
 
-fun check_elem (chs as []) = err_elem "Illegal" chs
-  | check_elem (chs as ["~"]) = err_elem "Illegal" chs
-  | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
-  | check_elem chs =
-      (case inter (op =) ["/", "\\", "$", ":", "\"", "'"] chs of
-        [] => chs
-      | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
+fun check_elem s =
+  if s = "" orelse s = "~" orelse s = "~~" then err_elem "Illegal" s
+  else
+    let
+      fun check c =
+        if exists_string (fn c' => c = c') s then
+          err_elem ("Illegal character " ^ quote c ^ " in") s
+        else ();
+      val _ = List.app check ["/", "\\", "$", ":", "\"", "'"];
+    in s end;
 
 in
 
-val root_elem = Root o implode o check_elem;
-val basic_elem = Basic o implode o check_elem;
-val variable_elem = Variable o implode o check_elem;
+val root_elem = Root o check_elem;
+val basic_elem = Basic o check_elem;
+val variable_elem = Variable o check_elem;
 
 end;
 
@@ -75,9 +78,9 @@
 
 val current = Path [];
 val root = Path [Root ""];
-fun named_root s = Path [root_elem (raw_explode s)];
-fun basic s = Path [basic_elem (raw_explode s)];
-fun variable s = Path [variable_elem (raw_explode s)];
+fun named_root s = Path [root_elem s];
+fun basic s = Path [basic_elem s];
+fun variable s = Path [variable_elem s];
 val parent = Path [Parent];
 
 fun is_absolute (Path xs) =
@@ -124,31 +127,27 @@
 
 (* explode *)
 
-local
-
-fun explode_elem ".." = Parent
-  | explode_elem "~" = Variable "USER_HOME"
-  | explode_elem "~~" = Variable "ISABELLE_HOME"
-  | explode_elem s =
-      (case raw_explode s of
-        "$" :: cs => variable_elem cs
-      | cs => basic_elem cs);
-
-val explode_elems =
-  rev o map explode_elem o filter_out (fn c => c = "" orelse c = ".");
+fun explode_path str =
+  let
+    fun explode_elem s =
+     (if s = ".." then Parent
+      else if s = "~" then Variable "USER_HOME"
+      else if s = "~~" then Variable "ISABELLE_HOME"
+      else
+        (case try (unprefix "$") s of
+          SOME s' => variable_elem s'
+        | NONE => basic_elem s))
+      handle ERROR msg => cat_error msg ("The error(s) above occurred in " ^ quote str);
 
-in
+    val (roots, raw_elems) =
+      (case take_prefix (equal "") (space_explode "/" str) |>> length of
+        (0, es) => ([], es)
+      | (1, es) => ([Root ""], es)
+      | (_, []) => ([Root ""], [])
+      | (_, e :: es) => ([root_elem e], es));
+    val elems = raw_elems |> filter_out (fn c => c = "" orelse c = ".") |> map explode_elem;
 
-fun explode_path str =
-  let val (roots, raw_elems) =
-    (case take_prefix (equal "") (space_explode "/" str) |>> length of
-      (0, es) => ([], es)
-    | (1, es) => ([Root ""], es)
-    | (_, []) => ([Root ""], [])
-    | (_, e :: es) => ([root_elem (raw_explode e)], es))
-  in Path (norm (explode_elems raw_elems @ roots)) end;
-
-end;
+  in Path (norm (rev elems @ roots)) end;
 
 
 (* print *)
diff -r 88b423034d4f -r 090a519982e9 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Tue May 21 18:03:36 2013 +0200
+++ b/src/Pure/General/path.scala	Tue May 21 21:05:10 2013 +0200
@@ -24,17 +24,16 @@
   private case object Parent extends Elem
 
   private def err_elem(msg: String, s: String): Nothing =
-    error (msg + " path element specification: " + quote(s))
+    error (msg + " path element specification " + quote(s))
 
   private def check_elem(s: String): String =
     if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
-    else
-      s.iterator.filter(c =>
-          c == '/' || c == '\\' || c == '$' || c == ':' || c == '"' || c == '\'').toList match {
-        case Nil => s
-        case bads =>
-          err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s)
-      }
+    else {
+      "/\\$:\"'".iterator.foreach(c =>
+        if (s.iterator.exists(_ == c))
+          err_elem("Illegal character " + quote(c.toString) + " in", s))
+      s
+    }
 
   private def root_elem(s: String): Elem = Root(check_elem(s))
   private def basic_elem(s: String): Elem = Basic(check_elem(s))
@@ -73,18 +72,18 @@
 
   /* explode */
 
-  private def explode_elem(s: String): Elem =
-    if (s == "..") Parent
-    else if (s == "~") Variable("USER_HOME")
-    else if (s == "~~") Variable("ISABELLE_HOME")
-    else if (s.startsWith("$")) variable_elem(s.substring(1))
-    else basic_elem(s)
-
-  private def explode_elems(ss: List[String]): List[Elem] =
-    ss.filterNot(s => s.isEmpty || s == ".").map(explode_elem).reverse
-
   def explode(str: String): Path =
   {
+    def explode_elem(s: String): Elem =
+      try {
+        if (s == "..") Parent
+        else if (s == "~") Variable("USER_HOME")
+        else if (s == "~~") Variable("ISABELLE_HOME")
+        else if (s.startsWith("$")) variable_elem(s.substring(1))
+        else basic_elem(s)
+      }
+      catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in " + quote(str)) }
+  
     val ss = space_explode('/', str)
     val r = ss.takeWhile(_.isEmpty).length
     val es = ss.dropWhile(_.isEmpty)
@@ -93,7 +92,9 @@
       else if (r == 1) (List(Root("")), es)
       else if (es.isEmpty) (List(Root("")), Nil)
       else (List(root_elem(es.head)), es.tail)
-    new Path(norm_elems(explode_elems(raw_elems) ++ roots))
+    val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem)
+
+    new Path(norm_elems(elems.reverse ++ roots))
   }
 
   def is_ok(str: String): Boolean =