src/Pure/display.ML
changeset 14876 477c414000f8
parent 14794 751d5af6d91e
child 14990 582b655da757
     1.1 --- a/src/Pure/display.ML	Sat Jun 05 13:07:49 2004 +0200
     1.2 +++ b/src/Pure/display.ML	Sat Jun 05 13:08:53 2004 +0200
     1.3 @@ -28,8 +28,8 @@
     1.4  signature DISPLAY =
     1.5  sig
     1.6    include BASIC_DISPLAY
     1.7 -  val pretty_flexpair: (term -> Pretty.T) -> term * term -> Pretty.T
     1.8 -  val pretty_thm_aux: (sort -> Pretty.T) * (term -> Pretty.T) -> bool -> thm -> Pretty.T
     1.9 +  val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
    1.10 +  val pretty_thm_aux: Pretty.pp -> bool -> thm -> Pretty.T
    1.11    val pretty_thm_no_quote: thm -> Pretty.T
    1.12    val pretty_thm: thm -> Pretty.T
    1.13    val pretty_thms: thm list -> Pretty.T
    1.14 @@ -44,8 +44,7 @@
    1.15    val pprint_theory: theory -> pprint_args -> unit
    1.16    val pretty_full_theory: theory -> Pretty.T list
    1.17    val pretty_name_space: string * NameSpace.T -> Pretty.T
    1.18 -  val pretty_goals_aux: (sort -> Pretty.T) * (typ -> Pretty.T) * (term -> Pretty.T)
    1.19 -    -> string -> bool * bool -> int -> thm -> Pretty.T list
    1.20 +  val pretty_goals_aux: Pretty.pp -> string -> bool * bool -> int -> thm -> Pretty.T list
    1.21    val pretty_goals: int -> thm -> Pretty.T list
    1.22    val print_goals: int -> thm -> unit
    1.23    val current_goals_markers: (string * string * string) ref
    1.24 @@ -67,25 +66,25 @@
    1.25  fun pretty_tag (name, args) = Pretty.strs (name :: map Library.quote args);
    1.26  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    1.27  
    1.28 -fun pretty_flexpair pretty_term (t, u) = Pretty.block
    1.29 -  [pretty_term t, Pretty.str " =?=", Pretty.brk 1, pretty_term u];
    1.30 +fun pretty_flexpair pp (t, u) = Pretty.block
    1.31 +  [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
    1.32  
    1.33 -fun pretty_thm_aux (pretty_sort, pretty_term) quote th =
    1.34 +fun pretty_thm_aux pp quote th =
    1.35    let
    1.36      val {hyps, tpairs, prop, der = (ora, _), ...} = rep_thm th;
    1.37      val xshyps = Thm.extra_shyps th;
    1.38      val (_, tags) = Thm.get_name_tags th;
    1.39  
    1.40      val q = if quote then Pretty.quote else I;
    1.41 -    val prt_term = q o pretty_term;
    1.42 +    val prt_term = q o (Pretty.term pp);
    1.43  
    1.44      val hlen = length xshyps + length hyps + length tpairs;
    1.45      val hsymbs =
    1.46        if hlen = 0 andalso not ora then []
    1.47        else if ! show_hyps then
    1.48          [Pretty.brk 2, Pretty.list "[" "]"
    1.49 -          (map (q o pretty_flexpair pretty_term) tpairs @ map prt_term hyps @
    1.50 -           map pretty_sort xshyps @
    1.51 +          (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps @
    1.52 +           map (Pretty.sort pp) xshyps @
    1.53              (if ora then [Pretty.str "!"] else []))]
    1.54        else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
    1.55          (if ora then "!" else "") ^ "]")];
    1.56 @@ -95,8 +94,7 @@
    1.57    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    1.58  
    1.59  fun gen_pretty_thm quote th =
    1.60 -  let val sg = Thm.sign_of_thm th
    1.61 -  in pretty_thm_aux (Sign.pretty_sort sg, Sign.pretty_term sg) quote th end;
    1.62 +  pretty_thm_aux (Sign.pp (Thm.sign_of_thm th)) quote th;
    1.63  
    1.64  val pretty_thm = gen_pretty_thm true;
    1.65  val pretty_thm_no_quote = gen_pretty_thm false;
    1.66 @@ -296,31 +294,31 @@
    1.67  
    1.68  in
    1.69  
    1.70 -fun pretty_goals_aux (prt_sort, prt_typ, prt_term) begin_goal (msg, main) maxgoals state =
    1.71 +fun pretty_goals_aux pp begin_goal (msg, main) maxgoals state =
    1.72    let
    1.73      fun prt_atoms prt prtT (X, xs) = Pretty.block
    1.74        [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
    1.75          Pretty.brk 1, prtT X];
    1.76  
    1.77 -    fun prt_var (x, ~1) = prt_term (Syntax.free x)
    1.78 -      | prt_var xi = prt_term (Syntax.var xi);
    1.79 +    fun prt_var (x, ~1) = Pretty.term pp (Syntax.free x)
    1.80 +      | prt_var xi = Pretty.term pp (Syntax.var xi);
    1.81  
    1.82 -    fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
    1.83 -      | prt_varT xi = prt_typ (TVar (xi, []));
    1.84 +    fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
    1.85 +      | prt_varT xi = Pretty.typ pp (TVar (xi, []));
    1.86  
    1.87 -    val prt_consts = prt_atoms (prt_term o Const) prt_typ;
    1.88 -    val prt_vars = prt_atoms prt_var prt_typ;
    1.89 -    val prt_varsT = prt_atoms prt_varT prt_sort;
    1.90 +    val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp);
    1.91 +    val prt_vars = prt_atoms prt_var (Pretty.typ pp);
    1.92 +    val prt_varsT = prt_atoms prt_varT (Pretty.sort pp);
    1.93  
    1.94  
    1.95      fun pretty_list _ _ [] = []
    1.96        | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
    1.97  
    1.98 -    fun pretty_subgoal (n, A) =
    1.99 -      Pretty.blk (0, [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]);
   1.100 +    fun pretty_subgoal (n, A) = Pretty.blk (0,
   1.101 +     [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), Pretty.term pp A]);
   1.102      fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
   1.103  
   1.104 -    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair prt_term);
   1.105 +    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp);
   1.106  
   1.107      val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
   1.108      val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
   1.109 @@ -332,7 +330,7 @@
   1.110      val ngoals = length As;
   1.111  
   1.112      fun pretty_gs (types, sorts) =
   1.113 -      (if main then [prt_term B] else []) @
   1.114 +      (if main then [Pretty.term pp B] else []) @
   1.115         (if ngoals = 0 then [Pretty.str "No subgoals!"]
   1.116          else if ngoals > maxgoals then
   1.117            pretty_subgoals (take (maxgoals, As)) @
   1.118 @@ -351,10 +349,7 @@
   1.119    end;
   1.120  
   1.121  fun pretty_goals_marker bg n th =
   1.122 -  let val sg = Thm.sign_of_thm th in
   1.123 -    pretty_goals_aux (Sign.pretty_sort sg, Sign.pretty_typ sg, Sign.pretty_term sg)
   1.124 -      bg (true, true) n th
   1.125 -  end;
   1.126 +  pretty_goals_aux (Sign.pp (Thm.sign_of_thm th)) bg (true, true) n th;
   1.127  
   1.128  val pretty_goals = pretty_goals_marker "";
   1.129  val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals_marker "";