src/Pure/display.ML
changeset 6087 c8ec08fced15
parent 5902 c39b23d752b6
child 6279 eb4dc43023af
     1.1 --- a/src/Pure/display.ML	Tue Jan 12 12:30:42 1999 +0100
     1.2 +++ b/src/Pure/display.ML	Tue Jan 12 13:14:22 1999 +0100
     1.3 @@ -9,10 +9,13 @@
     1.4  signature DISPLAY =
     1.5  sig
     1.6    val show_hyps		: bool ref
     1.7 +  val show_tags		: bool ref
     1.8    val pretty_thm	: thm -> Pretty.T
     1.9 +  val pretty_thms	: thm list -> Pretty.T
    1.10    val string_of_thm	: thm -> string
    1.11    val pprint_thm	: thm -> pprint_args -> unit
    1.12    val print_thm		: thm -> unit
    1.13 +  val print_thms	: thm list -> unit
    1.14    val prth		: thm -> thm
    1.15    val prthq		: thm Seq.seq -> thm Seq.seq
    1.16    val prths		: thm list -> thm list
    1.17 @@ -30,19 +33,25 @@
    1.18    val print_theory	: theory -> unit
    1.19    val pretty_name_space : string * NameSpace.T -> Pretty.T
    1.20    val show_consts	: bool ref
    1.21 -
    1.22  end;
    1.23  
    1.24  structure Display: DISPLAY =
    1.25  struct
    1.26  
    1.27 -(*If false, hypotheses are printed as dots*)
    1.28 -val show_hyps = ref true;
    1.29 +(** print thm **)
    1.30 +
    1.31 +val show_hyps = ref true;	(*false: print meta-hypotheses as dots*)
    1.32 +val show_tags = ref false;	(*false: suppress tags*)
    1.33 +
    1.34 +fun pretty_tag (name, args) = Pretty.strs (name :: args);
    1.35 +val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    1.36  
    1.37  fun pretty_thm th =
    1.38    let
    1.39      val {sign, hyps, prop, ...} = rep_thm th;
    1.40 -    val xshyps = extra_shyps th;
    1.41 +    val xshyps = Thm.extra_shyps th;
    1.42 +    val (_, tags) = Thm.get_name_tags th;
    1.43 +
    1.44      val hlen = length xshyps + length hyps;
    1.45      val hsymbs =
    1.46        if hlen = 0 then []
    1.47 @@ -52,16 +61,22 @@
    1.48             map (Sign.pretty_sort sign) xshyps)]
    1.49        else
    1.50          [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ "]")];
    1.51 -  in
    1.52 -    Pretty.block (Sign.pretty_term sign prop :: hsymbs)
    1.53 -  end;
    1.54 +    val tsymbs =
    1.55 +      if null tags orelse not (! show_tags) then []
    1.56 +      else [Pretty.brk 1, pretty_tags tags];
    1.57 +  in Pretty.block (Sign.pretty_term sign prop :: (hsymbs @ tsymbs)) end;
    1.58  
    1.59  val string_of_thm = Pretty.string_of o pretty_thm;
    1.60  val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm;
    1.61  
    1.62 +fun pretty_thms [th] = pretty_thm th
    1.63 +  | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
    1.64  
    1.65 -(** Top-level commands for printing theorems **)
    1.66 -val print_thm = writeln o string_of_thm;
    1.67 +
    1.68 +(* top-level commands for printing theorems *)
    1.69 +
    1.70 +val print_thm = Pretty.writeln o pretty_thm;
    1.71 +val print_thms = Pretty.writeln o pretty_thms;
    1.72  
    1.73  fun prth th = (print_thm th; th);
    1.74