src/Pure/display.ML
changeset 30723 a3adc9a96a16
parent 30711 952fdbee1b48
child 32089 568a23753e3a
equal deleted inserted replaced
30722:623d4831c8cf 30723:a3adc9a96a16
    15 
    15 
    16 signature DISPLAY =
    16 signature DISPLAY =
    17 sig
    17 sig
    18   include BASIC_DISPLAY
    18   include BASIC_DISPLAY
    19   val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
    19   val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
    20   val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
    20   val pretty_thm_aux: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
       
    21     term list -> thm -> Pretty.T
    21   val pretty_thm: thm -> Pretty.T
    22   val pretty_thm: thm -> Pretty.T
    22   val string_of_thm: thm -> string
    23   val string_of_thm: thm -> string
    23   val pretty_thms: thm list -> Pretty.T
    24   val pretty_thms: thm list -> Pretty.T
    24   val pretty_thm_sg: theory -> thm -> Pretty.T
    25   val pretty_thm_sg: theory -> thm -> Pretty.T
    25   val pretty_thms_sg: theory -> thm list -> Pretty.T
    26   val pretty_thms_sg: theory -> thm list -> Pretty.T
    55 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    56 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    56 
    57 
    57 fun pretty_flexpair pp (t, u) = Pretty.block
    58 fun pretty_flexpair pp (t, u) = Pretty.block
    58   [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
    59   [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
    59 
    60 
    60 fun display_status th =
    61 fun display_status false _ = ""
    61   let
    62   | display_status true th =
    62     val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
    63       let
    63     val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
    64         val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
    64   in
    65         val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
    65     if failed then "!!"
    66       in
    66     else if oracle andalso unfinished then "!?"
    67         if failed then "!!"
    67     else if oracle then "!"
    68         else if oracle andalso unfinished then "!?"
    68     else if unfinished then "?"
    69         else if oracle then "!"
    69     else ""
    70         else if unfinished then "?"
    70   end;
    71         else ""
    71 
    72       end;
    72 fun pretty_thm_aux pp quote show_hyps' asms raw_th =
    73 
       
    74 fun pretty_thm_aux pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
    73   let
    75   let
    74     val th = Thm.strip_shyps raw_th;
    76     val th = Thm.strip_shyps raw_th;
    75     val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
    77     val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
    76     val xshyps = Thm.extra_shyps th;
    78     val xshyps = Thm.extra_shyps th;
    77     val tags = Thm.get_tags th;
    79     val tags = Thm.get_tags th;
    78 
    80 
    79     val q = if quote then Pretty.quote else I;
    81     val q = if quote then Pretty.quote else I;
    80     val prt_term = q o Pretty.term pp;
    82     val prt_term = q o Pretty.term pp;
    81 
    83 
    82     val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    84     val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    83     val status = display_status th;
    85     val status = display_status show_status th;
    84 
    86 
    85     val hlen = length xshyps + length hyps' + length tpairs;
    87     val hlen = length xshyps + length hyps' + length tpairs;
    86     val hsymbs =
    88     val hsymbs =
    87       if hlen = 0 andalso status = "" then []
    89       if hlen = 0 andalso status = "" then []
    88       else if ! show_hyps orelse show_hyps' then
    90       else if ! show_hyps orelse show_hyps' then
    95       if null tags orelse not (! show_tags) then []
    97       if null tags orelse not (! show_tags) then []
    96       else [Pretty.brk 1, pretty_tags tags];
    98       else [Pretty.brk 1, pretty_tags tags];
    97   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    99   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    98 
   100 
    99 fun pretty_thm th =
   101 fun pretty_thm th =
   100   pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th)) true false [] th;
   102   pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th))
       
   103     {quote = true, show_hyps = false, show_status = true} [] th;
   101 
   104 
   102 val string_of_thm = Pretty.string_of o pretty_thm;
   105 val string_of_thm = Pretty.string_of o pretty_thm;
   103 
   106 
   104 fun pretty_thms [th] = pretty_thm th
   107 fun pretty_thms [th] = pretty_thm th
   105   | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
   108   | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));