src/Pure/Isar/proof.ML

   val assert_forward_or_chain: state -> state
   val assert_backward: state -> state
   val assert_no_chain: state -> state
   val enter_forward: state -> state
   val verbose: bool ref
-  val print_state: int -> state -> unit
+  val pretty_state: int -> state -> Pretty.T list
   val pretty_goals: bool -> state -> Pretty.T list
   val level: state -> int
   type method
   val method: (thm list -> tactic) -> method
   val method_cases: (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> method

 fun close_block (state as State (_, node :: nodes)) = State (node, nodes)
   | close_block state = raise STATE ("Unbalanced block parentheses", state);
 
 
 
-(** print_state **)
+(** pretty_state **)
 
 val verbose = ProofContext.verbose;
 
 fun pretty_goals_local ctxt = Display.pretty_goals_aux
   (ProofContext.pretty_sort ctxt, ProofContext.pretty_typ ctxt, ProofContext.pretty_term ctxt);
 
 fun pretty_facts _ _ None = []
   | pretty_facts s ctxt (Some ths) =
       [Pretty.big_list (s ^ "this:") (map (ProofContext.pretty_thm ctxt) ths), Pretty.str ""];
 
-fun print_state nr (state as State (Node {context = ctxt, facts, mode, goal = _}, nodes)) =
+fun pretty_state nr (state as State (Node {context = ctxt, facts, mode, goal = _}, nodes)) =
   let
     val ref (_, _, begin_goal) = Display.current_goals_markers;
 
     fun levels_up 0 = ""
       | levels_up 1 = ", 1 level up"

      (if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @
      (if ! verbose orelse mode = Forward then
        (pretty_facts "" ctxt facts @ prt_goal (find_goal state))
       else if mode = ForwardChain then pretty_facts "picking " ctxt facts
       else prt_goal (find_goal state))
-  in Pretty.writeln (Pretty.chunks prts) end;
+  in prts end;
 
 fun pretty_goals main state =
   let val (ctxt, (_, ((_, (_, thm)), _))) = find_goal state
   in pretty_goals_local ctxt "" (false, main) (! Display.goals_limit) thm end;