src/Pure/display.ML
changeset 30723 a3adc9a96a16
parent 30711 952fdbee1b48
child 32089 568a23753e3a
     1.1 --- a/src/Pure/display.ML	Thu Mar 26 14:14:02 2009 +0100
     1.2 +++ b/src/Pure/display.ML	Thu Mar 26 15:18:50 2009 +0100
     1.3 @@ -17,7 +17,8 @@
     1.4  sig
     1.5    include BASIC_DISPLAY
     1.6    val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
     1.7 -  val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
     1.8 +  val pretty_thm_aux: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
     1.9 +    term list -> thm -> Pretty.T
    1.10    val pretty_thm: thm -> Pretty.T
    1.11    val string_of_thm: thm -> string
    1.12    val pretty_thms: thm list -> Pretty.T
    1.13 @@ -57,19 +58,20 @@
    1.14  fun pretty_flexpair pp (t, u) = Pretty.block
    1.15    [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
    1.16  
    1.17 -fun display_status th =
    1.18 -  let
    1.19 -    val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
    1.20 -    val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
    1.21 -  in
    1.22 -    if failed then "!!"
    1.23 -    else if oracle andalso unfinished then "!?"
    1.24 -    else if oracle then "!"
    1.25 -    else if unfinished then "?"
    1.26 -    else ""
    1.27 -  end;
    1.28 +fun display_status false _ = ""
    1.29 +  | display_status true th =
    1.30 +      let
    1.31 +        val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
    1.32 +        val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
    1.33 +      in
    1.34 +        if failed then "!!"
    1.35 +        else if oracle andalso unfinished then "!?"
    1.36 +        else if oracle then "!"
    1.37 +        else if unfinished then "?"
    1.38 +        else ""
    1.39 +      end;
    1.40  
    1.41 -fun pretty_thm_aux pp quote show_hyps' asms raw_th =
    1.42 +fun pretty_thm_aux pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
    1.43    let
    1.44      val th = Thm.strip_shyps raw_th;
    1.45      val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
    1.46 @@ -80,7 +82,7 @@
    1.47      val prt_term = q o Pretty.term pp;
    1.48  
    1.49      val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    1.50 -    val status = display_status th;
    1.51 +    val status = display_status show_status th;
    1.52  
    1.53      val hlen = length xshyps + length hyps' + length tpairs;
    1.54      val hsymbs =
    1.55 @@ -97,7 +99,8 @@
    1.56    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    1.57  
    1.58  fun pretty_thm th =
    1.59 -  pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th)) true false [] th;
    1.60 +  pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th))
    1.61 +    {quote = true, show_hyps = false, show_status = true} [] th;
    1.62  
    1.63  val string_of_thm = Pretty.string_of o pretty_thm;
    1.64