src/Pure/display.ML
changeset 20629 8f6cc81ba4a3
parent 20226 6ea469c03314
child 21646 c07b5b0e8492
     1.1 --- a/src/Pure/display.ML	Tue Sep 19 23:15:37 2006 +0200
     1.2 +++ b/src/Pure/display.ML	Tue Sep 19 23:15:38 2006 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4    val pretty_thms_sg: theory -> thm list -> Pretty.T
     1.5    val pretty_ctyp: ctyp -> Pretty.T
     1.6    val pretty_cterm: cterm -> Pretty.T
     1.7 -  val pretty_full_theory: theory -> Pretty.T list
     1.8 +  val pretty_full_theory: bool -> theory -> Pretty.T list
     1.9    val pretty_goals_aux: Pretty.pp -> string -> bool * bool -> int -> thm -> Pretty.T list
    1.10    val pretty_goals: int -> thm -> Pretty.T list
    1.11    val print_goals: int -> thm -> unit
    1.12 @@ -148,7 +148,7 @@
    1.13  
    1.14  (* pretty_full_theory *)
    1.15  
    1.16 -fun pretty_full_theory thy =
    1.17 +fun pretty_full_theory verbose thy =
    1.18    let
    1.19      fun prt_cls c = Sign.pretty_sort thy [c];
    1.20      fun prt_sort S = Sign.pretty_sort thy S;
    1.21 @@ -211,27 +211,33 @@
    1.22      val (class_space, class_algebra) = classes;
    1.23      val {classes, arities} = Sorts.rep_algebra class_algebra;
    1.24  
    1.25 -    val clsses = NameSpace.dest_table (class_space, Symtab.make (Graph.dest classes));
    1.26 -    val tdecls = NameSpace.dest_table types;
    1.27 -    val arties = NameSpace.dest_table (Sign.type_space thy, arities);
    1.28 -    val cnsts = NameSpace.extern_table constants;
    1.29 +    fun prune xs = if verbose then xs else filter_out (can Name.dest_internal o fst) xs;
    1.30 +    fun prune' xs = if verbose then xs else filter_out (can Name.dest_internal o fst o fst) xs;
    1.31 +    fun dest_table tab = prune (NameSpace.dest_table tab);
    1.32 +    fun extern_table tab = prune (NameSpace.extern_table tab);
    1.33 +
    1.34 +    val clsses = dest_table (class_space, Symtab.make (Graph.dest classes));
    1.35 +    val tdecls = dest_table types;
    1.36 +    val arties = dest_table (Sign.type_space thy, arities);
    1.37 +    val cnsts = extern_table constants;
    1.38      val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
    1.39      val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
    1.40 -    val cnstrs = NameSpace.extern_table constraints;
    1.41 -    val axms = NameSpace.extern_table axioms;
    1.42 -    val oras = NameSpace.extern_table oracles;
    1.43 +    val cnstrs = extern_table constraints;
    1.44 +    val axms = extern_table axioms;
    1.45 +    val oras = extern_table oracles;
    1.46  
    1.47 -    val (reds0, (reds1, reds2)) = reducts |> map (fn (lhs, rhs) =>
    1.48 -        (apfst extern_const lhs, map (apfst extern_const) rhs))
    1.49 +    val (reds0, (reds1, reds2)) = prune' reducts |> map (fn (lhs, rhs) =>
    1.50 +        (apfst extern_const lhs, map (apfst extern_const) (prune rhs)))
    1.51        |> sort_wrt (#1 o #1)
    1.52        |> List.partition (null o #2)
    1.53        ||> List.partition (Defs.plain_args o #2 o #1);
    1.54      val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
    1.55    in
    1.56 -    [Pretty.strs ("names:" :: Context.names_of thy),
    1.57 -      Pretty.strs ("theory data:" :: Context.theory_data_of thy),
    1.58 -      Pretty.strs ("proof data:" :: Context.proof_data_of thy),
    1.59 -      Pretty.strs ["name prefix:", NameSpace.path_of naming],
    1.60 +    [Pretty.strs ("names:" :: Context.names_of thy)] @
    1.61 +    (if verbose then
    1.62 +      [Pretty.strs ("theory data:" :: Context.theory_data_of thy),
    1.63 +       Pretty.strs ("proof data:" :: Context.proof_data_of thy)] else []) @
    1.64 +    [Pretty.strs ["name prefix:", NameSpace.path_of naming],
    1.65        Pretty.big_list "classes:" (map pretty_classrel clsses),
    1.66        pretty_default default,
    1.67        pretty_witness witness,