--- a/src/Pure/General/path.ML Thu Jan 10 19:34:25 2019 +0100
+++ b/src/Pure/General/path.ML Fri Jan 11 10:59:21 2019 +0100
@@ -7,6 +7,7 @@
signature PATH =
sig
+ val check_elem: string -> unit
eqtype T
val is_current: T -> bool
val current: T
@@ -56,7 +57,9 @@
val illegal_elem = ["", "~", "~~", ".", ".."];
val illegal_char = ["/", "\\", "$", ":", "\"", "'", "<", ">", "|", "?", "*"];
-val check_elem = tap (fn s =>
+in
+
+fun check_elem s =
if member (op =) illegal_elem s then err_elem "Illegal" s
else
(s, ()) |-> fold_string (fn c => fn () =>
@@ -64,13 +67,11 @@
err_elem ("Illegal control character " ^ string_of_int (ord c) ^ " in") s
else if member (op =) illegal_char c then
err_elem ("Illegal character " ^ quote c ^ " in") s
- else ()));
-
-in
+ else ());
-val root_elem = Root o check_elem;
-val basic_elem = Basic o check_elem;
-val variable_elem = Variable o check_elem;
+val root_elem = Root o tap check_elem;
+val basic_elem = Basic o tap check_elem;
+val variable_elem = Variable o tap check_elem;
end;