improved print_state;
authorwenzelm
Tue Jun 01 19:46:52 1999 +0200 (1999-06-01)
changeset 6756fe6eb161df3e
parent 6755 9f830d69a46d
child 6757 604d1445c9f3
improved print_state;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Tue Jun 01 18:12:45 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Jun 01 19:46:52 1999 +0200
     1.3 @@ -260,19 +260,20 @@
     1.4  
     1.5  val verbose = ProofContext.verbose;
     1.6  
     1.7 +fun print_facts _ None = ()
     1.8 +  | print_facts s (Some ths) =
     1.9 +      Pretty.writeln (Pretty.big_list (s ^ " facts:") (map Display.pretty_thm ths));
    1.10 +
    1.11  fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) =
    1.12    let
    1.13      val ref (_, _, begin_goal) = Goals.current_goals_markers;
    1.14  
    1.15 -    fun print_facts None = ()
    1.16 -      | print_facts (Some ths) =
    1.17 -          Pretty.writeln (Pretty.big_list "Current facts:" (map Display.pretty_thm ths));
    1.18 -
    1.19      fun levels_up 0 = ""
    1.20        | levels_up i = " (" ^ string_of_int i ^ " levels up)";
    1.21  
    1.22 -    fun print_goal (i, ((kind, name, _, _), (_, thm))) =
    1.23 -      (writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":");
    1.24 +    fun print_goal (i, ((kind, name, _, _), (goal_facts, thm))) =
    1.25 +      (print_facts "Using" (if null goal_facts then None else Some goal_facts);
    1.26 +        writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":");
    1.27          Locale.print_goals_marker begin_goal (! goals_limit) thm);
    1.28    in
    1.29      writeln ("Nesting level: " ^ string_of_int (length nodes div 2));
    1.30 @@ -282,9 +283,9 @@
    1.31      if ! verbose orelse mode = Forward then
    1.32        (ProofContext.print_context context;
    1.33          writeln "";
    1.34 -        print_facts facts;
    1.35 +        print_facts "Current" facts;
    1.36          print_goal (find_goal 0 state))
    1.37 -    else if mode = ForwardChain then print_facts facts
    1.38 +    else if mode = ForwardChain then print_facts "Picking" facts
    1.39      else print_goal (find_goal 0 state)
    1.40    end;
    1.41