# HG changeset patch
# User wenzelm
# Date 1442870531 -7200
# Node ID dfccf6c06201c5d7e1b7d9cdb63784340b1023f6
# Parent  05d28dc76e5c7d6d9b025a620f1c1a76c23aba7e
clarified markup;
tuned signature;

diff -r 05d28dc76e5c -r dfccf6c06201 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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, [])
diff -r 05d28dc76e5c -r dfccf6c06201 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- 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;
diff -r 05d28dc76e5c -r dfccf6c06201 src/Pure/PIDE/query_operation.ML
--- 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 () => ()
diff -r 05d28dc76e5c -r dfccf6c06201 src/Pure/Tools/find_consts.ML
--- 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;
diff -r 05d28dc76e5c -r dfccf6c06201 src/Pure/Tools/find_theorems.ML
--- 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;
diff -r 05d28dc76e5c -r dfccf6c06201 src/Pure/Tools/print_operation.ML
--- 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;