src/Pure/Isar/proof_display.ML
changeset 28092 5886e9359aa8
parent 28087 a9cccdd9d521
child 28210 c164d1892553
     1.1 --- a/src/Pure/Isar/proof_display.ML	Tue Sep 02 21:31:28 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Tue Sep 02 22:20:16 2008 +0200
     1.3 @@ -5,15 +5,8 @@
     1.4  Printing of theorems, goals, results etc.
     1.5  *)
     1.6  
     1.7 -signature BASIC_PROOF_DISPLAY =
     1.8 -sig
     1.9 -  val print_theorems: theory -> unit
    1.10 -  val print_theory: theory -> unit
    1.11 -end
    1.12 -
    1.13  signature PROOF_DISPLAY =
    1.14  sig
    1.15 -  include BASIC_PROOF_DISPLAY
    1.16    val pprint_context: Proof.context -> pprint_args -> unit
    1.17    val pprint_typ: theory -> typ -> pprint_args -> unit
    1.18    val pprint_term: theory -> term -> pprint_args -> unit
    1.19 @@ -21,11 +14,11 @@
    1.20    val pprint_cterm: cterm -> pprint_args -> unit
    1.21    val pprint_thm: thm -> pprint_args -> unit
    1.22    val print_theorems_diff: theory -> theory -> unit
    1.23 +  val print_theorems: theory -> unit
    1.24    val pretty_full_theory: bool -> theory -> Pretty.T
    1.25 +  val print_theory: theory -> unit
    1.26    val string_of_rule: Proof.context -> string -> thm -> string
    1.27    val print_results: bool -> Proof.context -> ((string * string) * (string * thm list) list) -> unit
    1.28 -  val add_hook: ((string * thm list) list -> unit) -> unit
    1.29 -  val theory_results: Proof.context -> ((string * string) * (string * thm list) list) -> unit
    1.30    val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
    1.31  end
    1.32  
    1.33 @@ -79,69 +72,28 @@
    1.34  
    1.35  (* results *)
    1.36  
    1.37 +local
    1.38 +
    1.39  fun pretty_fact_name (kind, "") = Pretty.str kind
    1.40    | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
    1.41        Pretty.str (NameSpace.base name), Pretty.str ":"];
    1.42  
    1.43 -local
    1.44 -
    1.45  fun pretty_facts ctxt =
    1.46    flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
    1.47      map (single o ProofContext.pretty_fact ctxt);
    1.48  
    1.49 -fun pretty_results ctxt ((kind, ""), facts) =
    1.50 -      Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts)
    1.51 -  | pretty_results ctxt (kind_name, [fact]) = Pretty.blk (1,
    1.52 -      [pretty_fact_name kind_name, Pretty.fbrk, ProofContext.pretty_fact ctxt fact])
    1.53 -  | pretty_results ctxt (kind_name, facts) = Pretty.blk (1,
    1.54 -      [pretty_fact_name kind_name, Pretty.fbrk, Pretty.blk (1,
    1.55 -        Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
    1.56 -
    1.57  in
    1.58  
    1.59 -fun print_results true = Pretty.writeln oo pretty_results
    1.60 -  | print_results false = K (K ());
    1.61 -
    1.62 -end;
    1.63 -
    1.64 -
    1.65 -(* theory results -- subject to hook *)
    1.66 -
    1.67 -local val hooks = ref ([]: ((string * thm list) list -> unit) list) in
    1.68 -
    1.69 -fun add_hook f = CRITICAL (fn () => change hooks (cons f));
    1.70 -fun get_hooks () = CRITICAL (fn () => ! hooks);
    1.71 -
    1.72 -end;
    1.73 -
    1.74 -local
    1.75 -
    1.76 -fun name_results "" res = res
    1.77 -  | name_results name res =
    1.78 -      let
    1.79 -        val n = length (maps snd res);
    1.80 -        fun name_res (a, ths) i =
    1.81 -          let
    1.82 -            val m = length ths;
    1.83 -            val j = i + m;
    1.84 -          in
    1.85 -            if a <> "" then ((a, ths), j)
    1.86 -            else if m = n then ((name, ths), j)
    1.87 -            else ((Facts.string_of_ref (Facts.Named ((name, Position.none),
    1.88 -              SOME ([if m = 1 then Facts.Single i else Facts.FromTo (i, j - 1)]))), ths), j)
    1.89 -          end;
    1.90 -      in fst (fold_map name_res res 1) end;
    1.91 -
    1.92 -in
    1.93 -
    1.94 -fun theory_results ctxt ((kind, name), res) =
    1.95 -  if kind = "" orelse kind = Thm.internalK then ()
    1.96 -  else
    1.97 -    let
    1.98 -      val _ = print_results true ctxt ((kind, name), res);
    1.99 -      val res' = name_results name res;
   1.100 -      val _ = List.app (fn f => f res') (get_hooks ());
   1.101 -    in () end;
   1.102 +fun print_results do_print ctxt ((kind, name), facts) =
   1.103 +  if not do_print orelse kind = "" orelse kind = Thm.internalK then ()
   1.104 +  else if name = "" then
   1.105 +    Pretty.writeln (Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
   1.106 +  else Pretty.writeln
   1.107 +    (case facts of
   1.108 +      [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
   1.109 +        ProofContext.pretty_fact ctxt fact])
   1.110 +    | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
   1.111 +        Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
   1.112  
   1.113  end;
   1.114  
   1.115 @@ -166,6 +118,3 @@
   1.116  end;
   1.117  
   1.118  end;
   1.119 -
   1.120 -structure BasicProofDisplay: BASIC_PROOF_DISPLAY = ProofDisplay;
   1.121 -open BasicProofDisplay;