avoid markup-generating @{make_string}
authorblanchet
Wed May 21 14:09:42 2014 +0200 (2014-05-21 ago)
changeset 57037c51132be8e16
parent 57036 22568fb89165
child 57038 2114f3224b2c
avoid markup-generating @{make_string}
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed May 21 13:52:46 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed May 21 14:09:42 2014 +0200
     1.3 @@ -246,7 +246,7 @@
     1.4              SOME name => error ("No such prover: " ^ name ^ ".")
     1.5            | NONE => ())
     1.6          val _ = print "Sledgehammering..."
     1.7 -        val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode"))
     1.8 +        val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode"))
     1.9  
    1.10          val spying_str_of_factss =
    1.11            commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed May 21 13:52:46 2014 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed May 21 14:09:42 2014 +0200
     2.3 @@ -67,6 +67,7 @@
     2.4      -> prover_problem -> prover_result
     2.5  
     2.6    val SledgehammerN : string
     2.7 +  val str_of_mode : mode -> string
     2.8    val smtN : string
     2.9    val overlord_file_location_of_prover : string -> string * string
    2.10    val proof_banner : mode -> string -> string
    2.11 @@ -104,12 +105,19 @@
    2.12  open Sledgehammer_Fact
    2.13  open Sledgehammer_Proof_Methods
    2.14  
    2.15 -datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
    2.16 -
    2.17  (* Identifier that distinguishes Sledgehammer from other tools that could use
    2.18     "Async_Manager". *)
    2.19  val SledgehammerN = "Sledgehammer"
    2.20  
    2.21 +datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
    2.22 +
    2.23 +fun str_of_mode Auto_Try = "Auto Try"
    2.24 +  | str_of_mode Try = "Try"
    2.25 +  | str_of_mode Normal = "Normal"
    2.26 +  | str_of_mode MaSh = "MaSh"
    2.27 +  | str_of_mode Auto_Minimize = "Auto_Minimize"
    2.28 +  | str_of_mode Minimize = "Minimize"
    2.29 +
    2.30  val smtN = "smt"
    2.31  
    2.32  val proof_method_names = [metisN, smtN]