--- 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