src/Pure/display.ML
changeset 12418 753054ec8e88
parent 12081 f9735aad76dc
child 12831 a2a3896f9c48
     1.1 --- a/src/Pure/display.ML	Sat Dec 08 14:41:10 2001 +0100
     1.2 +++ b/src/Pure/display.ML	Sat Dec 08 14:41:36 2001 +0100
     1.3 @@ -48,8 +48,9 @@
     1.4    val pretty_goals: int -> thm -> Pretty.T list
     1.5    val print_goals: int -> thm -> unit
     1.6    val current_goals_markers: (string * string * string) ref
     1.7 -  val print_current_goals_default: (int -> int -> thm -> unit)
     1.8 -  val print_current_goals_fn : (int -> int -> thm -> unit) ref
     1.9 +  val pretty_current_goals: int -> int -> thm -> Pretty.T list
    1.10 +  val print_current_goals_default: int -> int -> thm -> unit
    1.11 +  val print_current_goals_fn: (int -> int -> thm -> unit) ref
    1.12  end;
    1.13  
    1.14  structure Display: DISPLAY =
    1.15 @@ -343,8 +344,7 @@
    1.16    end;
    1.17  
    1.18  val pretty_goals = pretty_goals_marker "";
    1.19 -val print_goals_marker = (Pretty.writeln o Pretty.chunks) ooo pretty_goals_marker;
    1.20 -val print_goals = print_goals_marker "";
    1.21 +val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals_marker "";
    1.22  
    1.23  end;
    1.24  
    1.25 @@ -353,20 +353,23 @@
    1.26  
    1.27  val current_goals_markers = ref ("", "", "");
    1.28  
    1.29 -fun print_current_goals_default n max th =
    1.30 +fun pretty_current_goals n m th =
    1.31    let
    1.32      val ref (begin_state, end_state, begin_goal) = current_goals_markers;
    1.33      val ngoals = nprems_of th;
    1.34    in
    1.35 -    if begin_state = "" then () else writeln begin_state;
    1.36 -    writeln ("Level " ^ string_of_int n ^
    1.37 +    (if begin_state = "" then [] else [Pretty.str begin_state]) @
    1.38 +    [Pretty.str ("Level " ^ string_of_int n ^
    1.39        (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
    1.40          (if ngoals <> 1 then "s" else "") ^ ")"
    1.41 -      else ""));
    1.42 -    print_goals_marker begin_goal max th;
    1.43 -    if end_state = "" then () else writeln end_state
    1.44 +      else ""))] @
    1.45 +    pretty_goals_marker begin_goal m th @
    1.46 +    (if end_state = "" then [] else [Pretty.str end_state])
    1.47    end;
    1.48  
    1.49 +fun print_current_goals_default n m th =
    1.50 +  Pretty.writeln (Pretty.chunks (pretty_current_goals n m th));
    1.51 +
    1.52  val print_current_goals_fn = ref print_current_goals_default;
    1.53  
    1.54  end;