pretty_thm_aux etc.: explicit show_status flag;
authorwenzelm
Thu Mar 26 15:18:50 2009 +0100 (2009-03-26)
changeset 30723a3adc9a96a16
parent 30722 623d4831c8cf
child 30724 2e54e89bcce7
pretty_thm_aux etc.: explicit show_status flag;
src/Pure/Isar/proof_context.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/display.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 26 14:14:02 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 26 15:18:50 2009 +0100
     1.3 @@ -36,6 +36,9 @@
     1.4    val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
     1.5    val extern_fact: Proof.context -> string -> xstring
     1.6    val pretty_term_abbrev: Proof.context -> term -> Pretty.T
     1.7 +  val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
     1.8 +  val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
     1.9 +  val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
    1.10    val pretty_thm: Proof.context -> thm -> Pretty.T
    1.11    val pretty_thms: Proof.context -> thm list -> Pretty.T
    1.12    val pretty_fact: Proof.context -> string * thm list -> Pretty.T
    1.13 @@ -295,21 +298,28 @@
    1.14  
    1.15  fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
    1.16  
    1.17 -fun pretty_thm ctxt th =
    1.18 -  let val asms = map Thm.term_of (Assumption.all_assms_of ctxt)
    1.19 -  in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end;
    1.20 +fun pretty_thm_aux ctxt show_status th =
    1.21 +  let
    1.22 +    val flags = {quote = false, show_hyps = true, show_status = show_status};
    1.23 +    val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
    1.24 +  in Display.pretty_thm_aux (Syntax.pp ctxt) flags asms th end;
    1.25  
    1.26 -fun pretty_thms ctxt [th] = pretty_thm ctxt th
    1.27 -  | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
    1.28 +fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th
    1.29 +  | pretty_thms_aux ctxt flag ths =
    1.30 +      Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths));
    1.31  
    1.32  fun pretty_fact_name ctxt a = Pretty.block
    1.33    [Pretty.markup (Markup.fact a) [Pretty.str (extern_fact ctxt a)], Pretty.str ":"];
    1.34  
    1.35 -fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths
    1.36 -  | pretty_fact ctxt (a, [th]) = Pretty.block
    1.37 -      [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm ctxt th]
    1.38 -  | pretty_fact ctxt (a, ths) = Pretty.block
    1.39 -      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm ctxt) ths));
    1.40 +fun pretty_fact_aux ctxt flag ("", ths) = pretty_thms_aux ctxt flag ths
    1.41 +  | pretty_fact_aux ctxt flag (a, [th]) = Pretty.block
    1.42 +      [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm_aux ctxt flag th]
    1.43 +  | pretty_fact_aux ctxt flag (a, ths) = Pretty.block
    1.44 +      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm_aux ctxt flag) ths));
    1.45 +
    1.46 +fun pretty_thm ctxt = pretty_thm_aux ctxt true;
    1.47 +fun pretty_thms ctxt = pretty_thms_aux ctxt true;
    1.48 +fun pretty_fact ctxt = pretty_fact_aux ctxt true;
    1.49  
    1.50  val string_of_thm = Pretty.string_of oo pretty_thm;
    1.51  
     2.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Mar 26 14:14:02 2009 +0100
     2.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Mar 26 15:18:50 2009 +0100
     2.3 @@ -655,13 +655,9 @@
     2.4                                    text=[XML.Elem("pgml",[],
     2.5                                                   maps YXML.parse_body strings)] })
     2.6  
     2.7 -        fun string_of_thm th = Pretty.string_of
     2.8 -                                   (Display.pretty_thm_aux
     2.9 -                                        (Syntax.pp_global (Thm.theory_of_thm th))
    2.10 -                                        false (* quote *)
    2.11 -                                        false (* show hyps *)
    2.12 -                                        [] (* asms *)
    2.13 -                                        th)
    2.14 +        fun string_of_thm th = Pretty.string_of (Display.pretty_thm_aux
    2.15 +            (Syntax.pp_global (Thm.theory_of_thm th))
    2.16 +            {quote = false, show_hyps = false, show_status = true} [] th)
    2.17  
    2.18          fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)
    2.19  
     3.1 --- a/src/Pure/display.ML	Thu Mar 26 14:14:02 2009 +0100
     3.2 +++ b/src/Pure/display.ML	Thu Mar 26 15:18:50 2009 +0100
     3.3 @@ -17,7 +17,8 @@
     3.4  sig
     3.5    include BASIC_DISPLAY
     3.6    val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
     3.7 -  val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
     3.8 +  val pretty_thm_aux: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
     3.9 +    term list -> thm -> Pretty.T
    3.10    val pretty_thm: thm -> Pretty.T
    3.11    val string_of_thm: thm -> string
    3.12    val pretty_thms: thm list -> Pretty.T
    3.13 @@ -57,19 +58,20 @@
    3.14  fun pretty_flexpair pp (t, u) = Pretty.block
    3.15    [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
    3.16  
    3.17 -fun display_status th =
    3.18 -  let
    3.19 -    val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
    3.20 -    val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
    3.21 -  in
    3.22 -    if failed then "!!"
    3.23 -    else if oracle andalso unfinished then "!?"
    3.24 -    else if oracle then "!"
    3.25 -    else if unfinished then "?"
    3.26 -    else ""
    3.27 -  end;
    3.28 +fun display_status false _ = ""
    3.29 +  | display_status true th =
    3.30 +      let
    3.31 +        val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
    3.32 +        val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
    3.33 +      in
    3.34 +        if failed then "!!"
    3.35 +        else if oracle andalso unfinished then "!?"
    3.36 +        else if oracle then "!"
    3.37 +        else if unfinished then "?"
    3.38 +        else ""
    3.39 +      end;
    3.40  
    3.41 -fun pretty_thm_aux pp quote show_hyps' asms raw_th =
    3.42 +fun pretty_thm_aux pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
    3.43    let
    3.44      val th = Thm.strip_shyps raw_th;
    3.45      val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
    3.46 @@ -80,7 +82,7 @@
    3.47      val prt_term = q o Pretty.term pp;
    3.48  
    3.49      val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    3.50 -    val status = display_status th;
    3.51 +    val status = display_status show_status th;
    3.52  
    3.53      val hlen = length xshyps + length hyps' + length tpairs;
    3.54      val hsymbs =
    3.55 @@ -97,7 +99,8 @@
    3.56    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    3.57  
    3.58  fun pretty_thm th =
    3.59 -  pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th)) true false [] th;
    3.60 +  pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th))
    3.61 +    {quote = true, show_hyps = false, show_status = true} [] th;
    3.62  
    3.63  val string_of_thm = Pretty.string_of o pretty_thm;
    3.64