# HG changeset patch # User wenzelm # Date 1183826354 -7200 # Node ID 55e579ef85aaa227f6c7ce60b27a11363e280b4f # Parent f25b1566f7b5cf5d95d73c5b6cc4f84be4a24170 pretty_goals_aux: subgoal markup; print_goals etc.: moved old version to old_goals.ML, removed hooks; tuned; diff -r f25b1566f7b5 -r 55e579ef85aa src/Pure/display.ML --- a/src/Pure/display.ML Sat Jul 07 18:39:12 2007 +0200 +++ b/src/Pure/display.ML Sat Jul 07 18:39:14 2007 +0200 @@ -40,13 +40,9 @@ val pretty_ctyp: ctyp -> Pretty.T val pretty_cterm: cterm -> Pretty.T val pretty_full_theory: bool -> theory -> Pretty.T list - val pretty_goals_aux: Pretty.pp -> string -> bool * bool -> int -> thm -> Pretty.T list + val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list val pretty_goals: int -> thm -> Pretty.T list val print_goals: int -> thm -> unit - val current_goals_markers: (string * string * string) ref - val pretty_current_goals: int -> int -> thm -> Pretty.T list - val print_current_goals_default: int -> int -> thm -> unit - val print_current_goals_fn: (int -> int -> thm -> unit) ref end; structure Display: DISPLAY = @@ -293,7 +289,7 @@ in -fun pretty_goals_aux pp begin_goal (msg, main) maxgoals state = +fun pretty_goals_aux pp markup (msg, main) maxgoals state = let fun prt_atoms prt prtT (X, xs) = Pretty.block [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::", @@ -313,8 +309,8 @@ fun pretty_list _ _ [] = [] | pretty_list name prt lst = [Pretty.big_list name (map prt lst)]; - fun pretty_subgoal (n, A) = Pretty.blk (0, - [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), Pretty.term pp A]); + fun pretty_subgoal (n, A) = Pretty.markup markup + [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A]; fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As); val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp); @@ -347,38 +343,14 @@ (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts) end; -fun pretty_goals_marker bg n th = - pretty_goals_aux (Sign.pp (Thm.theory_of_thm th)) bg (true, true) n th; +fun pretty_goals n th = + pretty_goals_aux (Sign.pp (Thm.theory_of_thm th)) Markup.none (true, true) n th; -val pretty_goals = pretty_goals_marker ""; -val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals_marker ""; +val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals; end; -(* print_current_goals *) - -val current_goals_markers = ref ("", "", ""); - -fun pretty_current_goals n m th = - let - val ref (begin_state, end_state, begin_goal) = current_goals_markers; - val ngoals = nprems_of th; - in - (if begin_state = "" then [] else [Pretty.str begin_state]) @ - [Pretty.str ("Level " ^ string_of_int n ^ - (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^ - (if ngoals <> 1 then "s" else "") ^ ")" - else ""))] @ - pretty_goals_marker begin_goal m th @ - (if end_state = "" then [] else [Pretty.str end_state]) - end; - -fun print_current_goals_default n m th = - Pretty.writeln (Pretty.chunks (pretty_current_goals n m th)); - -val print_current_goals_fn = ref print_current_goals_default; - end; structure BasicDisplay: BASIC_DISPLAY = Display;