clarified pretty_goals, pretty_thm_aux: plain context;
authorwenzelm
Thu Jul 23 16:52:16 2009 +0200 (2009-07-23)
changeset 32145220c9e439d39
parent 32144 183c1010ac14
child 32146 4937d9836824
clarified pretty_goals, pretty_thm_aux: plain context;
explicit pretty_goals_without_context, print_goals_without_context;
tuned;
src/HOL/Tools/Function/lexicographic_order.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_display.ML
src/Pure/Proof/reconstruct.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	Thu Jul 23 16:43:31 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jul 23 16:52:16 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_Goal.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
     1.8 +    Display_Goal.pretty_goals 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/Isar/proof.ML	Thu Jul 23 16:43:31 2009 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Thu Jul 23 16:52:16 2009 +0200
     2.3 @@ -318,8 +318,6 @@
     2.4  val show_main_goal = ref false;
     2.5  val verbose = ProofContext.verbose;
     2.6  
     2.7 -val pretty_goals_local = Display_Goal.pretty_goals_aux o Syntax.pp;
     2.8 -
     2.9  fun pretty_facts _ _ NONE = []
    2.10    | pretty_facts s ctxt (SOME ths) =
    2.11        [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""];
    2.12 @@ -346,7 +344,7 @@
    2.13              (if mode <> Backward orelse null using then NONE else SOME using) @
    2.14            [Pretty.str ("goal" ^
    2.15              description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
    2.16 -          pretty_goals_local ctxt Markup.subgoal
    2.17 +          Display_Goal.pretty_goals ctxt Markup.subgoal
    2.18              (true, ! show_main_goal) (! Display.goals_limit) goal @
    2.19            (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
    2.20        | prt_goal NONE = [];
    2.21 @@ -368,7 +366,7 @@
    2.22  
    2.23  fun pretty_goals main state =
    2.24    let val (ctxt, (_, goal)) = get_goal state
    2.25 -  in pretty_goals_local ctxt Markup.none (false, main) (! Display.goals_limit) goal end;
    2.26 +  in Display_Goal.pretty_goals ctxt Markup.none (false, main) (! Display.goals_limit) goal end;
    2.27  
    2.28  
    2.29  
    2.30 @@ -474,7 +472,8 @@
    2.31  
    2.32      val ngoals = Thm.nprems_of goal;
    2.33      val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
    2.34 -      (pretty_goals_local ctxt Markup.none (true, ! show_main_goal) (! Display.goals_limit) goal @
    2.35 +      (Display_Goal.pretty_goals ctxt Markup.none
    2.36 +          (true, ! show_main_goal) (! Display.goals_limit) goal @
    2.37          [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
    2.38  
    2.39      val extra_hyps = Assumption.extra_hyps ctxt goal;
     3.1 --- a/src/Pure/Isar/proof_display.ML	Thu Jul 23 16:43:31 2009 +0200
     3.2 +++ b/src/Pure/Isar/proof_display.ML	Thu Jul 23 16:52:16 2009 +0200
     3.3 @@ -35,7 +35,7 @@
     3.4    let
     3.5      val thy = Thm.theory_of_thm th;
     3.6      val flags = {quote = true, show_hyps = false, show_status = true};
     3.7 -  in Display.pretty_thm_raw (Syntax.pp_global thy) flags [] th end;
     3.8 +  in Display.pretty_thm_raw (Syntax.init_pretty_global thy) flags th end;
     3.9  
    3.10  val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
    3.11  val pp_term = Pretty.quote oo Syntax.pretty_term_global;
     4.1 --- a/src/Pure/Proof/reconstruct.ML	Thu Jul 23 16:43:31 2009 +0200
     4.2 +++ b/src/Pure/Proof/reconstruct.ML	Thu Jul 23 16:52:16 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_Goal.pretty_flexpair (Syntax.pp_global thy) (pairself
     4.8 +                Display_Goal.pretty_flexpair (Syntax.init_pretty_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/display.ML	Thu Jul 23 16:43:31 2009 +0200
     5.2 +++ b/src/Pure/display.ML	Thu Jul 23 16:52:16 2009 +0200
     5.3 @@ -16,8 +16,8 @@
     5.4  signature DISPLAY =
     5.5  sig
     5.6    include BASIC_DISPLAY
     5.7 -  val pretty_thm_raw: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
     5.8 -    term list -> thm -> Pretty.T
     5.9 +  val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool, show_status: bool} ->
    5.10 +    thm -> Pretty.T
    5.11    val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
    5.12    val pretty_thm: Proof.context -> thm -> Pretty.T
    5.13    val pretty_thm_global: theory -> thm -> Pretty.T
    5.14 @@ -68,7 +68,7 @@
    5.15          else ""
    5.16        end;
    5.17  
    5.18 -fun pretty_thm_raw pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
    5.19 +fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps', show_status} raw_th =
    5.20    let
    5.21      val th = Thm.strip_shyps raw_th;
    5.22      val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
    5.23 @@ -76,8 +76,9 @@
    5.24      val tags = Thm.get_tags th;
    5.25  
    5.26      val q = if quote then Pretty.quote else I;
    5.27 -    val prt_term = q o Pretty.term pp;
    5.28 +    val prt_term = q o Syntax.pretty_term ctxt;
    5.29  
    5.30 +    val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
    5.31      val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    5.32      val status = display_status show_status th;
    5.33  
    5.34 @@ -86,8 +87,8 @@
    5.35        if hlen = 0 andalso status = "" then []
    5.36        else if ! show_hyps orelse show_hyps' then
    5.37          [Pretty.brk 2, Pretty.list "[" "]"
    5.38 -          (map (q o Display_Goal.pretty_flexpair pp) tpairs @ map prt_term hyps' @
    5.39 -           map (Pretty.sort pp) xshyps @
    5.40 +          (map (q o Display_Goal.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
    5.41 +           map (Syntax.pretty_sort ctxt) xshyps @
    5.42              (if status = "" then [] else [Pretty.str status]))]
    5.43        else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
    5.44      val tsymbs =
    5.45 @@ -95,18 +96,14 @@
    5.46        else [Pretty.brk 1, pretty_tags tags];
    5.47    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    5.48  
    5.49 -fun pretty_thm_aux ctxt show_status th =
    5.50 -  let
    5.51 -    val flags = {quote = false, show_hyps = true, show_status = show_status};
    5.52 -    val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
    5.53 -  in pretty_thm_raw (Syntax.pp ctxt) flags asms th end;
    5.54 -
    5.55 +fun pretty_thm_aux ctxt show_status =
    5.56 +  pretty_thm_raw ctxt {quote = false, show_hyps = true, show_status = show_status};
    5.57  
    5.58  fun pretty_thm ctxt = pretty_thm_aux ctxt true;
    5.59  
    5.60 -fun pretty_thm_global thy th =
    5.61 -  pretty_thm_raw (Syntax.pp_global thy)
    5.62 -    {quote = false, show_hyps = false, show_status = true} [] th;
    5.63 +fun pretty_thm_global thy =
    5.64 +  pretty_thm_raw (Syntax.init_pretty_global thy)
    5.65 +    {quote = false, show_hyps = false, show_status = true};
    5.66  
    5.67  fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th;
    5.68  
     6.1 --- a/src/Pure/display_goal.ML	Thu Jul 23 16:43:31 2009 +0200
     6.2 +++ b/src/Pure/display_goal.ML	Thu Jul 23 16:52:16 2009 +0200
     6.3 @@ -9,10 +9,10 @@
     6.4  sig
     6.5    val goals_limit: int ref
     6.6    val show_consts: bool ref
     6.7 -  val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
     6.8 -  val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
     6.9 -  val pretty_goals: int -> thm -> Pretty.T list
    6.10 -  val print_goals: int -> thm -> unit
    6.11 +  val pretty_flexpair: Proof.context -> term * term -> Pretty.T
    6.12 +  val pretty_goals: Proof.context -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
    6.13 +  val pretty_goals_without_context: int -> thm -> Pretty.T list
    6.14 +  val print_goals_without_context: int -> thm -> unit
    6.15  end;
    6.16  
    6.17  structure Display_Goal: DISPLAY_GOAL =
    6.18 @@ -21,8 +21,8 @@
    6.19  val goals_limit = ref 10;      (*max number of goals to print*)
    6.20  val show_consts = ref false;   (*true: show consts with types in proof state output*)
    6.21  
    6.22 -fun pretty_flexpair pp (t, u) = Pretty.block
    6.23 -  [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
    6.24 +fun pretty_flexpair ctxt (t, u) = Pretty.block
    6.25 +  [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
    6.26  
    6.27  
    6.28  (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
    6.29 @@ -56,31 +56,35 @@
    6.30  
    6.31  in
    6.32  
    6.33 -fun pretty_goals_aux pp markup (msg, main) maxgoals state =
    6.34 +fun pretty_goals ctxt markup (msg, main) maxgoals state =
    6.35    let
    6.36 +    val prt_sort = Syntax.pretty_sort ctxt;
    6.37 +    val prt_typ = Syntax.pretty_typ ctxt;
    6.38 +    val prt_term = Syntax.pretty_term ctxt;
    6.39 +
    6.40      fun prt_atoms prt prtT (X, xs) = Pretty.block
    6.41        [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
    6.42          Pretty.brk 1, prtT X];
    6.43  
    6.44 -    fun prt_var (x, ~1) = Pretty.term pp (Syntax.free x)
    6.45 -      | prt_var xi = Pretty.term pp (Syntax.var xi);
    6.46 +    fun prt_var (x, ~1) = prt_term (Syntax.free x)
    6.47 +      | prt_var xi = prt_term (Syntax.var xi);
    6.48  
    6.49 -    fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
    6.50 -      | prt_varT xi = Pretty.typ pp (TVar (xi, []));
    6.51 +    fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
    6.52 +      | prt_varT xi = prt_typ (TVar (xi, []));
    6.53  
    6.54 -    val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp);
    6.55 -    val prt_vars = prt_atoms prt_var (Pretty.typ pp);
    6.56 -    val prt_varsT = prt_atoms prt_varT (Pretty.sort pp);
    6.57 +    val prt_consts = prt_atoms (prt_term o Const) prt_typ;
    6.58 +    val prt_vars = prt_atoms prt_var prt_typ;
    6.59 +    val prt_varsT = prt_atoms prt_varT prt_sort;
    6.60  
    6.61  
    6.62      fun pretty_list _ _ [] = []
    6.63        | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
    6.64  
    6.65      fun pretty_subgoal (n, A) = Pretty.markup markup
    6.66 -      [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A];
    6.67 +      [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
    6.68      fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
    6.69  
    6.70 -    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp);
    6.71 +    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
    6.72  
    6.73      val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
    6.74      val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
    6.75 @@ -92,7 +96,7 @@
    6.76      val ngoals = length As;
    6.77  
    6.78      fun pretty_gs (types, sorts) =
    6.79 -      (if main then [Pretty.term pp B] else []) @
    6.80 +      (if main then [prt_term B] else []) @
    6.81         (if ngoals = 0 then [Pretty.str "No subgoals!"]
    6.82          else if ngoals > maxgoals then
    6.83            pretty_subgoals (Library.take (maxgoals, As)) @
    6.84 @@ -110,10 +114,11 @@
    6.85     (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
    6.86    end;
    6.87  
    6.88 -fun pretty_goals n th =
    6.89 -  pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
    6.90 +fun pretty_goals_without_context n th =
    6.91 +  pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
    6.92  
    6.93 -val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
    6.94 +val print_goals_without_context =
    6.95 +  (Pretty.writeln o Pretty.chunks) oo pretty_goals_without_context;
    6.96  
    6.97  end;
    6.98  
     7.1 --- a/src/Pure/goal.ML	Thu Jul 23 16:43:31 2009 +0200
     7.2 +++ b/src/Pure/goal.ML	Thu Jul 23 16:52:16 2009 +0200
     7.3 @@ -78,7 +78,7 @@
     7.4    (case Thm.nprems_of th of
     7.5      0 => conclude th
     7.6    | n => raise THM ("Proof failed.\n" ^
     7.7 -      Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals n th)) ^
     7.8 +      Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals_without_context n th)) ^
     7.9        ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
    7.10  
    7.11  
     8.1 --- a/src/Pure/old_goals.ML	Thu Jul 23 16:43:31 2009 +0200
     8.2 +++ b/src/Pure/old_goals.ML	Thu Jul 23 16:52:16 2009 +0200
     8.3 @@ -135,7 +135,8 @@
     8.4  (*Default action is to print an error message; could be suppressed for
     8.5    special applications.*)
     8.6  fun result_error_default state msg : thm =
     8.7 -  Pretty.str "Bad final proof state:" :: Display_Goal.pretty_goals (!goals_limit) state @
     8.8 +  Pretty.str "Bad final proof state:" ::
     8.9 +      Display_Goal.pretty_goals_without_context (!goals_limit) state @
    8.10      [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
    8.11  
    8.12  val result_error_fn = ref result_error_default;
    8.13 @@ -277,7 +278,7 @@
    8.14        (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
    8.15          (if ngoals <> 1 then "s" else "") ^ ")"
    8.16        else ""))] @
    8.17 -    Display_Goal.pretty_goals m th
    8.18 +    Display_Goal.pretty_goals_without_context m th
    8.19    end |> Pretty.chunks |> Pretty.writeln;
    8.20  
    8.21  (*Printing can raise exceptions, so the assignment occurs last.
     9.1 --- a/src/Pure/tctical.ML	Thu Jul 23 16:43:31 2009 +0200
     9.2 +++ b/src/Pure/tctical.ML	Thu Jul 23 16:52:16 2009 +0200
     9.3 @@ -191,12 +191,11 @@
     9.4  (*** Tracing tactics ***)
     9.5  
     9.6  (*Print the current proof state and pass it on.*)
     9.7 -fun print_tac msg =
     9.8 -    (fn st =>
     9.9 -     (tracing msg;
    9.10 -      tracing ((Pretty.string_of o Pretty.chunks o
    9.11 -                 Display_Goal.pretty_goals (! Display_Goal.goals_limit)) st);
    9.12 -      Seq.single st));
    9.13 +fun print_tac msg st =
    9.14 + (tracing (msg ^ "\n" ^
    9.15 +    Pretty.string_of (Pretty.chunks
    9.16 +      (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st)));
    9.17 +  Seq.single st);
    9.18  
    9.19  (*Pause until a line is typed -- if non-empty then fail. *)
    9.20  fun pause_tac st =
    9.21 @@ -232,10 +231,10 @@
    9.22  
    9.23  (*Extract from a tactic, a thm->thm seq function that handles tracing*)
    9.24  fun tracify flag tac st =
    9.25 -  if !flag andalso not (!suppress_tracing)
    9.26 -           then (Display_Goal.print_goals (! Display_Goal.goals_limit) st;
    9.27 -                 tracing "** Press RETURN to continue:";
    9.28 -                 exec_trace_command flag (tac,st))
    9.29 +  if !flag andalso not (!suppress_tracing) then
    9.30 +   (Display_Goal.print_goals_without_context (! Display_Goal.goals_limit) st;
    9.31 +    tracing "** Press RETURN to continue:";
    9.32 +    exec_trace_command flag (tac, st))
    9.33    else tac st;
    9.34  
    9.35  (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)