print results as "state", to avoid intrusion into the source text;
print new local theory (again);
--- a/src/Pure/Isar/obtain.ML Wed May 07 13:25:54 2014 +0200
+++ b/src/Pure/Isar/obtain.ML Wed May 07 13:55:16 2014 +0200
@@ -300,7 +300,7 @@
val goal = Var (("guess", 0), propT);
fun print_result ctxt' (k, [(s, [_, th])]) =
- Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]);
+ Proof_Display.print_results int ctxt' (k, [(s, [th])]);
val before_qed =
Method.primitive_text (fn ctxt =>
Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>
--- a/src/Pure/Isar/proof.ML Wed May 07 13:25:54 2014 +0200
+++ b/src/Pure/Isar/proof.ML Wed May 07 13:55:16 2014 +0200
@@ -1042,7 +1042,7 @@
local
fun gen_have prep_att prepp before_qed after_qed stmt int =
- local_goal (Proof_Display.print_results Markup.state int)
+ local_goal (Proof_Display.print_results int)
prep_att prepp "have" before_qed after_qed stmt;
fun gen_show prep_att prepp before_qed after_qed stmt int state =
@@ -1056,7 +1056,7 @@
fun print_results ctxt res =
if ! testing then ()
- else Proof_Display.print_results Markup.state int ctxt res;
+ else Proof_Display.print_results int ctxt res;
fun print_rule ctxt th =
if ! testing then rule := SOME th
else if int then
--- a/src/Pure/Isar/proof_display.ML Wed May 07 13:25:54 2014 +0200
+++ b/src/Pure/Isar/proof_display.ML Wed May 07 13:55:16 2014 +0200
@@ -22,8 +22,7 @@
val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
val method_error: string -> Position.T ->
{context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
- val print_results: Markup.T -> bool -> Proof.context ->
- ((string * string) * (string * thm list) list) -> unit
+ val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
end
@@ -141,13 +140,13 @@
in
-fun print_results markup do_print ctxt ((kind, name), facts) =
+fun print_results do_print ctxt ((kind, name), facts) =
if not do_print orelse kind = "" then ()
else if name = "" then
- (Output.urgent_message o Pretty.string_of o Pretty.mark markup)
+ (Pretty.writeln o Pretty.mark Markup.state)
(Pretty.block (Pretty.keyword1 kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
else
- (Output.urgent_message o Pretty.string_of o Pretty.mark markup)
+ (Pretty.writeln o Pretty.mark Markup.state)
(case facts of
[fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
Proof_Context.pretty_fact ctxt fact])
@@ -176,7 +175,7 @@
fun print_consts do_print ctxt pred cs =
if not do_print orelse null cs then ()
- else Pretty.writeln (pretty_consts ctxt pred cs);
+ else Pretty.writeln (Pretty.mark Markup.state (pretty_consts ctxt pred cs));
end;
--- a/src/Pure/Isar/specification.ML Wed May 07 13:25:54 2014 +0200
+++ b/src/Pure/Isar/specification.ML Wed May 07 13:55:16 2014 +0200
@@ -301,7 +301,7 @@
|> Attrib.partial_evaluation ctxt'
|> Element.transform_facts (Proof_Context.export_morphism ctxt' lthy);
val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
- val _ = Proof_Display.print_results Markup.empty int lthy' ((kind, ""), res);
+ val _ = Proof_Display.print_results int lthy' ((kind, ""), res);
in (res, lthy') end;
in
@@ -400,12 +400,12 @@
(map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy;
val lthy'' =
if Attrib.is_empty_binding (name, atts) then
- (Proof_Display.print_results Markup.empty int lthy' ((kind, ""), res); lthy')
+ (Proof_Display.print_results int lthy' ((kind, ""), res); lthy')
else
let
val ([(res_name, _)], lthy'') =
Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy';
- val _ = Proof_Display.print_results Markup.empty int lthy' ((kind, res_name), res);
+ val _ = Proof_Display.print_results int lthy' ((kind, res_name), res);
in lthy'' end;
in after_qed results' lthy'' end;
in
--- a/src/Pure/Isar/toplevel.ML Wed May 07 13:25:54 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed May 07 13:55:16 2014 +0200
@@ -409,6 +409,10 @@
let
val lthy = f thy;
val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy);
+ val _ =
+ if begin then
+ Pretty.writeln (Pretty.mark Markup.state (Pretty.chunks (Local_Theory.pretty lthy)))
+ else ();
in Theory (gthy, SOME lthy) end
| _ => raise UNDEF));