pretty_goals_aux: subgoal markup;
authorwenzelm
Sat Jul 07 18:39:14 2007 +0200 (2007-07-07 ago)
changeset 2363455e579ef85aa
parent 23633 f25b1566f7b5
child 23635 e31a814c080a
pretty_goals_aux: subgoal markup;
print_goals etc.: moved old version to old_goals.ML, removed hooks;
tuned;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Sat Jul 07 18:39:12 2007 +0200
     1.2 +++ b/src/Pure/display.ML	Sat Jul 07 18:39:14 2007 +0200
     1.3 @@ -40,13 +40,9 @@
     1.4    val pretty_ctyp: ctyp -> Pretty.T
     1.5    val pretty_cterm: cterm -> Pretty.T
     1.6    val pretty_full_theory: bool -> theory -> Pretty.T list
     1.7 -  val pretty_goals_aux: Pretty.pp -> string -> bool * bool -> int -> thm -> Pretty.T list
     1.8 +  val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
     1.9    val pretty_goals: int -> thm -> Pretty.T list
    1.10    val print_goals: int -> thm -> unit
    1.11 -  val current_goals_markers: (string * string * string) ref
    1.12 -  val pretty_current_goals: int -> int -> thm -> Pretty.T list
    1.13 -  val print_current_goals_default: int -> int -> thm -> unit
    1.14 -  val print_current_goals_fn: (int -> int -> thm -> unit) ref
    1.15  end;
    1.16  
    1.17  structure Display: DISPLAY =
    1.18 @@ -293,7 +289,7 @@
    1.19  
    1.20  in
    1.21  
    1.22 -fun pretty_goals_aux pp begin_goal (msg, main) maxgoals state =
    1.23 +fun pretty_goals_aux pp markup (msg, main) maxgoals state =
    1.24    let
    1.25      fun prt_atoms prt prtT (X, xs) = Pretty.block
    1.26        [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
    1.27 @@ -313,8 +309,8 @@
    1.28      fun pretty_list _ _ [] = []
    1.29        | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
    1.30  
    1.31 -    fun pretty_subgoal (n, A) = Pretty.blk (0,
    1.32 -     [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), Pretty.term pp A]);
    1.33 +    fun pretty_subgoal (n, A) = Pretty.markup markup
    1.34 +      [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A];
    1.35      fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
    1.36  
    1.37      val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp);
    1.38 @@ -347,38 +343,14 @@
    1.39     (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
    1.40    end;
    1.41  
    1.42 -fun pretty_goals_marker bg n th =
    1.43 -  pretty_goals_aux (Sign.pp (Thm.theory_of_thm th)) bg (true, true) n th;
    1.44 +fun pretty_goals n th =
    1.45 +  pretty_goals_aux (Sign.pp (Thm.theory_of_thm th)) Markup.none (true, true) n th;
    1.46  
    1.47 -val pretty_goals = pretty_goals_marker "";
    1.48 -val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals_marker "";
    1.49 +val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
    1.50  
    1.51  end;
    1.52  
    1.53  
    1.54 -(* print_current_goals *)
    1.55 -
    1.56 -val current_goals_markers = ref ("", "", "");
    1.57 -
    1.58 -fun pretty_current_goals n m th =
    1.59 -  let
    1.60 -    val ref (begin_state, end_state, begin_goal) = current_goals_markers;
    1.61 -    val ngoals = nprems_of th;
    1.62 -  in
    1.63 -    (if begin_state = "" then [] else [Pretty.str begin_state]) @
    1.64 -    [Pretty.str ("Level " ^ string_of_int n ^
    1.65 -      (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
    1.66 -        (if ngoals <> 1 then "s" else "") ^ ")"
    1.67 -      else ""))] @
    1.68 -    pretty_goals_marker begin_goal m th @
    1.69 -    (if end_state = "" then [] else [Pretty.str end_state])
    1.70 -  end;
    1.71 -
    1.72 -fun print_current_goals_default n m th =
    1.73 -  Pretty.writeln (Pretty.chunks (pretty_current_goals n m th));
    1.74 -
    1.75 -val print_current_goals_fn = ref print_current_goals_default;
    1.76 -
    1.77  end;
    1.78  
    1.79  structure BasicDisplay: BASIC_DISPLAY = Display;