src/Pure/Isar/proof_display.ML
author wenzelm
Tue Sep 13 22:19:54 2005 +0200 (2005-09-13)
changeset 17369 dec2ddbb3edf
child 17756 d4a35f82fbb4
permissions -rw-r--r--
Printing of Isar proof elements etc.
wenzelm@17369
     1
(*  Title:      Pure/Isar/proof_display.ML
wenzelm@17369
     2
    ID:         $Id$
wenzelm@17369
     3
    Author:     Makarius
wenzelm@17369
     4
wenzelm@17369
     5
Printing of Isar proof configurations etc.
wenzelm@17369
     6
*)
wenzelm@17369
     7
wenzelm@17369
     8
signature PROOF_DISPLAY =
wenzelm@17369
     9
sig
wenzelm@17369
    10
  val string_of_rule: ProofContext.context -> string -> thm -> string
wenzelm@17369
    11
  val print_results: bool -> ProofContext.context ->
wenzelm@17369
    12
    ((string * string) * (string * thm list) list) -> unit
wenzelm@17369
    13
  val present_results: ProofContext.context ->
wenzelm@17369
    14
    ((string * string) * (string * thm list) list) -> unit
wenzelm@17369
    15
end
wenzelm@17369
    16
wenzelm@17369
    17
structure ProofDisplay: PROOF_DISPLAY =
wenzelm@17369
    18
struct
wenzelm@17369
    19
wenzelm@17369
    20
(* refinement rule *)
wenzelm@17369
    21
wenzelm@17369
    22
fun pretty_rule ctxt s thm =
wenzelm@17369
    23
  Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
wenzelm@17369
    24
    Pretty.fbrk, ProofContext.pretty_thm ctxt thm];
wenzelm@17369
    25
wenzelm@17369
    26
val string_of_rule = Pretty.string_of ooo pretty_rule;
wenzelm@17369
    27
wenzelm@17369
    28
wenzelm@17369
    29
(* results *)
wenzelm@17369
    30
wenzelm@17369
    31
local
wenzelm@17369
    32
wenzelm@17369
    33
fun pretty_facts ctxt =
wenzelm@17369
    34
  List.concat o (separate [Pretty.fbrk, Pretty.str "and "]) o
wenzelm@17369
    35
    map (single o ProofContext.pretty_fact ctxt);
wenzelm@17369
    36
wenzelm@17369
    37
fun pretty_results ctxt ((kind, ""), facts) =
wenzelm@17369
    38
      Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts)
wenzelm@17369
    39
  | pretty_results ctxt ((kind, name), [fact]) = Pretty.blk (1,
wenzelm@17369
    40
      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, ProofContext.pretty_fact ctxt fact])
wenzelm@17369
    41
  | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1,
wenzelm@17369
    42
      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
wenzelm@17369
    43
        Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
wenzelm@17369
    44
wenzelm@17369
    45
fun name_results "" res = res
wenzelm@17369
    46
  | name_results name res =
wenzelm@17369
    47
      let
wenzelm@17369
    48
        val n = length (List.concat (map #2 res));
wenzelm@17369
    49
        fun name_res (a, ths) i =
wenzelm@17369
    50
          let
wenzelm@17369
    51
            val m = length ths;
wenzelm@17369
    52
            val j = i + m;
wenzelm@17369
    53
          in
wenzelm@17369
    54
            if a <> "" then ((a, ths), j)
wenzelm@17369
    55
            else if m = n then ((name, ths), j)
wenzelm@17369
    56
            else if m = 1 then
wenzelm@17369
    57
              ((PureThy.string_of_thmref (NameSelection (name, [Single i])), ths), j)
wenzelm@17369
    58
            else ((PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths), j)
wenzelm@17369
    59
          end;
wenzelm@17369
    60
      in #1 (fold_map name_res res 1) end;
wenzelm@17369
    61
wenzelm@17369
    62
in
wenzelm@17369
    63
wenzelm@17369
    64
fun print_results true = Pretty.writeln oo pretty_results
wenzelm@17369
    65
  | print_results false = K (K ());
wenzelm@17369
    66
wenzelm@17369
    67
fun present_results ctxt ((kind, name), res) =
wenzelm@17369
    68
  if kind = "" orelse kind = Drule.internalK then ()
wenzelm@17369
    69
  else (print_results true ctxt ((kind, name), res);
wenzelm@17369
    70
    Context.setmp (SOME (ProofContext.theory_of ctxt))
wenzelm@17369
    71
      (Present.results kind) (name_results name res));
wenzelm@17369
    72
wenzelm@17369
    73
end;
wenzelm@17369
    74
wenzelm@17369
    75
end;