--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Sep 21 21:46:14 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Sep 21 23:22:11 2015 +0200
@@ -118,7 +118,7 @@
end
fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, minimize, timeout,
- preplay_timeout, expect, ...}) mode output_result only learn
+ preplay_timeout, expect, ...}) mode writeln_result only learn
{comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
let
val ctxt = Proof.context_of state
@@ -230,8 +230,8 @@
val outcome =
if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else ""
val _ =
- if outcome <> "" andalso is_some output_result then
- the output_result outcome
+ if outcome <> "" andalso is_some writeln_result then
+ the writeln_result outcome
else
outcome
|> Async_Manager_Legacy.break_into_chunks
@@ -258,7 +258,7 @@
(if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss)
fun run_sledgehammer (params as {verbose, spy, blocking, provers, max_facts, ...}) mode
- output_result i (fact_override as {only, ...}) state =
+ writeln_result i (fact_override as {only, ...}) state =
if null provers then
error "No prover is set."
else
@@ -269,7 +269,7 @@
let
val _ = Proof.assert_backward state
val print =
- if mode = Normal andalso is_none output_result then writeln else K ()
+ if mode = Normal andalso is_none writeln_result then writeln else K ()
val ctxt = Proof.context_of state
val keywords = Thy_Header.get_keywords' ctxt
val {facts = chained, goal, ...} = Proof.goal state
@@ -315,7 +315,7 @@
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
factss = factss}
val learn = mash_learn_proof ctxt params (Thm.prop_of goal) all_facts
- val launch = launch_prover params mode output_result only learn
+ val launch = launch_prover params mode writeln_result only learn
in
if mode = Auto_Try then
(unknownN, [])
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Sep 21 21:46:14 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Sep 21 23:22:11 2015 +0200
@@ -299,7 +299,7 @@
val default_learn_prover_timeout = 2.0
-fun hammer_away override_params output_result subcommand opt_i fact_override state0 =
+fun hammer_away override_params writeln_result subcommand opt_i fact_override state0 =
let
(* We generally want chained facts to be picked up by the relevance filter, because it can then
give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs,
@@ -328,7 +328,7 @@
if subcommand = runN then
let val i = the_default 1 opt_i in
ignore (run_sledgehammer
- (get_params Normal thy override_params) Normal output_result i fact_override state)
+ (get_params Normal thy override_params) Normal writeln_result i fact_override state)
end
else if subcommand = messagesN then
messages opt_i
@@ -408,20 +408,21 @@
val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))
val _ =
- Query_Operation.register {name = sledgehammerN, pri = 0} (fn {state = st, args, output_result} =>
- (case try Toplevel.proof_of st of
- SOME state =>
- let
- val [provers_arg, isar_proofs_arg, try0_arg] = args
- val override_params =
- ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
- [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]),
- ("try0", [try0_arg]),
- ("blocking", ["true"]),
- ("debug", ["false"]),
- ("verbose", ["false"]),
- ("overlord", ["false"])]);
- in hammer_away override_params (SOME output_result) runN NONE no_fact_override state end
- | NONE => error "Unknown proof context"))
+ Query_Operation.register {name = sledgehammerN, pri = 0}
+ (fn {state = st, args, writeln_result, ...} =>
+ (case try Toplevel.proof_of st of
+ SOME state =>
+ let
+ val [provers_arg, isar_proofs_arg, try0_arg] = args
+ val override_params =
+ ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
+ [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]),
+ ("try0", [try0_arg]),
+ ("blocking", ["true"]),
+ ("debug", ["false"]),
+ ("verbose", ["false"]),
+ ("overlord", ["false"])]);
+ in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end
+ | NONE => error "Unknown proof context"))
end;
--- a/src/Pure/PIDE/query_operation.ML Mon Sep 21 21:46:14 2015 +0200
+++ b/src/Pure/PIDE/query_operation.ML Mon Sep 21 23:22:11 2015 +0200
@@ -8,7 +8,8 @@
signature QUERY_OPERATION =
sig
val register: {name: string, pri: int} ->
- ({state: Toplevel.state, args: string list, output_result: string -> unit} -> unit) -> unit
+ ({state: Toplevel.state, args: string list,
+ output_result: string -> unit, writeln_result: string -> unit} -> unit) -> unit
end;
structure Query_Operation: QUERY_OPERATION =
@@ -20,13 +21,16 @@
SOME {delay = NONE, pri = pri, persistent = false, strict = false,
print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
let
- fun result s = Output.result [(Markup.instanceN, instance)] [s];
- fun status m = result (Markup.markup_only m);
- fun output_result s = result (Markup.markup Markup.writeln s);
- fun toplevel_error exn = result (Markup.markup Markup.error (Runtime.exn_message exn));
+ fun output_result s = Output.result [(Markup.instanceN, instance)] [s];
+ fun status m = output_result (Markup.markup_only m);
+ fun writeln_result s = output_result (Markup.markup Markup.writeln s);
+ fun toplevel_error exn =
+ output_result (Markup.markup Markup.error (Runtime.exn_message exn));
val _ = status Markup.running;
- fun run () = f {state = state, args = args, output_result = output_result};
+ fun run () =
+ f {state = state, args = args, output_result = output_result,
+ writeln_result = writeln_result};
val _ =
(case Exn.capture (*sic!*) (restore_attributes run) () of
Exn.Res () => ()
--- a/src/Pure/Tools/find_consts.ML Mon Sep 21 21:46:14 2015 +0200
+++ b/src/Pure/Tools/find_consts.ML Mon Sep 21 23:22:11 2015 +0200
@@ -165,13 +165,13 @@
val _ =
Query_Operation.register {name = "find_consts", pri = Task_Queue.urgent_pri}
- (fn {state, args, output_result} =>
+ (fn {state, args, writeln_result, ...} =>
(case try Toplevel.context_of state of
SOME ctxt =>
let
val [query_arg] = args;
val query = read_query Position.none query_arg;
- in output_result (Pretty.string_of (pretty_consts ctxt query)) end
+ in writeln_result (Pretty.string_of (pretty_consts ctxt query)) end
| NONE => error "Unknown context"));
end;
--- a/src/Pure/Tools/find_theorems.ML Mon Sep 21 21:46:14 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML Mon Sep 21 23:22:11 2015 +0200
@@ -551,7 +551,7 @@
val _ =
Query_Operation.register {name = "find_theorems", pri = Task_Queue.urgent_pri}
- (fn {state = st, args, output_result} =>
+ (fn {state = st, args, writeln_result, ...} =>
if can Toplevel.context_of st then
let
val [limit_arg, allow_dups_arg, query_arg] = args;
@@ -559,7 +559,7 @@
val opt_limit = Int.fromString limit_arg;
val rem_dups = allow_dups_arg = "false";
val criteria = read_query Position.none query_arg;
- in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
+ in writeln_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
else error "Unknown context");
end;
--- a/src/Pure/Tools/print_operation.ML Mon Sep 21 21:46:14 2015 +0200
+++ b/src/Pure/Tools/print_operation.ML Mon Sep 21 23:22:11 2015 +0200
@@ -46,7 +46,7 @@
val _ =
Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri}
- (fn {state, args, output_result} =>
+ (fn {state, args, writeln_result, ...} =>
let
val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
fun err s = Pretty.mark_str (Markup.bad, s);
@@ -54,7 +54,7 @@
(case AList.lookup (op =) (Synchronized.value print_operations) name of
SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
| NONE => [err ("Unknown print operation: " ^ quote name)]);
- in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
+ in writeln_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
end;