src/Pure/display_goal.ML
changeset 32145 220c9e439d39
parent 32089 568a23753e3a
child 32167 d32817dda0e6
     1.1 --- a/src/Pure/display_goal.ML	Thu Jul 23 16:43:31 2009 +0200
     1.2 +++ b/src/Pure/display_goal.ML	Thu Jul 23 16:52:16 2009 +0200
     1.3 @@ -9,10 +9,10 @@
     1.4  sig
     1.5    val goals_limit: int ref
     1.6    val show_consts: bool ref
     1.7 -  val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
     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 pretty_flexpair: Proof.context -> term * term -> Pretty.T
    1.12 +  val pretty_goals: Proof.context -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
    1.13 +  val pretty_goals_without_context: int -> thm -> Pretty.T list
    1.14 +  val print_goals_without_context: int -> thm -> unit
    1.15  end;
    1.16  
    1.17  structure Display_Goal: DISPLAY_GOAL =
    1.18 @@ -21,8 +21,8 @@
    1.19  val goals_limit = ref 10;      (*max number of goals to print*)
    1.20  val show_consts = ref false;   (*true: show consts with types in proof state output*)
    1.21  
    1.22 -fun pretty_flexpair pp (t, u) = Pretty.block
    1.23 -  [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
    1.24 +fun pretty_flexpair ctxt (t, u) = Pretty.block
    1.25 +  [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
    1.26  
    1.27  
    1.28  (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
    1.29 @@ -56,31 +56,35 @@
    1.30  
    1.31  in
    1.32  
    1.33 -fun pretty_goals_aux pp markup (msg, main) maxgoals state =
    1.34 +fun pretty_goals ctxt markup (msg, main) maxgoals state =
    1.35    let
    1.36 +    val prt_sort = Syntax.pretty_sort ctxt;
    1.37 +    val prt_typ = Syntax.pretty_typ ctxt;
    1.38 +    val prt_term = Syntax.pretty_term ctxt;
    1.39 +
    1.40      fun prt_atoms prt prtT (X, xs) = Pretty.block
    1.41        [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
    1.42          Pretty.brk 1, prtT X];
    1.43  
    1.44 -    fun prt_var (x, ~1) = Pretty.term pp (Syntax.free x)
    1.45 -      | prt_var xi = Pretty.term pp (Syntax.var xi);
    1.46 +    fun prt_var (x, ~1) = prt_term (Syntax.free x)
    1.47 +      | prt_var xi = prt_term (Syntax.var xi);
    1.48  
    1.49 -    fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
    1.50 -      | prt_varT xi = Pretty.typ pp (TVar (xi, []));
    1.51 +    fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
    1.52 +      | prt_varT xi = prt_typ (TVar (xi, []));
    1.53  
    1.54 -    val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp);
    1.55 -    val prt_vars = prt_atoms prt_var (Pretty.typ pp);
    1.56 -    val prt_varsT = prt_atoms prt_varT (Pretty.sort pp);
    1.57 +    val prt_consts = prt_atoms (prt_term o Const) prt_typ;
    1.58 +    val prt_vars = prt_atoms prt_var prt_typ;
    1.59 +    val prt_varsT = prt_atoms prt_varT prt_sort;
    1.60  
    1.61  
    1.62      fun pretty_list _ _ [] = []
    1.63        | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
    1.64  
    1.65      fun pretty_subgoal (n, A) = Pretty.markup markup
    1.66 -      [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A];
    1.67 +      [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
    1.68      fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
    1.69  
    1.70 -    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp);
    1.71 +    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
    1.72  
    1.73      val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
    1.74      val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
    1.75 @@ -92,7 +96,7 @@
    1.76      val ngoals = length As;
    1.77  
    1.78      fun pretty_gs (types, sorts) =
    1.79 -      (if main then [Pretty.term pp B] else []) @
    1.80 +      (if main then [prt_term B] else []) @
    1.81         (if ngoals = 0 then [Pretty.str "No subgoals!"]
    1.82          else if ngoals > maxgoals then
    1.83            pretty_subgoals (Library.take (maxgoals, As)) @
    1.84 @@ -110,10 +114,11 @@
    1.85     (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
    1.86    end;
    1.87  
    1.88 -fun pretty_goals n th =
    1.89 -  pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
    1.90 +fun pretty_goals_without_context n th =
    1.91 +  pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
    1.92  
    1.93 -val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
    1.94 +val print_goals_without_context =
    1.95 +  (Pretty.writeln o Pretty.chunks) oo pretty_goals_without_context;
    1.96  
    1.97  end;
    1.98