# HG changeset patch # User blanchet # Date 1471170369 -7200 # Node ID 1bc4bc2c9fd1050b0a5262e0b35acb9e2570e1f0 # Parent 94a89b95b871c88ff697537c7af1210335442aa2 killed final stops in Sledgehammer and friends diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Aug 14 12:26:09 2016 +0200 @@ -301,7 +301,7 @@ let fun default_prover_name () = hd (#provers (Sledgehammer_Commands.default_params thy [])) - handle List.Empty => error "No ATP available." + handle List.Empty => error "No ATP available" in (case AList.lookup (op =) args proverK of SOME name => name diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Sun Aug 14 12:26:09 2016 +0200 @@ -88,11 +88,11 @@ val name = (case names |> filter (curry (op <>) "") |> distinct (op =) of [name] => name - | names => error ("Input files out of sync: facts " ^ commas (map quote names) ^ ".")) + | names => error ("Input files out of sync: facts " ^ commas (map quote names))) val th = case find_first (fn (_, th) => nickname_of_thm th = name) facts of SOME (_, th) => th - | NONE => error ("No fact called \"" ^ name ^ "\".") + | NONE => error ("No fact called \"" ^ name) val goal = goal_of_thm (Proof_Context.theory_of ctxt) th val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt val isar_deps = these (isar_dependencies_of name_tabs th) diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/TPTP/mash_export.ML Sun Aug 14 12:26:09 2016 +0200 @@ -310,7 +310,7 @@ val (name', mepo_suggs) = extract_suggestions mepo_line ||> (map fst #> weight_facts_steeply) - val _ = if name = name' then () else error "Input files out of sync." + val _ = if name = name' then () else error "Input files out of sync" val mess = [(mepo_weight, (mepo_suggs, [])), (mash_weight, (mash_suggs, []))] @@ -322,7 +322,7 @@ val mepo_lines = Path.explode mepo_file_name |> File.read_lines in if length mash_lines = length mepo_lines then List.app do_fact (mash_lines ~~ mepo_lines) - else warning "Skipped: MaSh file missing or out of sync with MePo file." + else warning "Skipped: MaSh file missing or out of sync with MePo file" end end; diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Aug 14 12:26:09 2016 +0200 @@ -666,7 +666,7 @@ | ("erased", (NONE, All_Types (* naja *))) => Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types) | _ => raise Same.SAME)) - handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".") + handle Same.SAME => error ("Unknown type encoding: " ^ quote s) fun adjust_order THF_Without_Choice (Higher_Order _) = Higher_Order THF_Without_Choice @@ -1803,7 +1803,7 @@ else if lam_trans = keep_lamsN then map (Envir.eta_contract) #> rpair [] else - error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".") + error ("Unknown lambda translation scheme: " ^ quote lam_trans) val pull_and_reorder_definitions = let diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Sun Aug 14 12:26:09 2016 +0200 @@ -173,44 +173,41 @@ "" val missing_message_tail = - " appears to be missing. You will need to install it if you want to invoke \ - \remote provers." + " appears to be missing; you will need to install it if you want to invoke \ + \remote provers" fun from_lemmas [] = "" | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) -fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable." - | string_of_atp_failure Unprovable = "The generated problem is unprovable." - | string_of_atp_failure GaveUp = "The prover gave up." +fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable" + | string_of_atp_failure Unprovable = "The generated problem is unprovable" + | string_of_atp_failure GaveUp = "The prover gave up" | string_of_atp_failure ProofMissing = - "The prover claims the conjecture is a theorem but did not provide a proof." + "The prover claims the conjecture is a theorem but did not provide a proof" | string_of_atp_failure ProofIncomplete = - "The prover claims the conjecture is a theorem but provided an incomplete proof." + "The prover claims the conjecture is a theorem but provided an incomplete proof" | string_of_atp_failure ProofUnparsable = - "The prover claims the conjecture is a theorem but provided an unparsable proof." + "The prover claims the conjecture is a theorem but provided an unparsable proof" | string_of_atp_failure (UnsoundProof (false, ss)) = "The prover derived \"False\"" ^ from_lemmas ss ^ - ". Specify a sound type encoding or omit the \"type_enc\" option." + "; specify a sound type encoding or omit the \"type_enc\" option" | string_of_atp_failure (UnsoundProof (true, ss)) = "The prover derived \"False\"" ^ from_lemmas ss ^ - ". This could be due to inconsistent axioms (including \"sorry\"s) or to \ - \a bug in Sledgehammer. If the problem persists, please contact the \ - \Isabelle developers." - | string_of_atp_failure CantConnect = "Cannot connect to server." - | string_of_atp_failure TimedOut = "Timed out." + ", which could be due to inconsistent axioms (including \"sorry\"s) or to \ + \a bug in Sledgehammer" + | string_of_atp_failure CantConnect = "Cannot connect to server" + | string_of_atp_failure TimedOut = "Timed out" | string_of_atp_failure Inappropriate = - "The generated problem lies outside the prover's scope." - | string_of_atp_failure OutOfResources = "The prover ran out of resources." + "The generated problem lies outside the prover's scope" + | string_of_atp_failure OutOfResources = "The prover ran out of resources" | string_of_atp_failure NoPerl = "Perl" ^ missing_message_tail | string_of_atp_failure NoLibwwwPerl = "The Perl module \"libwww-perl\"" ^ missing_message_tail - | string_of_atp_failure MalformedInput = - "The generated problem is malformed. Please report this to the Isabelle \ - \developers." - | string_of_atp_failure MalformedOutput = "The prover output is malformed." - | string_of_atp_failure Interrupted = "The prover was interrupted." - | string_of_atp_failure Crashed = "The prover crashed." - | string_of_atp_failure InternalError = "An internal prover error occurred." + | string_of_atp_failure MalformedInput = "The generated problem is malformed" + | string_of_atp_failure MalformedOutput = "The prover output is malformed" + | string_of_atp_failure Interrupted = "The prover was interrupted" + | string_of_atp_failure Crashed = "The prover crashed" + | string_of_atp_failure InternalError = "An internal prover error occurred" | string_of_atp_failure (UnknownError s) = "A prover error occurred" ^ (if s = "" then ". (Pass the \"verbose\" option for details.)" diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Aug 14 12:26:09 2016 +0200 @@ -271,7 +271,7 @@ | ATerm ((s, tys), us) => if s = "" then error "Isar proof reconstruction failed because the ATP proof \ - \contains unparsable material." + \contains unparsable material" else if s = tptp_equal then list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), map (do_term NONE) us) @@ -349,7 +349,7 @@ ATerm ((s, tys), us) => if s = "" then error "Isar proof reconstruction failed because the ATP proof contains unparsable \ - \material." + \material" else if String.isPrefix native_type_prefix s then @{const True} (* ignore TPTP type information (needed?) *) else if s = tptp_equal then @@ -428,10 +428,10 @@ fun term_of_atp ctxt (ATP_Problem.THF _) type_enc = if ATP_Problem_Generate.is_type_enc_higher_order type_enc then K (term_of_atp_ho ctxt) - else error "Unsupported Isar reconstruction." + else error "Unsupported Isar reconstruction" | term_of_atp ctxt _ type_enc = if not (ATP_Problem_Generate.is_type_enc_higher_order type_enc) then term_of_atp_fo ctxt - else error "Unsupported Isar reconstruction." + else error "Unsupported Isar reconstruction" fun term_of_atom ctxt format type_enc textual sym_tab pos (u as ATerm ((s, _), _)) = if String.isPrefix class_prefix s then diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/ATP/atp_satallax.ML --- a/src/HOL/Tools/ATP/atp_satallax.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/ATP/atp_satallax.ML Sun Aug 14 12:26:09 2016 +0200 @@ -122,7 +122,7 @@ group_by_pair new_goals generated_assumptions end else - raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction.") + raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction") end fun to_satallax_step (((id, role), formula), (SOME (_,((rule, l), used_rules)))) = let diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sun Aug 14 12:26:09 2016 +0200 @@ -139,7 +139,7 @@ val extend = I fun merge data : T = Symtab.merge (eq_snd (op =)) data - handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") + handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name) ) fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000) @@ -640,7 +640,7 @@ (warning (case extract_known_atp_failure known_perl_failures output of SOME failure => string_of_atp_failure failure - | NONE => trim_line output ^ "."); []))) () + | NONE => trim_line output); []))) () handle Timeout.TIMEOUT _ => [] fun find_remote_system name [] systems = @@ -658,11 +658,11 @@ fun the_remote_system name versions = (case get_remote_system name versions of (SOME sys, _) => sys - | (NONE, []) => error "SystemOnTPTP is not available." + | (NONE, []) => error "SystemOnTPTP is currently not available" | (NONE, syss) => (case syss |> filter_out (String.isPrefix "%") |> filter_out (curry (op =) "") of - [] => error "SystemOnTPTP is currently not available." - | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg ^ ".") + [] => error "SystemOnTPTP is currently not available" + | [msg] => error ("SystemOnTPTP is currently not available: " ^ msg) | syss => error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n(Available systems: " ^ commas_quote syss ^ ".)"))) @@ -744,11 +744,11 @@ fun add_atp (name, config) thy = Data.map (Symtab.update_new (name, (config, stamp ()))) thy - handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".") + handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name) fun get_atp thy name = fst (the (Symtab.lookup (Data.get thy) name)) - handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") + handle Option.Option => error ("Unknown ATP: " ^ name) val supported_atps = Symtab.keys o Data.get diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/Sledgehammer/async_manager_legacy.ML --- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Sun Aug 14 12:26:09 2016 +0200 @@ -123,7 +123,7 @@ (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action |> these - |> List.app (unregister (false, "Timed out.")); + |> List.app (unregister (false, "Timed out")); print_new_messages (); (* give threads some time to respond to interrupt *) OS.Process.sleep min_wait_time) diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Aug 14 12:26:09 2016 +0200 @@ -135,8 +135,8 @@ |> filter_used_facts false used_facts |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |> commas - |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ - " proof (of " ^ string_of_int (length facts) ^ "): ") "." + |> curry (op ^) ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ + " proof (of " ^ string_of_int (length facts) ^ "): ") |> writeln fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) = @@ -206,7 +206,7 @@ not (is_prover_installed ctxt name) then () else - error ("Unexpected outcome: " ^ quote outcome_code ^ ".") + error ("Unexpected outcome: " ^ quote outcome_code) in (outcome_code, message) end in if mode = Auto_Try then @@ -228,11 +228,11 @@ fun string_of_facts facts = "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ": " ^ - (facts |> map (fst o fst) |> space_implode " ") ^ "." + (facts |> map (fst o fst) |> space_implode " ") fun string_of_factss factss = if forall (null o snd) factss then - "Found no relevant facts." + "Found no relevant facts" else cat_lines (map (fn (filter, facts) => (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss) @@ -240,7 +240,7 @@ fun run_sledgehammer (params as {verbose, spy, provers, max_facts, ...}) mode writeln_result i (fact_override as {only, ...}) state = if null provers then - error "No prover is set." + error "No prover is set" else (case subgoal_count state of 0 => (error "No subgoal!"; (false, (noneN, []))) @@ -269,7 +269,7 @@ nearly_all_facts ctxt ho_atp fact_override keywords css chained hyp_ts concl_t val _ = (case find_first (not o is_prover_supported ctxt) provers of - SOME name => error ("No such prover: " ^ name ^ ".") + SOME name => error ("No such prover: " ^ name) | NONE => ()) val _ = print "Sledgehammering..." val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode")) @@ -319,7 +319,7 @@ in launch_provers () handle Timeout.TIMEOUT _ => - (print "Sledgehammer ran out of time."; (unknownN, [])) + (print "Sledgehammer ran out of time"; (unknownN, [])) end |> `(fn (outcome_code, _) => outcome_code = someN)) diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Sun Aug 14 12:26:09 2016 +0200 @@ -112,7 +112,7 @@ if value <> ["false"] then param' else - error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ").") + error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ")") | NONE => (case AList.lookup (op =) negated_alias_params name of SOME name' => (name', @@ -144,9 +144,9 @@ else if is_some (Int.fromString name) then ("max_facts", [name]) else - error ("Unknown parameter: " ^ quote name ^ ".") + error ("Unknown parameter: " ^ quote name) else - error ("Unknown parameter: " ^ quote name ^ ".")) + error ("Unknown parameter: " ^ quote name)) (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are read correctly. *) @@ -218,14 +218,14 @@ | SOME s => (case Int.fromString s of SOME n => n - | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value."))) + | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value"))) fun lookup_real name = (case lookup name of NONE => 0.0 | SOME s => (case Real.fromString s of SOME n => n - | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value."))) + | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value"))) fun lookup_real_pair name = (case lookup name of NONE => (0.0, 0.0) @@ -341,7 +341,7 @@ else if subcommand = refresh_tptpN then refresh_systems_on_tptp () else - error ("Unknown subcommand: " ^ quote subcommand ^ ".") + error ("Unknown subcommand: " ^ quote subcommand) end fun string_of_raw_param (key, values) = diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Aug 14 12:26:09 2016 +0200 @@ -454,7 +454,7 @@ SOME s => s | NONE => one_line_proof_text ctxt 0 one_line_params ^ - (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else "")) + (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else "")) end fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) = diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Aug 14 12:26:09 2016 +0200 @@ -149,7 +149,7 @@ | "knn_ext" => SOME MaSh_kNN_Ext | "none" => NONE | "" => NONE - | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm ^ "."); NONE)) + | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm); NONE)) val is_mash_enabled = is_some o mash_algorithm val the_mash_algorithm = the_default MaSh_NB_kNN o mash_algorithm @@ -1038,7 +1038,7 @@ if verbose andalso auto_level = 0 then writeln ("MaSh: " ^ quote prover ^ " on " ^ quote name ^ " with " ^ string_of_int num_isar_deps ^ " + " ^ string_of_int (length facts - num_isar_deps) ^ - " facts.") + " facts") else (); (case run_prover_for_mash ctxt params prover name facts goal of @@ -1046,7 +1046,7 @@ (if verbose andalso auto_level = 0 then let val num_facts = length used_facts in writeln ("Found proof with " ^ string_of_int num_facts ^ " fact" ^ - plural_s num_facts ^ ".") + plural_s num_facts) end else (); @@ -1237,7 +1237,7 @@ |> apply2 (map fact_of_raw_fact) end -fun mash_unlearn () = (clear_state (); writeln "Reset MaSh.") +fun mash_unlearn () = (clear_state (); writeln "Reset MaSh") fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (accum as (access_G, (fact_xtab, feat_xtab))) = @@ -1336,9 +1336,9 @@ in if no_new_facts andalso not run_prover then if auto_level < 2 then - "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn." ^ + "No new " ^ (if run_prover then "automatic" else "Isar") ^ " proofs to learn" ^ (if auto_level = 0 andalso not run_prover then - "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover." + "\n\nHint: Try " ^ sendback learn_proverN ^ " to learn from an automatic prover" else "") else @@ -1393,7 +1393,7 @@ let val num_proofs = length learns + length relearns in writeln ("Learned " ^ string_of_int num_proofs ^ " " ^ (if run_prover then "automatic" else "Isar") ^ " proof" ^ - plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout ^ ".") + plural_s num_proofs ^ " in the last " ^ string_of_time commit_timeout) end else ()) @@ -1483,7 +1483,7 @@ "Learned " ^ string_of_int num_new_facts ^ " fact" ^ plural_s num_new_facts ^ " and " ^ string_of_int num_nontrivial ^ " nontrivial " ^ (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s num_nontrivial ^ - (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "") ^ "." + (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer) else "") else "" end @@ -1508,8 +1508,8 @@ plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ " timeout: " ^ string_of_time timeout ^ ").\n\nCollecting Isar proofs first..."); learn 1 false; - writeln "Now collecting automatic proofs. This may take several hours. You \ - \can safely stop the learning process at any point."; + writeln "Now collecting automatic proofs\n\ + \This may take several hours; you can safely stop the learning process at any point"; learn 0 true) else (writeln ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ @@ -1535,7 +1535,7 @@ fun relevant_facts ctxt (params as {verbose, learn, fact_filter, timeout, ...}) prover max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = if not (subset (op =) (the_list fact_filter, fact_filters)) then - error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".") + error ("Unknown fact filter: " ^ quote (the fact_filter)) else if only then [("", map fact_of_raw_fact facts)] else if max_facts <= 0 orelse null facts then @@ -1551,7 +1551,7 @@ (if verbose then writeln ("Started MaShing through " ^ (if exact then "" else "at least ") ^ string_of_int min_num_facts_to_learn ^ - " fact" ^ plural_s min_num_facts_to_learn ^ " in the background.") + " fact" ^ plural_s min_num_facts_to_learn ^ " in the background") else ()); launch_thread timeout diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Sun Aug 14 12:26:09 2016 +0200 @@ -181,7 +181,7 @@ fun try_command_line banner play command = let val s = string_of_play_outcome play in banner ^ ": " ^ Active.sendback_markup_command command ^ - (s |> s <> "" ? enclose " (" ")") ^ "." + (s |> s <> "" ? enclose " (" ")") end fun one_line_proof_text ctxt num_chained @@ -189,7 +189,7 @@ let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in map fst extra |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained - |> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "." + |> (if play = Play_Failed then prefix "One-line proof reconstruction failed: " else try_command_line banner play) end diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Sun Aug 14 12:26:09 2016 +0200 @@ -194,7 +194,7 @@ sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt) |> List.partition (String.isPrefix remote_prefix) in - writeln ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".") + writeln ("Supported provers: " ^ commas (local_provers @ remote_provers)) end end; diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Sun Aug 14 12:26:09 2016 +0200 @@ -161,7 +161,7 @@ else if File.exists (Path.explode dest_dir) then Path.append (Path.explode dest_dir) problem_file_name else - error ("No such directory: " ^ quote dest_dir ^ ".") + error ("No such directory: " ^ quote dest_dir) val exec = exec full_proofs val command0 = (case find_first (fn var => getenv var <> "") (fst exec) of @@ -176,9 +176,9 @@ in (case find_first File.exists paths of SOME path => path - | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".")) + | NONE => error ("Bad executable: " ^ Path.print (hd paths))) end - | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set.")) + | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set")) fun split_time s = let diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Sun Aug 14 12:26:09 2016 +0200 @@ -58,14 +58,14 @@ else if is_smt_prover ctxt name then SMT_Solver.default_max_relevant ctxt name else - error ("No such prover: " ^ name ^ ".") + error ("No such prover: " ^ name) end fun get_prover ctxt mode name = let val thy = Proof_Context.theory_of ctxt in if is_atp thy name then run_atp mode name else if is_smt_prover ctxt name then run_smt_solver mode name - else error ("No such prover: " ^ name ^ ".") + else error ("No such prover: " ^ name) end (* wrapper for calling external prover *) @@ -116,7 +116,7 @@ | NONE => "Found proof" ^ (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^ - " (" ^ string_of_time run_time ^ ").")); + " (" ^ string_of_time run_time ^ ")")); result end @@ -206,7 +206,7 @@ fun test timeout non_chained = test_facts params silent prover timeout i n state goal (chained @ non_chained) in - (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name ^ "."); + (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name); (case test timeout non_chained of result as {outcome = NONE, used_facts, run_time, ...} => let @@ -222,14 +222,14 @@ ["Minimized to " ^ n_facts (map fst min_facts)] ^ (case length chained of 0 => "" - | n => " (plus " ^ string_of_int n ^ " chained)") ^ "."); + | n => " (plus " ^ string_of_int n ^ " chained)")); (if learn then do_learn (maps snd min_facts_and_chained) else ()); (SOME min_facts_and_chained, message) end | {outcome = SOME TimedOut, ...} => (NONE, fn _ => "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \ - \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").") + \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\")") | {message, ...} => (NONE, (prefix "Prover error: " o message)))) handle ERROR msg => (NONE, fn _ => "Error: " ^ msg) end diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Sun Aug 14 12:26:09 2016 +0200 @@ -60,7 +60,7 @@ | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) = (case AList.lookup (op =) smt_failures code of SOME failure => failure - | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ ".")) + | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code)) | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s diff -r 94a89b95b871 -r 1bc4bc2c9fd1 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Aug 14 12:26:09 2016 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Aug 14 12:26:09 2016 +0200 @@ -61,7 +61,7 @@ handle Option.Option => let val ss = map quote ((option ? cons "smart") ["true", "false"]) in error ("Parameter " ^ quote name ^ " must be assigned " ^ - space_implode " " (serial_commas "or" ss) ^ ".") + space_implode " " (serial_commas "or" ss)) end val has_junk = @@ -71,7 +71,7 @@ let val secs = if has_junk s then NONE else Real.fromString s in if is_none secs orelse the secs < 0.0 then error ("Parameter " ^ quote name ^ " must be assigned a nonnegative number of seconds \ - \(e.g., \"60\", \"0.5\") or \"none\".") + \(e.g., \"60\", \"0.5\") or \"none\"") else seconds (the secs) end