src/Pure/old_goals.ML
changeset 23635 e31a814c080a
parent 23239 3648e97da60b
child 25685 c36e10812ae4
     1.1 --- a/src/Pure/old_goals.ML	Sat Jul 07 18:39:14 2007 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Sat Jul 07 18:39:15 2007 +0200
     1.3 @@ -14,8 +14,6 @@
     1.4    val premises: unit -> thm list
     1.5    val prove_goal: theory -> string -> (thm list -> tactic list) -> thm
     1.6    val prove_goalw: theory -> thm list -> string -> (thm list -> tactic list) -> thm
     1.7 -  val disable_pr: unit -> unit
     1.8 -  val enable_pr: unit -> unit
     1.9    val topthm: unit -> thm
    1.10    val result: unit -> thm
    1.11    val uresult: unit -> thm
    1.12 @@ -271,15 +269,20 @@
    1.13    | pop (pair::pairs) = (pair,pairs);
    1.14  
    1.15  
    1.16 -(* Print a level of the goal stack -- subject to quiet mode *)
    1.17 -
    1.18 -val quiet = ref false;
    1.19 -fun disable_pr () = quiet := true;
    1.20 -fun enable_pr () = quiet := false;
    1.21 +(* Print a level of the goal stack *)
    1.22  
    1.23  fun print_top ((th, _), pairs) =
    1.24 -  if ! quiet then ()
    1.25 -  else ! Display.print_current_goals_fn (length pairs) (! goals_limit) th;
    1.26 +  let
    1.27 +    val n = length pairs;
    1.28 +    val m = (! goals_limit);
    1.29 +    val ngoals = nprems_of th;
    1.30 +  in
    1.31 +    [Pretty.str ("Level " ^ string_of_int n ^
    1.32 +      (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
    1.33 +        (if ngoals <> 1 then "s" else "") ^ ")"
    1.34 +      else ""))] @
    1.35 +    Display.pretty_goals m th
    1.36 +  end |> Pretty.chunks |> Pretty.writeln;
    1.37  
    1.38  (*Printing can raise exceptions, so the assignment occurs last.
    1.39    Can do   setstate[(st,Seq.empty)]  to set st as the state.  *)
    1.40 @@ -334,8 +337,8 @@
    1.41    end;
    1.42  
    1.43  (*Print the given level of the proof; prlev ~1 prints previous level*)
    1.44 -fun prlev n = (enable_pr (); apply_fun (print_top o pop o (chop_level n)));
    1.45 -fun pr () = (enable_pr (); apply_fun print_top);
    1.46 +fun prlev n = apply_fun (print_top o pop o (chop_level n));
    1.47 +fun pr () = apply_fun print_top;
    1.48  
    1.49  (*Set goals_limit and print again*)
    1.50  fun prlim n = (goals_limit:=n; pr());