pretty_thm/goals_aux, pretty_flexpair: pp;
authorwenzelm
Sat Jun 05 13:08:53 2004 +0200 (2004-06-05)
changeset 14876477c414000f8
parent 14875 c48d086264c4
child 14877 28084696907f
pretty_thm/goals_aux, pretty_flexpair: pp;
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Proof/reconstruct.ML
src/Pure/display.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Sat Jun 05 13:07:49 2004 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Sat Jun 05 13:08:53 2004 +0200
     1.3 @@ -329,8 +329,7 @@
     1.4  
     1.5  val verbose = ProofContext.verbose;
     1.6  
     1.7 -fun pretty_goals_local ctxt = Display.pretty_goals_aux
     1.8 -  (ProofContext.pretty_sort ctxt, ProofContext.pretty_typ ctxt, ProofContext.pretty_term ctxt);
     1.9 +val pretty_goals_local = Display.pretty_goals_aux o ProofContext.pp;
    1.10  
    1.11  fun pretty_facts _ _ None = []
    1.12    | pretty_facts s ctxt (Some ths) =
     2.1 --- a/src/Pure/Isar/proof_context.ML	Sat Jun 05 13:07:49 2004 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Jun 05 13:08:53 2004 +0200
     2.3 @@ -392,7 +392,7 @@
     2.4  
     2.5  fun pretty_thm ctxt thm =
     2.6    if ! Display.show_hyps then
     2.7 -    Display.pretty_thm_aux (pretty_sort ctxt, pretty_term ctxt) false thm
     2.8 +    Display.pretty_thm_aux (pp ctxt) false thm
     2.9    else pretty_term ctxt (Thm.prop_of thm);
    2.10  
    2.11  fun pretty_thms ctxt [th] = pretty_thm ctxt th
     3.1 --- a/src/Pure/Proof/reconstruct.ML	Sat Jun 05 13:07:49 2004 +0200
     3.2 +++ b/src/Pure/Proof/reconstruct.ML	Sat Jun 05 13:08:53 2004 +0200
     3.3 @@ -265,7 +265,7 @@
     3.4        let
     3.5          fun search env [] = error ("Unsolvable constraints:\n" ^
     3.6                Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
     3.7 -                Display.pretty_flexpair (Sign.pretty_term sg) (pairself
     3.8 +                Display.pretty_flexpair (Sign.pp sg) (pairself
     3.9                    (Envir.norm_term bigenv) p)) cs)))
    3.10            | search env ((u, p as (t1, t2), vs)::ps) =
    3.11                if u then
     4.1 --- a/src/Pure/display.ML	Sat Jun 05 13:07:49 2004 +0200
     4.2 +++ b/src/Pure/display.ML	Sat Jun 05 13:08:53 2004 +0200
     4.3 @@ -28,8 +28,8 @@
     4.4  signature DISPLAY =
     4.5  sig
     4.6    include BASIC_DISPLAY
     4.7 -  val pretty_flexpair: (term -> Pretty.T) -> term * term -> Pretty.T
     4.8 -  val pretty_thm_aux: (sort -> Pretty.T) * (term -> Pretty.T) -> bool -> thm -> Pretty.T
     4.9 +  val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
    4.10 +  val pretty_thm_aux: Pretty.pp -> bool -> thm -> Pretty.T
    4.11    val pretty_thm_no_quote: thm -> Pretty.T
    4.12    val pretty_thm: thm -> Pretty.T
    4.13    val pretty_thms: thm list -> Pretty.T
    4.14 @@ -44,8 +44,7 @@
    4.15    val pprint_theory: theory -> pprint_args -> unit
    4.16    val pretty_full_theory: theory -> Pretty.T list
    4.17    val pretty_name_space: string * NameSpace.T -> Pretty.T
    4.18 -  val pretty_goals_aux: (sort -> Pretty.T) * (typ -> Pretty.T) * (term -> Pretty.T)
    4.19 -    -> string -> bool * bool -> int -> thm -> Pretty.T list
    4.20 +  val pretty_goals_aux: Pretty.pp -> string -> bool * bool -> int -> thm -> Pretty.T list
    4.21    val pretty_goals: int -> thm -> Pretty.T list
    4.22    val print_goals: int -> thm -> unit
    4.23    val current_goals_markers: (string * string * string) ref
    4.24 @@ -67,25 +66,25 @@
    4.25  fun pretty_tag (name, args) = Pretty.strs (name :: map Library.quote args);
    4.26  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    4.27  
    4.28 -fun pretty_flexpair pretty_term (t, u) = Pretty.block
    4.29 -  [pretty_term t, Pretty.str " =?=", Pretty.brk 1, pretty_term u];
    4.30 +fun pretty_flexpair pp (t, u) = Pretty.block
    4.31 +  [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
    4.32  
    4.33 -fun pretty_thm_aux (pretty_sort, pretty_term) quote th =
    4.34 +fun pretty_thm_aux pp quote th =
    4.35    let
    4.36      val {hyps, tpairs, prop, der = (ora, _), ...} = rep_thm th;
    4.37      val xshyps = Thm.extra_shyps th;
    4.38      val (_, tags) = Thm.get_name_tags th;
    4.39  
    4.40      val q = if quote then Pretty.quote else I;
    4.41 -    val prt_term = q o pretty_term;
    4.42 +    val prt_term = q o (Pretty.term pp);
    4.43  
    4.44      val hlen = length xshyps + length hyps + length tpairs;
    4.45      val hsymbs =
    4.46        if hlen = 0 andalso not ora then []
    4.47        else if ! show_hyps then
    4.48          [Pretty.brk 2, Pretty.list "[" "]"
    4.49 -          (map (q o pretty_flexpair pretty_term) tpairs @ map prt_term hyps @
    4.50 -           map pretty_sort xshyps @
    4.51 +          (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps @
    4.52 +           map (Pretty.sort pp) xshyps @
    4.53              (if ora then [Pretty.str "!"] else []))]
    4.54        else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
    4.55          (if ora then "!" else "") ^ "]")];
    4.56 @@ -95,8 +94,7 @@
    4.57    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    4.58  
    4.59  fun gen_pretty_thm quote th =
    4.60 -  let val sg = Thm.sign_of_thm th
    4.61 -  in pretty_thm_aux (Sign.pretty_sort sg, Sign.pretty_term sg) quote th end;
    4.62 +  pretty_thm_aux (Sign.pp (Thm.sign_of_thm th)) quote th;
    4.63  
    4.64  val pretty_thm = gen_pretty_thm true;
    4.65  val pretty_thm_no_quote = gen_pretty_thm false;
    4.66 @@ -296,31 +294,31 @@
    4.67  
    4.68  in
    4.69  
    4.70 -fun pretty_goals_aux (prt_sort, prt_typ, prt_term) begin_goal (msg, main) maxgoals state =
    4.71 +fun pretty_goals_aux pp begin_goal (msg, main) maxgoals state =
    4.72    let
    4.73      fun prt_atoms prt prtT (X, xs) = Pretty.block
    4.74        [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
    4.75          Pretty.brk 1, prtT X];
    4.76  
    4.77 -    fun prt_var (x, ~1) = prt_term (Syntax.free x)
    4.78 -      | prt_var xi = prt_term (Syntax.var xi);
    4.79 +    fun prt_var (x, ~1) = Pretty.term pp (Syntax.free x)
    4.80 +      | prt_var xi = Pretty.term pp (Syntax.var xi);
    4.81  
    4.82 -    fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
    4.83 -      | prt_varT xi = prt_typ (TVar (xi, []));
    4.84 +    fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
    4.85 +      | prt_varT xi = Pretty.typ pp (TVar (xi, []));
    4.86  
    4.87 -    val prt_consts = prt_atoms (prt_term o Const) prt_typ;
    4.88 -    val prt_vars = prt_atoms prt_var prt_typ;
    4.89 -    val prt_varsT = prt_atoms prt_varT prt_sort;
    4.90 +    val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp);
    4.91 +    val prt_vars = prt_atoms prt_var (Pretty.typ pp);
    4.92 +    val prt_varsT = prt_atoms prt_varT (Pretty.sort pp);
    4.93  
    4.94  
    4.95      fun pretty_list _ _ [] = []
    4.96        | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
    4.97  
    4.98 -    fun pretty_subgoal (n, A) =
    4.99 -      Pretty.blk (0, [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]);
   4.100 +    fun pretty_subgoal (n, A) = Pretty.blk (0,
   4.101 +     [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), Pretty.term pp A]);
   4.102      fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
   4.103  
   4.104 -    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair prt_term);
   4.105 +    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp);
   4.106  
   4.107      val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
   4.108      val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
   4.109 @@ -332,7 +330,7 @@
   4.110      val ngoals = length As;
   4.111  
   4.112      fun pretty_gs (types, sorts) =
   4.113 -      (if main then [prt_term B] else []) @
   4.114 +      (if main then [Pretty.term pp B] else []) @
   4.115         (if ngoals = 0 then [Pretty.str "No subgoals!"]
   4.116          else if ngoals > maxgoals then
   4.117            pretty_subgoals (take (maxgoals, As)) @
   4.118 @@ -351,10 +349,7 @@
   4.119    end;
   4.120  
   4.121  fun pretty_goals_marker bg n th =
   4.122 -  let val sg = Thm.sign_of_thm th in
   4.123 -    pretty_goals_aux (Sign.pretty_sort sg, Sign.pretty_typ sg, Sign.pretty_term sg)
   4.124 -      bg (true, true) n th
   4.125 -  end;
   4.126 +  pretty_goals_aux (Sign.pp (Thm.sign_of_thm th)) bg (true, true) n th;
   4.127  
   4.128  val pretty_goals = pretty_goals_marker "";
   4.129  val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals_marker "";