src/Pure/display.ML
changeset 6889 adcf91ad5add
parent 6846 f2380295d4dd
child 6894 b92c2f0413b8
     1.1 --- a/src/Pure/display.ML	Fri Jul 02 19:04:32 1999 +0200
     1.2 +++ b/src/Pure/display.ML	Sat Jul 03 00:21:35 1999 +0200
     1.3 @@ -44,12 +44,19 @@
     1.4  val show_hyps = ref true;	(*false: print meta-hypotheses as dots*)
     1.5  val show_tags = ref false;	(*false: suppress tags*)
     1.6  
     1.7 +local
     1.8 +
     1.9  fun pretty_tag (name, args) = Pretty.strs (name :: args);
    1.10  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    1.11  
    1.12 +fun is_oracle (Thm.Oracle _) = true
    1.13 +  | is_oracle _ = false;
    1.14 +
    1.15 +fun ex_oracle (Join (der, ders)) = is_oracle der orelse exists ex_oracle ders;
    1.16 +
    1.17  fun pretty_thm_aux quote th =
    1.18    let
    1.19 -    val {sign, hyps, prop, ...} = rep_thm th;
    1.20 +    val {sign, hyps, prop, der, ...} = rep_thm th;
    1.21      val xshyps = Thm.extra_shyps th;
    1.22      val (_, tags) = Thm.get_name_tags th;
    1.23  
    1.24 @@ -60,17 +67,23 @@
    1.25        if hlen = 0 then []
    1.26        else if ! show_hyps then
    1.27          [Pretty.brk 2, Pretty.list "[" "]"
    1.28 -          (map prt_term hyps @ map (Sign.pretty_sort sign) xshyps)]
    1.29 -      else
    1.30 -        [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ "]")];
    1.31 +          (map prt_term hyps @ map (Sign.pretty_sort sign) xshyps @
    1.32 +            (if ex_oracle der then [Pretty.str "!"] else []))]
    1.33 +      else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
    1.34 +        (if ex_oracle der then "!" else "") ^ "]")];
    1.35      val tsymbs =
    1.36        if null tags orelse not (! show_tags) then []
    1.37        else [Pretty.brk 1, pretty_tags tags];
    1.38    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    1.39  
    1.40 +in
    1.41 +
    1.42  val pretty_thm_no_quote = pretty_thm_aux false;
    1.43  val pretty_thm = pretty_thm_aux true;
    1.44  
    1.45 +end;
    1.46 +
    1.47 +
    1.48  val string_of_thm = Pretty.string_of o pretty_thm;
    1.49  val pprint_thm = Pretty.pprint o pretty_thm;
    1.50