src/Pure/Isar/proof_display.ML

   val pretty_goal_facts: Proof.context -> string -> thm list option -> Pretty.T list
   val pretty_goal_inst: Proof.context -> term list list -> thm -> Pretty.T list
   val method_error: string -> Position.T ->
     {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
   val show_results: bool Config.T
-  val print_results: bool -> Position.T -> Proof.context ->
+  val print_results: {interactive: bool, pos: Position.T, proof_state: bool} -> Proof.context ->
     ((string * string) * (string * thm list) list) -> unit
   val print_theorem: Position.T -> Proof.context -> string * thm list -> unit
   val print_consts: bool -> Position.T -> Proof.context ->
     (string * typ -> bool) -> (string * typ) list -> unit
   val markup_extern_label: Position.T -> (Markup.T * xstring) option

   flat o (separate [Pretty.fbrk, Pretty.keyword2 "and", Pretty.str " "]) o
     map (single o Proof_Context.pretty_fact ctxt);
 
 in
 
-fun print_results int pos ctxt ((kind, name), facts) =
-  if kind = "" orelse no_print int ctxt then ()
-  else if name = "" then
-    (Output.state o Pretty.string_of)
-      (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
-        pretty_facts ctxt facts))
-  else
-    (Output.state o Pretty.string_of)
-      (case facts of
-        [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
-          Proof_Context.pretty_fact ctxt fact])
-      | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
-          Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
+fun print_results {interactive, pos, proof_state} ctxt ((kind, name), facts) =
+  let val print = if proof_state then Output.state o Pretty.string_of else Pretty.writeln in
+    if kind = "" orelse no_print interactive ctxt then ()
+    else if name = "" then
+      print
+        (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
+          pretty_facts ctxt facts))
+    else
+      print
+        (case facts of
+          [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
+            Proof_Context.pretty_fact ctxt fact])
+        | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
+            Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]))
+  end;
 
 fun print_theorem pos ctxt fact =
-  print_results true pos ctxt ((Thm.theoremK, ""), [fact]);
+  print_results {interactive = true, pos = pos, proof_state = false}
+    ctxt ((Thm.theoremK, ""), [fact]);
 
 end;
 
 
 (* consts *)

 
 in
 
 fun print_consts int pos ctxt pred cs =
   if null cs orelse no_print int ctxt then ()
-  else Output.state (Pretty.string_of (pretty_consts pos ctxt pred cs));
+  else Pretty.writeln (pretty_consts pos ctxt pred cs);
 
 end;
 
 
 (* position label *)