more generic explosion of options (also accept newlines, etc.)
authorboehmes
Wed Nov 25 12:29:37 2009 +0100 (2009-11-25)
changeset 33894395df8f652b6
parent 33893 24b648ea4834
child 33895 3e7c51bbeb24
more generic explosion of options (also accept newlines, etc.)
src/HOL/SMT/Tools/z3_solver.ML
     1.1 --- a/src/HOL/SMT/Tools/z3_solver.ML	Wed Nov 25 12:28:29 2009 +0100
     1.2 +++ b/src/HOL/SMT/Tools/z3_solver.ML	Wed Nov 25 12:29:37 2009 +0100
     1.3 @@ -22,10 +22,12 @@
     1.4  
     1.5  fun add xs ys = ys @ xs
     1.6  
     1.7 +fun explode_options s = String.tokens (Symbol.is_ascii_blank o str) s
     1.8 +
     1.9  fun get_options ctxt =
    1.10    ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false"]
    1.11    |> Config.get ctxt proofs ? add ["DISPLAY_PROOF=true", "PROOF_MODE=2"]
    1.12 -  |> add (space_explode " " (Config.get ctxt options))
    1.13 +  |> add (explode_options (Config.get ctxt options))
    1.14  
    1.15  fun pretty_config context = [
    1.16    Pretty.str ("With proofs: " ^