new display of theory stamps
authorpaulson
Sat Mar 26 18:20:29 2005 +0100 (2005-03-26 ago)
changeset 15633741deccec4e3
parent 15632 bb178a7a69c1
child 15634 bca33c49b083
new display of theory stamps
src/Pure/Isar/toplevel.ML
src/Pure/Thy/thy_info.ML
src/Pure/install_pp.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Mar 26 16:14:17 2005 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Mar 26 18:20:29 2005 +0100
     1.3 @@ -98,7 +98,7 @@
     1.4  
     1.5  fun pretty_context thy = [Pretty.block
     1.6    [Pretty.str "theory", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
     1.7 -    Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy]];
     1.8 +    Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]];
     1.9  
    1.10  fun pretty_prf prf = Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf);
    1.11  
     2.1 --- a/src/Pure/Thy/thy_info.ML	Sat Mar 26 16:14:17 2005 +0100
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Mar 26 18:20:29 2005 +0100
     2.3 @@ -47,6 +47,8 @@
     2.4    val end_theory: theory -> theory
     2.5    val finish: unit -> unit
     2.6    val register_theory: theory -> unit
     2.7 +  val pretty_theory: theory -> Pretty.T
     2.8 +  val pprint_theory: theory -> pprint_args -> unit
     2.9  end;
    2.10  
    2.11  structure ThyInfo: THY_INFO =
    2.12 @@ -165,6 +167,19 @@
    2.13      error (loader_msg "nothing known about theory" [name]);
    2.14  
    2.15  
    2.16 +(* pretty printing a theory: omit finished theories *)
    2.17 +
    2.18 +fun unfinished_names stamps =
    2.19 +    List.last (List.filter is_finished stamps) :: List.filter (not o is_finished) stamps;
    2.20 +
    2.21 +fun pretty_sg sg = 
    2.22 +      Pretty.str_list "{" "}" 
    2.23 +        (unfinished_names (List.filter known_thy (Sign.stamp_names_of sg)));
    2.24 +
    2.25 +val pretty_theory = pretty_sg o Theory.sign_of;
    2.26 +val pprint_theory = Pretty.pprint o pretty_theory;
    2.27 +
    2.28 +
    2.29  (* access theory *)
    2.30  
    2.31  fun lookup_theory name =
     3.1 --- a/src/Pure/install_pp.ML	Sat Mar 26 16:14:17 2005 +0100
     3.2 +++ b/src/Pure/install_pp.ML	Sat Mar 26 18:20:29 2005 +0100
     3.3 @@ -4,7 +4,7 @@
     3.4  Set up automatic toplevel pretty printing.
     3.5  *)
     3.6  
     3.7 -install_pp (make_pp ["Theory", "theory"] Display.pprint_theory);
     3.8 +install_pp (make_pp ["Theory", "theory"] ThyInfo.pprint_theory);
     3.9  install_pp (make_pp ["Thm", "thm"] Display.pprint_thm);
    3.10  install_pp (make_pp ["Thm", "cterm"] Display.pprint_cterm);
    3.11  install_pp (make_pp ["Thm", "ctyp"] Display.pprint_ctyp);