src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 37962 d7dbe01f48d7
parent 37575 cfc5e281740f
child 37995 06f02b15ef8a
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 23 15:04:49 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 23 21:29:29 2010 +0200
     1.3 @@ -9,8 +9,10 @@
     1.4    val plural_s : int -> string
     1.5    val serial_commas : string -> string list -> string list
     1.6    val timestamp : unit -> string
     1.7 +  val strip_spaces : string -> string
     1.8    val parse_bool_option : bool -> string -> string -> bool option
     1.9    val parse_time_option : string -> string -> Time.time option
    1.10 +  val scan_integer : string list -> int * string list
    1.11    val nat_subscript : int -> string
    1.12    val unyxml : string -> string
    1.13    val maybe_quote : string -> string
    1.14 @@ -31,6 +33,25 @@
    1.15  
    1.16  val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
    1.17  
    1.18 +fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
    1.19 +
    1.20 +fun strip_spaces_in_list [] = ""
    1.21 +  | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
    1.22 +  | strip_spaces_in_list [c1, c2] =
    1.23 +    strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
    1.24 +  | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
    1.25 +    if Char.isSpace c1 then
    1.26 +      strip_spaces_in_list (c2 :: c3 :: cs)
    1.27 +    else if Char.isSpace c2 then
    1.28 +      if Char.isSpace c3 then
    1.29 +        strip_spaces_in_list (c1 :: c3 :: cs)
    1.30 +      else
    1.31 +        str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
    1.32 +        strip_spaces_in_list (c3 :: cs)
    1.33 +    else
    1.34 +      str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
    1.35 +val strip_spaces = strip_spaces_in_list o String.explode
    1.36 +
    1.37  fun parse_bool_option option name s =
    1.38    (case s of
    1.39       "smart" => if option then NONE else raise Option
    1.40 @@ -61,6 +82,9 @@
    1.41          SOME (Time.fromMilliseconds msecs)
    1.42      end
    1.43  
    1.44 +fun is_head_digit s = Char.isDigit (String.sub (s, 0))
    1.45 +val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
    1.46 +
    1.47  val subscript = implode o map (prefix "\<^isub>") o explode
    1.48  fun nat_subscript n =
    1.49    n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript