src/Pure/display.ML
changeset 32089 568a23753e3a
parent 30723 a3adc9a96a16
child 32090 39acf19e9f3a
     1.1 --- a/src/Pure/display.ML	Mon Jul 20 20:03:19 2009 +0200
     1.2 +++ b/src/Pure/display.ML	Mon Jul 20 21:20:09 2009 +0200
     1.3 @@ -1,22 +1,21 @@
     1.4  (*  Title:      Pure/display.ML
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6 -    Copyright   1993  University of Cambridge
     1.7 +    Author:     Makarius
     1.8  
     1.9 -Printing of theorems, goals, results etc.
    1.10 +Printing of theorems, results etc.
    1.11  *)
    1.12  
    1.13  signature BASIC_DISPLAY =
    1.14  sig
    1.15    val goals_limit: int ref
    1.16 +  val show_consts: bool ref
    1.17    val show_hyps: bool ref
    1.18    val show_tags: bool ref
    1.19 -  val show_consts: bool ref
    1.20  end;
    1.21  
    1.22  signature DISPLAY =
    1.23  sig
    1.24    include BASIC_DISPLAY
    1.25 -  val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
    1.26    val pretty_thm_aux: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
    1.27      term list -> thm -> Pretty.T
    1.28    val pretty_thm: thm -> Pretty.T
    1.29 @@ -37,27 +36,26 @@
    1.30    val print_cterm: cterm -> unit
    1.31    val print_syntax: theory -> unit
    1.32    val pretty_full_theory: bool -> theory -> Pretty.T list
    1.33 -  val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
    1.34 -  val pretty_goals: int -> thm -> Pretty.T list
    1.35 -  val print_goals: int -> thm -> unit
    1.36  end;
    1.37  
    1.38  structure Display: DISPLAY =
    1.39  struct
    1.40  
    1.41 +(** options **)
    1.42 +
    1.43 +val goals_limit = Display_Goal.goals_limit;
    1.44 +val show_consts = Display_Goal.show_consts;
    1.45 +
    1.46 +val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
    1.47 +val show_tags = ref false;      (*false: suppress tags*)
    1.48 +
    1.49 +
    1.50  
    1.51  (** print thm **)
    1.52  
    1.53 -val goals_limit = ref 10;       (*max number of goals to print*)
    1.54 -val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
    1.55 -val show_tags = ref false;      (*false: suppress tags*)
    1.56 -
    1.57  fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
    1.58  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    1.59  
    1.60 -fun pretty_flexpair pp (t, u) = Pretty.block
    1.61 -  [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
    1.62 -
    1.63  fun display_status false _ = ""
    1.64    | display_status true th =
    1.65        let
    1.66 @@ -89,7 +87,7 @@
    1.67        if hlen = 0 andalso status = "" then []
    1.68        else if ! show_hyps orelse show_hyps' then
    1.69          [Pretty.brk 2, Pretty.list "[" "]"
    1.70 -          (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
    1.71 +          (map (q o Display_Goal.pretty_flexpair pp) tpairs @ map prt_term hyps' @
    1.72             map (Pretty.sort pp) xshyps @
    1.73              (if status = "" then [] else [Pretty.str status]))]
    1.74        else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
    1.75 @@ -242,109 +240,7 @@
    1.76           Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]]
    1.77    end;
    1.78  
    1.79 -
    1.80 -
    1.81 -(** print_goals **)
    1.82 -
    1.83 -(* print_goals etc. *)
    1.84 -
    1.85 -val show_consts = ref false;  (*true: show consts with types in proof state output*)
    1.86 -
    1.87 -
    1.88 -(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
    1.89 -
    1.90 -local
    1.91 -
    1.92 -fun ins_entry (x, y) =
    1.93 -  AList.default (op =) (x, []) #>
    1.94 -  AList.map_entry (op =) x (insert (op =) y);
    1.95 -
    1.96 -val add_consts = Term.fold_aterms
    1.97 -  (fn Const (c, T) => ins_entry (T, (c, T))
    1.98 -    | _ => I);
    1.99 -
   1.100 -val add_vars = Term.fold_aterms
   1.101 -  (fn Free (x, T) => ins_entry (T, (x, ~1))
   1.102 -    | Var (xi, T) => ins_entry (T, xi)
   1.103 -    | _ => I);
   1.104 -
   1.105 -val add_varsT = Term.fold_atyps
   1.106 -  (fn TFree (x, S) => ins_entry (S, (x, ~1))
   1.107 -    | TVar (xi, S) => ins_entry (S, xi)
   1.108 -    | _ => I);
   1.109 -
   1.110 -fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
   1.111 -fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
   1.112 -
   1.113 -fun consts_of t = sort_cnsts (add_consts t []);
   1.114 -fun vars_of t = sort_idxs (add_vars t []);
   1.115 -fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
   1.116 -
   1.117 -in
   1.118 -
   1.119 -fun pretty_goals_aux pp markup (msg, main) maxgoals state =
   1.120 -  let
   1.121 -    fun prt_atoms prt prtT (X, xs) = Pretty.block
   1.122 -      [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
   1.123 -        Pretty.brk 1, prtT X];
   1.124 -
   1.125 -    fun prt_var (x, ~1) = Pretty.term pp (Syntax.free x)
   1.126 -      | prt_var xi = Pretty.term pp (Syntax.var xi);
   1.127 -
   1.128 -    fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
   1.129 -      | prt_varT xi = Pretty.typ pp (TVar (xi, []));
   1.130 -
   1.131 -    val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp);
   1.132 -    val prt_vars = prt_atoms prt_var (Pretty.typ pp);
   1.133 -    val prt_varsT = prt_atoms prt_varT (Pretty.sort pp);
   1.134 -
   1.135 -
   1.136 -    fun pretty_list _ _ [] = []
   1.137 -      | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
   1.138 -
   1.139 -    fun pretty_subgoal (n, A) = Pretty.markup markup
   1.140 -      [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A];
   1.141 -    fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
   1.142 -
   1.143 -    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp);
   1.144 -
   1.145 -    val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
   1.146 -    val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
   1.147 -    val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
   1.148 -
   1.149 -
   1.150 -    val {prop, tpairs, ...} = Thm.rep_thm state;
   1.151 -    val (As, B) = Logic.strip_horn prop;
   1.152 -    val ngoals = length As;
   1.153 -
   1.154 -    fun pretty_gs (types, sorts) =
   1.155 -      (if main then [Pretty.term pp B] else []) @
   1.156 -       (if ngoals = 0 then [Pretty.str "No subgoals!"]
   1.157 -        else if ngoals > maxgoals then
   1.158 -          pretty_subgoals (Library.take (maxgoals, As)) @
   1.159 -          (if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   1.160 -           else [])
   1.161 -        else pretty_subgoals As) @
   1.162 -      pretty_ffpairs tpairs @
   1.163 -      (if ! show_consts then pretty_consts prop else []) @
   1.164 -      (if types then pretty_vars prop else []) @
   1.165 -      (if sorts then pretty_varsT prop else []);
   1.166 -  in
   1.167 -    setmp show_no_free_types true
   1.168 -      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
   1.169 -        (setmp show_sorts false pretty_gs))
   1.170 -   (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   1.171 -  end;
   1.172 -
   1.173 -fun pretty_goals n th =
   1.174 -  pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
   1.175 -
   1.176 -val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
   1.177 -
   1.178  end;
   1.179  
   1.180 -
   1.181 -end;
   1.182 -
   1.183 -structure BasicDisplay: BASIC_DISPLAY = Display;
   1.184 -open BasicDisplay;
   1.185 +structure Basic_Display: BASIC_DISPLAY = Display;
   1.186 +open Basic_Display;