clarified markup;
authorwenzelm
Mon Sep 21 23:22:11 2015 +0200 (2015-09-21)
changeset 61223dfccf6c06201
parent 61222 05d28dc76e5c
child 61224 759b5299a9f2
clarified markup;
tuned signature;
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/Pure/PIDE/query_operation.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
src/Pure/Tools/print_operation.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Sep 21 21:46:14 2015 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Sep 21 23:22:11 2015 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4    end
     1.5  
     1.6  fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, minimize, timeout,
     1.7 -      preplay_timeout, expect, ...}) mode output_result only learn
     1.8 +      preplay_timeout, expect, ...}) mode writeln_result only learn
     1.9      {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
    1.10    let
    1.11      val ctxt = Proof.context_of state
    1.12 @@ -230,8 +230,8 @@
    1.13          val outcome =
    1.14            if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else ""
    1.15          val _ =
    1.16 -          if outcome <> "" andalso is_some output_result then
    1.17 -            the output_result outcome
    1.18 +          if outcome <> "" andalso is_some writeln_result then
    1.19 +            the writeln_result outcome
    1.20            else
    1.21              outcome
    1.22              |> Async_Manager_Legacy.break_into_chunks
    1.23 @@ -258,7 +258,7 @@
    1.24        (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss)
    1.25  
    1.26  fun run_sledgehammer (params as {verbose, spy, blocking, provers, max_facts, ...}) mode
    1.27 -    output_result i (fact_override as {only, ...}) state =
    1.28 +    writeln_result i (fact_override as {only, ...}) state =
    1.29    if null provers then
    1.30      error "No prover is set."
    1.31    else
    1.32 @@ -269,7 +269,7 @@
    1.33        let
    1.34          val _ = Proof.assert_backward state
    1.35          val print =
    1.36 -          if mode = Normal andalso is_none output_result then writeln else K ()
    1.37 +          if mode = Normal andalso is_none writeln_result then writeln else K ()
    1.38          val ctxt = Proof.context_of state
    1.39          val keywords = Thy_Header.get_keywords' ctxt
    1.40          val {facts = chained, goal, ...} = Proof.goal state
    1.41 @@ -315,7 +315,7 @@
    1.42                {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
    1.43                 factss = factss}
    1.44              val learn = mash_learn_proof ctxt params (Thm.prop_of goal) all_facts
    1.45 -            val launch = launch_prover params mode output_result only learn
    1.46 +            val launch = launch_prover params mode writeln_result only learn
    1.47            in
    1.48              if mode = Auto_Try then
    1.49                (unknownN, [])
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Sep 21 21:46:14 2015 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Sep 21 23:22:11 2015 +0200
     2.3 @@ -299,7 +299,7 @@
     2.4  
     2.5  val default_learn_prover_timeout = 2.0
     2.6  
     2.7 -fun hammer_away override_params output_result subcommand opt_i fact_override state0 =
     2.8 +fun hammer_away override_params writeln_result subcommand opt_i fact_override state0 =
     2.9    let
    2.10      (* We generally want chained facts to be picked up by the relevance filter, because it can then
    2.11         give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs,
    2.12 @@ -328,7 +328,7 @@
    2.13      if subcommand = runN then
    2.14        let val i = the_default 1 opt_i in
    2.15          ignore (run_sledgehammer
    2.16 -          (get_params Normal thy override_params) Normal output_result i fact_override state)
    2.17 +          (get_params Normal thy override_params) Normal writeln_result i fact_override state)
    2.18        end
    2.19      else if subcommand = messagesN then
    2.20        messages opt_i
    2.21 @@ -408,20 +408,21 @@
    2.22  val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))
    2.23  
    2.24  val _ =
    2.25 -  Query_Operation.register {name = sledgehammerN, pri = 0} (fn {state = st, args, output_result} =>
    2.26 -    (case try Toplevel.proof_of st of
    2.27 -      SOME state =>
    2.28 -        let
    2.29 -          val [provers_arg, isar_proofs_arg, try0_arg] = args
    2.30 -          val override_params =
    2.31 -            ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
    2.32 -              [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]),
    2.33 -               ("try0", [try0_arg]),
    2.34 -               ("blocking", ["true"]),
    2.35 -               ("debug", ["false"]),
    2.36 -               ("verbose", ["false"]),
    2.37 -               ("overlord", ["false"])]);
    2.38 -        in hammer_away override_params (SOME output_result) runN NONE no_fact_override state end
    2.39 -    | NONE => error "Unknown proof context"))
    2.40 +  Query_Operation.register {name = sledgehammerN, pri = 0}
    2.41 +    (fn {state = st, args, writeln_result, ...} =>
    2.42 +      (case try Toplevel.proof_of st of
    2.43 +        SOME state =>
    2.44 +          let
    2.45 +            val [provers_arg, isar_proofs_arg, try0_arg] = args
    2.46 +            val override_params =
    2.47 +              ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
    2.48 +                [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]),
    2.49 +                 ("try0", [try0_arg]),
    2.50 +                 ("blocking", ["true"]),
    2.51 +                 ("debug", ["false"]),
    2.52 +                 ("verbose", ["false"]),
    2.53 +                 ("overlord", ["false"])]);
    2.54 +          in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end
    2.55 +      | NONE => error "Unknown proof context"))
    2.56  
    2.57  end;
     3.1 --- a/src/Pure/PIDE/query_operation.ML	Mon Sep 21 21:46:14 2015 +0200
     3.2 +++ b/src/Pure/PIDE/query_operation.ML	Mon Sep 21 23:22:11 2015 +0200
     3.3 @@ -8,7 +8,8 @@
     3.4  signature QUERY_OPERATION =
     3.5  sig
     3.6    val register: {name: string, pri: int} ->
     3.7 -    ({state: Toplevel.state, args: string list, output_result: string -> unit} -> unit) -> unit
     3.8 +    ({state: Toplevel.state, args: string list,
     3.9 +      output_result: string -> unit, writeln_result: string -> unit} -> unit) -> unit
    3.10  end;
    3.11  
    3.12  structure Query_Operation: QUERY_OPERATION =
    3.13 @@ -20,13 +21,16 @@
    3.14        SOME {delay = NONE, pri = pri, persistent = false, strict = false,
    3.15          print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
    3.16            let
    3.17 -            fun result s = Output.result [(Markup.instanceN, instance)] [s];
    3.18 -            fun status m = result (Markup.markup_only m);
    3.19 -            fun output_result s = result (Markup.markup Markup.writeln s);
    3.20 -            fun toplevel_error exn = result (Markup.markup Markup.error (Runtime.exn_message exn));
    3.21 +            fun output_result s = Output.result [(Markup.instanceN, instance)] [s];
    3.22 +            fun status m = output_result (Markup.markup_only m);
    3.23 +            fun writeln_result s = output_result (Markup.markup Markup.writeln s);
    3.24 +            fun toplevel_error exn =
    3.25 +              output_result (Markup.markup Markup.error (Runtime.exn_message exn));
    3.26  
    3.27              val _ = status Markup.running;
    3.28 -            fun run () = f {state = state, args = args, output_result = output_result};
    3.29 +            fun run () =
    3.30 +              f {state = state, args = args, output_result = output_result,
    3.31 +                  writeln_result = writeln_result};
    3.32              val _ =
    3.33                (case Exn.capture (*sic!*) (restore_attributes run) () of
    3.34                  Exn.Res () => ()
     4.1 --- a/src/Pure/Tools/find_consts.ML	Mon Sep 21 21:46:14 2015 +0200
     4.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Sep 21 23:22:11 2015 +0200
     4.3 @@ -165,13 +165,13 @@
     4.4  
     4.5  val _ =
     4.6    Query_Operation.register {name = "find_consts", pri = Task_Queue.urgent_pri}
     4.7 -    (fn {state, args, output_result} =>
     4.8 +    (fn {state, args, writeln_result, ...} =>
     4.9        (case try Toplevel.context_of state of
    4.10          SOME ctxt =>
    4.11            let
    4.12              val [query_arg] = args;
    4.13              val query = read_query Position.none query_arg;
    4.14 -          in output_result (Pretty.string_of (pretty_consts ctxt query)) end
    4.15 +          in writeln_result (Pretty.string_of (pretty_consts ctxt query)) end
    4.16        | NONE => error "Unknown context"));
    4.17  
    4.18  end;
     5.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Sep 21 21:46:14 2015 +0200
     5.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Sep 21 23:22:11 2015 +0200
     5.3 @@ -551,7 +551,7 @@
     5.4  
     5.5  val _ =
     5.6    Query_Operation.register {name = "find_theorems", pri = Task_Queue.urgent_pri}
     5.7 -    (fn {state = st, args, output_result} =>
     5.8 +    (fn {state = st, args, writeln_result, ...} =>
     5.9        if can Toplevel.context_of st then
    5.10          let
    5.11            val [limit_arg, allow_dups_arg, query_arg] = args;
    5.12 @@ -559,7 +559,7 @@
    5.13            val opt_limit = Int.fromString limit_arg;
    5.14            val rem_dups = allow_dups_arg = "false";
    5.15            val criteria = read_query Position.none query_arg;
    5.16 -        in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
    5.17 +        in writeln_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
    5.18        else error "Unknown context");
    5.19  
    5.20  end;
     6.1 --- a/src/Pure/Tools/print_operation.ML	Mon Sep 21 21:46:14 2015 +0200
     6.2 +++ b/src/Pure/Tools/print_operation.ML	Mon Sep 21 23:22:11 2015 +0200
     6.3 @@ -46,7 +46,7 @@
     6.4  
     6.5  val _ =
     6.6    Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri}
     6.7 -    (fn {state, args, output_result} =>
     6.8 +    (fn {state, args, writeln_result, ...} =>
     6.9        let
    6.10          val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
    6.11          fun err s = Pretty.mark_str (Markup.bad, s);
    6.12 @@ -54,7 +54,7 @@
    6.13            (case AList.lookup (op =) (Synchronized.value print_operations) name of
    6.14              SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
    6.15            | NONE => [err ("Unknown print operation: " ^ quote name)]);
    6.16 -      in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
    6.17 +      in writeln_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
    6.18  
    6.19  end;
    6.20