moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
authorwenzelm
Mon Jul 20 21:20:09 2009 +0200 (2009-07-20 ago)
changeset 32089568a23753e3a
parent 32088 2110fcd86efb
child 32090 39acf19e9f3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
load display.ML after assumption.ML, to accomodate proper contextual theorem display;
src/HOL/Tools/Function/lexicographic_order.ML
src/Pure/IsaMakefile
src/Pure/Isar/proof.ML
src/Pure/Proof/reconstruct.ML
src/Pure/ROOT.ML
src/Pure/display.ML
src/Pure/display_goal.ML
src/Pure/goal.ML
src/Pure/old_goals.ML
src/Pure/tctical.ML
     1.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Mon Jul 20 20:03:19 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Mon Jul 20 21:20:09 2009 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4  fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
     1.5  
     1.6  fun pr_goals ctxt st =
     1.7 -    Display.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
     1.8 +    Display_Goal.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
     1.9       |> Pretty.chunks
    1.10       |> Pretty.string_of
    1.11  
     2.1 --- a/src/Pure/IsaMakefile	Mon Jul 20 20:03:19 2009 +0200
     2.2 +++ b/src/Pure/IsaMakefile	Mon Jul 20 21:20:09 2009 +0200
     2.3 @@ -90,13 +90,13 @@
     2.4    Tools/find_theorems.ML Tools/named_thms.ML Tools/xml_syntax.ML	\
     2.5    assumption.ML axclass.ML codegen.ML config.ML conjunction.ML		\
     2.6    consts.ML context.ML context_position.ML conv.ML defs.ML display.ML	\
     2.7 -  drule.ML envir.ML facts.ML goal.ML interpretation.ML item_net.ML	\
     2.8 -  library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML	\
     2.9 -  name.ML net.ML old_goals.ML old_term.ML pattern.ML primitive_defs.ML	\
    2.10 -  proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML		\
    2.11 -  simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML	\
    2.12 -  term_ord.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML	\
    2.13 -  unify.ML variable.ML
    2.14 +  display_goal.ML drule.ML envir.ML facts.ML goal.ML interpretation.ML	\
    2.15 +  item_net.ML library.ML logic.ML meta_simplifier.ML more_thm.ML	\
    2.16 +  morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML	\
    2.17 +  primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML	\
    2.18 +  sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML	\
    2.19 +  term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML		\
    2.20 +  type_infer.ML unify.ML variable.ML
    2.21  	@./mk
    2.22  
    2.23  
     3.1 --- a/src/Pure/Isar/proof.ML	Mon Jul 20 20:03:19 2009 +0200
     3.2 +++ b/src/Pure/Isar/proof.ML	Mon Jul 20 21:20:09 2009 +0200
     3.3 @@ -318,7 +318,7 @@
     3.4  val show_main_goal = ref false;
     3.5  val verbose = ProofContext.verbose;
     3.6  
     3.7 -val pretty_goals_local = Display.pretty_goals_aux o Syntax.pp;
     3.8 +val pretty_goals_local = Display_Goal.pretty_goals_aux o Syntax.pp;
     3.9  
    3.10  fun pretty_facts _ _ NONE = []
    3.11    | pretty_facts s ctxt (SOME ths) =
     4.1 --- a/src/Pure/Proof/reconstruct.ML	Mon Jul 20 20:03:19 2009 +0200
     4.2 +++ b/src/Pure/Proof/reconstruct.ML	Mon Jul 20 21:20:09 2009 +0200
     4.3 @@ -255,7 +255,7 @@
     4.4        let
     4.5          fun search env [] = error ("Unsolvable constraints:\n" ^
     4.6                Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
     4.7 -                Display.pretty_flexpair (Syntax.pp_global thy) (pairself
     4.8 +                Display_Goal.pretty_flexpair (Syntax.pp_global thy) (pairself
     4.9                    (Envir.norm_term bigenv) p)) cs)))
    4.10            | search env ((u, p as (t1, t2), vs)::ps) =
    4.11                if u then
     5.1 --- a/src/Pure/ROOT.ML	Mon Jul 20 20:03:19 2009 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Mon Jul 20 21:20:09 2009 +0200
     5.3 @@ -115,17 +115,18 @@
     5.4  use "more_thm.ML";
     5.5  use "facts.ML";
     5.6  use "pure_thy.ML";
     5.7 -use "display.ML";
     5.8  use "drule.ML";
     5.9  use "morphism.ML";
    5.10  use "variable.ML";
    5.11  use "conv.ML";
    5.12 +use "display_goal.ML";
    5.13  use "tctical.ML";
    5.14  use "search.ML";
    5.15  use "tactic.ML";
    5.16  use "meta_simplifier.ML";
    5.17  use "conjunction.ML";
    5.18  use "assumption.ML";
    5.19 +use "display.ML";
    5.20  use "goal.ML";
    5.21  use "axclass.ML";
    5.22  
     6.1 --- a/src/Pure/display.ML	Mon Jul 20 20:03:19 2009 +0200
     6.2 +++ b/src/Pure/display.ML	Mon Jul 20 21:20:09 2009 +0200
     6.3 @@ -1,22 +1,21 @@
     6.4  (*  Title:      Pure/display.ML
     6.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.6 -    Copyright   1993  University of Cambridge
     6.7 +    Author:     Makarius
     6.8  
     6.9 -Printing of theorems, goals, results etc.
    6.10 +Printing of theorems, results etc.
    6.11  *)
    6.12  
    6.13  signature BASIC_DISPLAY =
    6.14  sig
    6.15    val goals_limit: int ref
    6.16 +  val show_consts: bool ref
    6.17    val show_hyps: bool ref
    6.18    val show_tags: bool ref
    6.19 -  val show_consts: bool ref
    6.20  end;
    6.21  
    6.22  signature DISPLAY =
    6.23  sig
    6.24    include BASIC_DISPLAY
    6.25 -  val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
    6.26    val pretty_thm_aux: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
    6.27      term list -> thm -> Pretty.T
    6.28    val pretty_thm: thm -> Pretty.T
    6.29 @@ -37,27 +36,26 @@
    6.30    val print_cterm: cterm -> unit
    6.31    val print_syntax: theory -> unit
    6.32    val pretty_full_theory: bool -> theory -> Pretty.T list
    6.33 -  val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
    6.34 -  val pretty_goals: int -> thm -> Pretty.T list
    6.35 -  val print_goals: int -> thm -> unit
    6.36  end;
    6.37  
    6.38  structure Display: DISPLAY =
    6.39  struct
    6.40  
    6.41 +(** options **)
    6.42 +
    6.43 +val goals_limit = Display_Goal.goals_limit;
    6.44 +val show_consts = Display_Goal.show_consts;
    6.45 +
    6.46 +val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
    6.47 +val show_tags = ref false;      (*false: suppress tags*)
    6.48 +
    6.49 +
    6.50  
    6.51  (** print thm **)
    6.52  
    6.53 -val goals_limit = ref 10;       (*max number of goals to print*)
    6.54 -val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
    6.55 -val show_tags = ref false;      (*false: suppress tags*)
    6.56 -
    6.57  fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
    6.58  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    6.59  
    6.60 -fun pretty_flexpair pp (t, u) = Pretty.block
    6.61 -  [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
    6.62 -
    6.63  fun display_status false _ = ""
    6.64    | display_status true th =
    6.65        let
    6.66 @@ -89,7 +87,7 @@
    6.67        if hlen = 0 andalso status = "" then []
    6.68        else if ! show_hyps orelse show_hyps' then
    6.69          [Pretty.brk 2, Pretty.list "[" "]"
    6.70 -          (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
    6.71 +          (map (q o Display_Goal.pretty_flexpair pp) tpairs @ map prt_term hyps' @
    6.72             map (Pretty.sort pp) xshyps @
    6.73              (if status = "" then [] else [Pretty.str status]))]
    6.74        else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
    6.75 @@ -242,109 +240,7 @@
    6.76           Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]]
    6.77    end;
    6.78  
    6.79 -
    6.80 -
    6.81 -(** print_goals **)
    6.82 -
    6.83 -(* print_goals etc. *)
    6.84 -
    6.85 -val show_consts = ref false;  (*true: show consts with types in proof state output*)
    6.86 -
    6.87 -
    6.88 -(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
    6.89 -
    6.90 -local
    6.91 -
    6.92 -fun ins_entry (x, y) =
    6.93 -  AList.default (op =) (x, []) #>
    6.94 -  AList.map_entry (op =) x (insert (op =) y);
    6.95 -
    6.96 -val add_consts = Term.fold_aterms
    6.97 -  (fn Const (c, T) => ins_entry (T, (c, T))
    6.98 -    | _ => I);
    6.99 -
   6.100 -val add_vars = Term.fold_aterms
   6.101 -  (fn Free (x, T) => ins_entry (T, (x, ~1))
   6.102 -    | Var (xi, T) => ins_entry (T, xi)
   6.103 -    | _ => I);
   6.104 -
   6.105 -val add_varsT = Term.fold_atyps
   6.106 -  (fn TFree (x, S) => ins_entry (S, (x, ~1))
   6.107 -    | TVar (xi, S) => ins_entry (S, xi)
   6.108 -    | _ => I);
   6.109 -
   6.110 -fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
   6.111 -fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
   6.112 -
   6.113 -fun consts_of t = sort_cnsts (add_consts t []);
   6.114 -fun vars_of t = sort_idxs (add_vars t []);
   6.115 -fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
   6.116 -
   6.117 -in
   6.118 -
   6.119 -fun pretty_goals_aux pp markup (msg, main) maxgoals state =
   6.120 -  let
   6.121 -    fun prt_atoms prt prtT (X, xs) = Pretty.block
   6.122 -      [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
   6.123 -        Pretty.brk 1, prtT X];
   6.124 -
   6.125 -    fun prt_var (x, ~1) = Pretty.term pp (Syntax.free x)
   6.126 -      | prt_var xi = Pretty.term pp (Syntax.var xi);
   6.127 -
   6.128 -    fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
   6.129 -      | prt_varT xi = Pretty.typ pp (TVar (xi, []));
   6.130 -
   6.131 -    val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp);
   6.132 -    val prt_vars = prt_atoms prt_var (Pretty.typ pp);
   6.133 -    val prt_varsT = prt_atoms prt_varT (Pretty.sort pp);
   6.134 -
   6.135 -
   6.136 -    fun pretty_list _ _ [] = []
   6.137 -      | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
   6.138 -
   6.139 -    fun pretty_subgoal (n, A) = Pretty.markup markup
   6.140 -      [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A];
   6.141 -    fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
   6.142 -
   6.143 -    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp);
   6.144 -
   6.145 -    val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
   6.146 -    val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
   6.147 -    val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
   6.148 -
   6.149 -
   6.150 -    val {prop, tpairs, ...} = Thm.rep_thm state;
   6.151 -    val (As, B) = Logic.strip_horn prop;
   6.152 -    val ngoals = length As;
   6.153 -
   6.154 -    fun pretty_gs (types, sorts) =
   6.155 -      (if main then [Pretty.term pp B] else []) @
   6.156 -       (if ngoals = 0 then [Pretty.str "No subgoals!"]
   6.157 -        else if ngoals > maxgoals then
   6.158 -          pretty_subgoals (Library.take (maxgoals, As)) @
   6.159 -          (if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   6.160 -           else [])
   6.161 -        else pretty_subgoals As) @
   6.162 -      pretty_ffpairs tpairs @
   6.163 -      (if ! show_consts then pretty_consts prop else []) @
   6.164 -      (if types then pretty_vars prop else []) @
   6.165 -      (if sorts then pretty_varsT prop else []);
   6.166 -  in
   6.167 -    setmp show_no_free_types true
   6.168 -      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
   6.169 -        (setmp show_sorts false pretty_gs))
   6.170 -   (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   6.171 -  end;
   6.172 -
   6.173 -fun pretty_goals n th =
   6.174 -  pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
   6.175 -
   6.176 -val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
   6.177 -
   6.178  end;
   6.179  
   6.180 -
   6.181 -end;
   6.182 -
   6.183 -structure BasicDisplay: BASIC_DISPLAY = Display;
   6.184 -open BasicDisplay;
   6.185 +structure Basic_Display: BASIC_DISPLAY = Display;
   6.186 +open Basic_Display;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/display_goal.ML	Mon Jul 20 21:20:09 2009 +0200
     7.3 @@ -0,0 +1,121 @@
     7.4 +(*  Title:      Pure/display_goal.ML
     7.5 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.6 +    Author:     Makarius
     7.7 +
     7.8 +Display tactical goal state.
     7.9 +*)
    7.10 +
    7.11 +signature DISPLAY_GOAL =
    7.12 +sig
    7.13 +  val goals_limit: int ref
    7.14 +  val show_consts: bool ref
    7.15 +  val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
    7.16 +  val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
    7.17 +  val pretty_goals: int -> thm -> Pretty.T list
    7.18 +  val print_goals: int -> thm -> unit
    7.19 +end;
    7.20 +
    7.21 +structure Display_Goal: DISPLAY_GOAL =
    7.22 +struct
    7.23 +
    7.24 +val goals_limit = ref 10;      (*max number of goals to print*)
    7.25 +val show_consts = ref false;   (*true: show consts with types in proof state output*)
    7.26 +
    7.27 +fun pretty_flexpair pp (t, u) = Pretty.block
    7.28 +  [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
    7.29 +
    7.30 +
    7.31 +(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
    7.32 +
    7.33 +local
    7.34 +
    7.35 +fun ins_entry (x, y) =
    7.36 +  AList.default (op =) (x, []) #>
    7.37 +  AList.map_entry (op =) x (insert (op =) y);
    7.38 +
    7.39 +val add_consts = Term.fold_aterms
    7.40 +  (fn Const (c, T) => ins_entry (T, (c, T))
    7.41 +    | _ => I);
    7.42 +
    7.43 +val add_vars = Term.fold_aterms
    7.44 +  (fn Free (x, T) => ins_entry (T, (x, ~1))
    7.45 +    | Var (xi, T) => ins_entry (T, xi)
    7.46 +    | _ => I);
    7.47 +
    7.48 +val add_varsT = Term.fold_atyps
    7.49 +  (fn TFree (x, S) => ins_entry (S, (x, ~1))
    7.50 +    | TVar (xi, S) => ins_entry (S, xi)
    7.51 +    | _ => I);
    7.52 +
    7.53 +fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
    7.54 +fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
    7.55 +
    7.56 +fun consts_of t = sort_cnsts (add_consts t []);
    7.57 +fun vars_of t = sort_idxs (add_vars t []);
    7.58 +fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
    7.59 +
    7.60 +in
    7.61 +
    7.62 +fun pretty_goals_aux pp markup (msg, main) maxgoals state =
    7.63 +  let
    7.64 +    fun prt_atoms prt prtT (X, xs) = Pretty.block
    7.65 +      [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
    7.66 +        Pretty.brk 1, prtT X];
    7.67 +
    7.68 +    fun prt_var (x, ~1) = Pretty.term pp (Syntax.free x)
    7.69 +      | prt_var xi = Pretty.term pp (Syntax.var xi);
    7.70 +
    7.71 +    fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
    7.72 +      | prt_varT xi = Pretty.typ pp (TVar (xi, []));
    7.73 +
    7.74 +    val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp);
    7.75 +    val prt_vars = prt_atoms prt_var (Pretty.typ pp);
    7.76 +    val prt_varsT = prt_atoms prt_varT (Pretty.sort pp);
    7.77 +
    7.78 +
    7.79 +    fun pretty_list _ _ [] = []
    7.80 +      | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
    7.81 +
    7.82 +    fun pretty_subgoal (n, A) = Pretty.markup markup
    7.83 +      [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A];
    7.84 +    fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
    7.85 +
    7.86 +    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp);
    7.87 +
    7.88 +    val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
    7.89 +    val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
    7.90 +    val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
    7.91 +
    7.92 +
    7.93 +    val {prop, tpairs, ...} = Thm.rep_thm state;
    7.94 +    val (As, B) = Logic.strip_horn prop;
    7.95 +    val ngoals = length As;
    7.96 +
    7.97 +    fun pretty_gs (types, sorts) =
    7.98 +      (if main then [Pretty.term pp B] else []) @
    7.99 +       (if ngoals = 0 then [Pretty.str "No subgoals!"]
   7.100 +        else if ngoals > maxgoals then
   7.101 +          pretty_subgoals (Library.take (maxgoals, As)) @
   7.102 +          (if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   7.103 +           else [])
   7.104 +        else pretty_subgoals As) @
   7.105 +      pretty_ffpairs tpairs @
   7.106 +      (if ! show_consts then pretty_consts prop else []) @
   7.107 +      (if types then pretty_vars prop else []) @
   7.108 +      (if sorts then pretty_varsT prop else []);
   7.109 +  in
   7.110 +    setmp show_no_free_types true
   7.111 +      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
   7.112 +        (setmp show_sorts false pretty_gs))
   7.113 +   (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   7.114 +  end;
   7.115 +
   7.116 +fun pretty_goals n th =
   7.117 +  pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
   7.118 +
   7.119 +val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
   7.120 +
   7.121 +end;
   7.122 +
   7.123 +end;
   7.124 +
     8.1 --- a/src/Pure/goal.ML	Mon Jul 20 20:03:19 2009 +0200
     8.2 +++ b/src/Pure/goal.ML	Mon Jul 20 21:20:09 2009 +0200
     8.3 @@ -78,7 +78,7 @@
     8.4    (case Thm.nprems_of th of
     8.5      0 => conclude th
     8.6    | n => raise THM ("Proof failed.\n" ^
     8.7 -      Pretty.string_of (Pretty.chunks (Display.pretty_goals n th)) ^
     8.8 +      Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals n th)) ^
     8.9        ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
    8.10  
    8.11  
     9.1 --- a/src/Pure/old_goals.ML	Mon Jul 20 20:03:19 2009 +0200
     9.2 +++ b/src/Pure/old_goals.ML	Mon Jul 20 21:20:09 2009 +0200
     9.3 @@ -135,7 +135,7 @@
     9.4  (*Default action is to print an error message; could be suppressed for
     9.5    special applications.*)
     9.6  fun result_error_default state msg : thm =
     9.7 -  Pretty.str "Bad final proof state:" :: Display.pretty_goals (!goals_limit) state @
     9.8 +  Pretty.str "Bad final proof state:" :: Display_Goal.pretty_goals (!goals_limit) state @
     9.9      [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
    9.10  
    9.11  val result_error_fn = ref result_error_default;
    9.12 @@ -277,7 +277,7 @@
    9.13        (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
    9.14          (if ngoals <> 1 then "s" else "") ^ ")"
    9.15        else ""))] @
    9.16 -    Display.pretty_goals m th
    9.17 +    Display_Goal.pretty_goals m th
    9.18    end |> Pretty.chunks |> Pretty.writeln;
    9.19  
    9.20  (*Printing can raise exceptions, so the assignment occurs last.
    10.1 --- a/src/Pure/tctical.ML	Mon Jul 20 20:03:19 2009 +0200
    10.2 +++ b/src/Pure/tctical.ML	Mon Jul 20 21:20:09 2009 +0200
    10.3 @@ -195,7 +195,7 @@
    10.4      (fn st =>
    10.5       (tracing msg;
    10.6        tracing ((Pretty.string_of o Pretty.chunks o
    10.7 -                 Display.pretty_goals (! Display.goals_limit)) st);
    10.8 +                 Display_Goal.pretty_goals (! Display_Goal.goals_limit)) st);
    10.9        Seq.single st));
   10.10  
   10.11  (*Pause until a line is typed -- if non-empty then fail. *)
   10.12 @@ -233,7 +233,7 @@
   10.13  (*Extract from a tactic, a thm->thm seq function that handles tracing*)
   10.14  fun tracify flag tac st =
   10.15    if !flag andalso not (!suppress_tracing)
   10.16 -           then (Display.print_goals (! Display.goals_limit) st;
   10.17 +           then (Display_Goal.print_goals (! Display_Goal.goals_limit) st;
   10.18                   tracing "** Press RETURN to continue:";
   10.19                   exec_trace_command flag (tac,st))
   10.20    else tac st;