src/Pure/display.ML
changeset 30711 952fdbee1b48
parent 30409 6037cac149a1
child 30723 a3adc9a96a16
     1.1 --- a/src/Pure/display.ML	Tue Mar 24 19:37:50 2009 +0100
     1.2 +++ b/src/Pure/display.ML	Tue Mar 24 21:24:53 2009 +0100
     1.3 @@ -57,6 +57,18 @@
     1.4  fun pretty_flexpair pp (t, u) = Pretty.block
     1.5    [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
     1.6  
     1.7 +fun display_status th =
     1.8 +  let
     1.9 +    val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
    1.10 +    val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
    1.11 +  in
    1.12 +    if failed then "!!"
    1.13 +    else if oracle andalso unfinished then "!?"
    1.14 +    else if oracle then "!"
    1.15 +    else if unfinished then "?"
    1.16 +    else ""
    1.17 +  end;
    1.18 +
    1.19  fun pretty_thm_aux pp quote show_hyps' asms raw_th =
    1.20    let
    1.21      val th = Thm.strip_shyps raw_th;
    1.22 @@ -68,20 +80,17 @@
    1.23      val prt_term = q o Pretty.term pp;
    1.24  
    1.25      val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    1.26 -(* FIXME
    1.27 -    val ora' = Thm.oracle_of th andalso (! show_hyps orelse not (! quick_and_dirty)); *)
    1.28 -    val ora' = false;
    1.29 +    val status = display_status th;
    1.30  
    1.31      val hlen = length xshyps + length hyps' + length tpairs;
    1.32      val hsymbs =
    1.33 -      if hlen = 0 andalso not ora' then []
    1.34 +      if hlen = 0 andalso status = "" then []
    1.35        else if ! show_hyps orelse show_hyps' then
    1.36          [Pretty.brk 2, Pretty.list "[" "]"
    1.37            (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
    1.38             map (Pretty.sort pp) xshyps @
    1.39 -            (if ora' then [Pretty.str "!"] else []))]
    1.40 -      else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
    1.41 -        (if ora' then "!" else "") ^ "]")];
    1.42 +            (if status = "" then [] else [Pretty.str status]))]
    1.43 +      else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
    1.44      val tsymbs =
    1.45        if null tags orelse not (! show_tags) then []
    1.46        else [Pretty.brk 1, pretty_tags tags];