src/Pure/display.ML
changeset 17475 d008d04068a1
parent 17468 7c040a5fd171
child 17704 f776b3bf4126
     1.1 --- a/src/Pure/display.ML	Sat Sep 17 19:17:33 2005 +0200
     1.2 +++ b/src/Pure/display.ML	Sat Sep 17 19:17:34 2005 +0200
     1.3 @@ -77,16 +77,17 @@
     1.4      val prt_term = q o (Pretty.term pp);
     1.5  
     1.6      val hyps' = if ! show_hyps then hyps else fold (remove (op aconv)) asms hyps;
     1.7 +    val ora' = ora andalso (! show_hyps orelse not (! quick_and_dirty));
     1.8      val hlen = length xshyps + length hyps' + length tpairs;
     1.9      val hsymbs =
    1.10 -      if hlen = 0 andalso not ora then []
    1.11 +      if hlen = 0 andalso not ora' then []
    1.12        else if ! show_hyps orelse show_hyps' then
    1.13          [Pretty.brk 2, Pretty.list "[" "]"
    1.14            (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
    1.15             map (Pretty.sort pp) xshyps @
    1.16 -            (if ora then [Pretty.str "!"] else []))]
    1.17 +            (if ora' then [Pretty.str "!"] else []))]
    1.18        else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
    1.19 -        (if ora then "!" else "") ^ "]")];
    1.20 +        (if ora' then "!" else "") ^ "]")];
    1.21      val tsymbs =
    1.22        if null tags orelse not (! show_tags) then []
    1.23        else [Pretty.brk 1, pretty_tags tags];