# HG changeset patch
# User wenzelm
# Date 1546180079 -3600
# Node ID 47c589d3af77c72cc1f32a923c6bf36617b394a8
# Parent  5aa5a8d6e5b57ae8b0fa92b0bbf48d1958e1bc4f
tuned;

diff -r 5aa5a8d6e5b5 -r 47c589d3af77 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Sat Dec 29 20:32:09 2018 +0100
+++ b/src/Pure/General/path.ML	Sun Dec 30 15:27:59 2018 +0100
@@ -51,18 +51,18 @@
 
 local
 
-fun err_elem msg s = error (msg ^ " path element specification " ^ quote s);
+fun err_elem msg s = error (msg ^ " path element " ^ quote s);
 
-fun check_elem s =
-  if s = "" orelse s = "~" orelse s = "~~" then err_elem "Illegal" s
+val illegal_elem = ["", "~", "~~"];
+val illegal_char = ["/", "\\", "$", ":", "\"", "'"];
+
+val check_elem = tap (fn s =>
+  if member (op =) illegal_elem 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;
+    illegal_char |> List.app (fn c =>
+      if exists_string (fn c' => c = c') s then
+        err_elem ("Illegal character " ^ quote c ^ " in") s
+      else ()));
 
 in
 
diff -r 5aa5a8d6e5b5 -r 47c589d3af77 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sat Dec 29 20:32:09 2018 +0100
+++ b/src/Pure/General/path.scala	Sun Dec 30 15:27:59 2018 +0100
@@ -24,14 +24,17 @@
   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 " + quote(s))
+
+  private val illegal_elem = Set("", "~", "~~")
+  private val illegal_char = "/\\$:\"'"
 
   private def check_elem(s: String): String =
-    if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
+    if (illegal_elem.contains(s)) err_elem("Illegal", s)
     else {
-      "/\\$:\"'".iterator.foreach(c =>
-        if (s.iterator.contains(c))
-          err_elem("Illegal character " + quote(c.toString) + " in", s))
+      for (c <- illegal_char if s.contains(c)) {
+        err_elem("Illegal character " + quote(c.toString) + " in", s)
+      }
       s
     }