src/Pure/display.ML
changeset 16534 95460b6eb712
parent 16490 e10b0d5fa33a
child 16845 bedf7b5fb781
     1.1 --- a/src/Pure/display.ML	Wed Jun 22 19:41:18 2005 +0200
     1.2 +++ b/src/Pure/display.ML	Wed Jun 22 19:41:19 2005 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  
     1.5  (** print thm **)
     1.6  
     1.7 -val goals_limit = ref 10;       (*max number of goals to print -- set by user*)
     1.8 +val goals_limit = ref 10;       (*max number of goals to print*)
     1.9  val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
    1.10  val show_tags = ref false;      (*false: suppress tags*)
    1.11  
    1.12 @@ -113,13 +113,8 @@
    1.13  val print_thms = Pretty.writeln o pretty_thms;
    1.14  
    1.15  fun prth th = (print_thm th; th);
    1.16 -
    1.17 -(*Print and return a sequence of theorems, separated by blank lines. *)
    1.18 -fun prthq thseq =
    1.19 -  (Seq.print (fn _ => print_thm) 100000 thseq; thseq);
    1.20 -
    1.21 -(*Print and return a list of theorems, separated by blank lines. *)
    1.22 -fun prths ths = (List.app (fn th => (print_thm th; writeln "")) ths; ths);
    1.23 +fun prthq thq = (Seq.print (K print_thm) 100000 thq; thq);
    1.24 +fun prths ths = (prthq (Seq.of_list ths); ths);
    1.25  
    1.26  
    1.27  (* other printing commands *)
    1.28 @@ -207,20 +202,23 @@
    1.29  
    1.30      val clsses = NameSpace.extern_table (apsnd (Symtab.make o Graph.dest) classes);
    1.31      val tdecls = NameSpace.extern_table types;
    1.32 +    val arties = Symtab.dest arities
    1.33 +      |> Library.sort_wrt (NameSpace.extern (Sign.type_space thy) o #1);
    1.34      val cnsts = NameSpace.extern_table consts;
    1.35      val finals = NameSpace.extern_table (#1 consts, Defs.finals defs);
    1.36      val axms = NameSpace.extern_table axioms;
    1.37      val oras = NameSpace.extern_table oracles;
    1.38    in
    1.39      [Pretty.strs ("names:" :: Context.names_of thy),
    1.40 -      Pretty.strs ("data:" :: Context.theory_data thy),
    1.41 +      Pretty.strs ("theory data:" :: Context.theory_data_of thy),
    1.42 +      Pretty.strs ("proof data:" :: Context.proof_data_of thy),
    1.43        Pretty.strs ["name prefix:", NameSpace.path_of naming],
    1.44        Pretty.big_list "classes:" (map pretty_classrel clsses),
    1.45        pretty_default default,
    1.46        pretty_witness witness,
    1.47        Pretty.big_list "syntactic types:" (List.mapPartial (pretty_type true) tdecls),
    1.48        Pretty.big_list "logical types:" (List.mapPartial (pretty_type false) tdecls),
    1.49 -      Pretty.big_list "type arities:" (pretty_arities (Symtab.dest arities)),
    1.50 +      Pretty.big_list "type arities:" (pretty_arities arties),
    1.51        Pretty.big_list "consts:" (map pretty_const cnsts),
    1.52        Pretty.big_list "finals consts:" (map pretty_final finals),
    1.53        Pretty.big_list "axioms:" (map prt_axm axms),
    1.54 @@ -233,8 +231,7 @@
    1.55  
    1.56  (* print_goals etc. *)
    1.57  
    1.58 -(*show consts with types in proof state output?*)
    1.59 -val show_consts = ref false;
    1.60 +val show_consts = ref false;  (*true: show consts with types in proof state output*)
    1.61  
    1.62  
    1.63  (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)