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