--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Aug 24 21:40:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Aug 24 22:57:22 2010 +0200
@@ -9,7 +9,8 @@
val is_true_for : (string * bool) vector -> string -> bool
val plural_s : int -> string
val serial_commas : string -> string list -> string list
- val strip_spaces : string -> string
+ val simplify_spaces : string -> string
+ val strip_spaces_except_between_ident_chars : string -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
val scan_integer : string list -> int * string list
@@ -39,24 +40,27 @@
| serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
| serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-
-fun strip_spaces_in_list [] = ""
- | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
- | strip_spaces_in_list [c1, c2] =
- strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
- | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
+fun strip_spaces_in_list _ [] = ""
+ | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then "" else str c1
+ | strip_spaces_in_list is_evil [c1, c2] =
+ strip_spaces_in_list is_evil [c1] ^ strip_spaces_in_list is_evil [c2]
+ | strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) =
if Char.isSpace c1 then
- strip_spaces_in_list (c2 :: c3 :: cs)
+ strip_spaces_in_list is_evil (c2 :: c3 :: cs)
else if Char.isSpace c2 then
if Char.isSpace c3 then
- strip_spaces_in_list (c1 :: c3 :: cs)
+ strip_spaces_in_list is_evil (c1 :: c3 :: cs)
else
- str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
- strip_spaces_in_list (c3 :: cs)
+ str c1 ^ (if forall is_evil [c1, c3] then " " else "") ^
+ strip_spaces_in_list is_evil (c3 :: cs)
else
- str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
-val strip_spaces = strip_spaces_in_list o String.explode
+ str c1 ^ strip_spaces_in_list is_evil (c2 :: c3 :: cs)
+fun strip_spaces is_evil = strip_spaces_in_list is_evil o String.explode
+
+val simplify_spaces = strip_spaces (K true)
+
+fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
+val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
fun parse_bool_option option name s =
(case s of