8 sig |
8 sig |
9 val find_first_in_list_vector : (''a * 'b) list vector -> ''a -> 'b option |
9 val find_first_in_list_vector : (''a * 'b) list vector -> ''a -> 'b option |
10 val plural_s : int -> string |
10 val plural_s : int -> string |
11 val serial_commas : string -> string list -> string list |
11 val serial_commas : string -> string list -> string list |
12 val simplify_spaces : string -> string |
12 val simplify_spaces : string -> string |
13 val strip_spaces_except_between_ident_chars : string -> string |
|
14 val parse_bool_option : bool -> string -> string -> bool option |
13 val parse_bool_option : bool -> string -> string -> bool option |
15 val parse_time_option : string -> string -> Time.time option |
14 val parse_time_option : string -> string -> Time.time option |
16 val scan_integer : string list -> int * string list |
15 val scan_integer : string list -> int * string list |
17 val nat_subscript : int -> string |
16 val nat_subscript : int -> string |
18 val unyxml : string -> string |
17 val unyxml : string -> string |
39 | serial_commas _ [s] = [s] |
38 | serial_commas _ [s] = [s] |
40 | serial_commas conj [s1, s2] = [s1, conj, s2] |
39 | serial_commas conj [s1, s2] = [s1, conj, s2] |
41 | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] |
40 | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] |
42 | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss |
41 | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss |
43 |
42 |
44 fun strip_spaces_in_list _ [] = [] |
43 val simplify_spaces = ATP_Proof.strip_spaces (K true) |
45 | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1] |
|
46 | strip_spaces_in_list is_evil [c1, c2] = |
|
47 strip_spaces_in_list is_evil [c1] @ strip_spaces_in_list is_evil [c2] |
|
48 | strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) = |
|
49 if Char.isSpace c1 then |
|
50 strip_spaces_in_list is_evil (c2 :: c3 :: cs) |
|
51 else if Char.isSpace c2 then |
|
52 if Char.isSpace c3 then |
|
53 strip_spaces_in_list is_evil (c1 :: c3 :: cs) |
|
54 else |
|
55 str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @ |
|
56 strip_spaces_in_list is_evil (c3 :: cs) |
|
57 else |
|
58 str c1 :: strip_spaces_in_list is_evil (c2 :: c3 :: cs) |
|
59 fun strip_spaces is_evil = |
|
60 implode o strip_spaces_in_list is_evil o String.explode |
|
61 |
|
62 val simplify_spaces = strip_spaces (K true) |
|
63 |
|
64 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" |
|
65 val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char |
|
66 |
44 |
67 fun parse_bool_option option name s = |
45 fun parse_bool_option option name s = |
68 (case s of |
46 (case s of |
69 "smart" => if option then NONE else raise Option |
47 "smart" => if option then NONE else raise Option |
70 | "false" => SOME false |
48 | "false" => SOME false |