src/Pure/display.ML
changeset 32145 220c9e439d39
parent 32090 39acf19e9f3a
child 32187 cca43ca13f4f
equal deleted inserted replaced
32144:183c1010ac14 32145:220c9e439d39
    14 end;
    14 end;
    15 
    15 
    16 signature DISPLAY =
    16 signature DISPLAY =
    17 sig
    17 sig
    18   include BASIC_DISPLAY
    18   include BASIC_DISPLAY
    19   val pretty_thm_raw: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
    19   val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool, show_status: bool} ->
    20     term list -> thm -> Pretty.T
    20     thm -> Pretty.T
    21   val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
    21   val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
    22   val pretty_thm: Proof.context -> thm -> Pretty.T
    22   val pretty_thm: Proof.context -> thm -> Pretty.T
    23   val pretty_thm_global: theory -> thm -> Pretty.T
    23   val pretty_thm_global: theory -> thm -> Pretty.T
    24   val pretty_thm_without_context: thm -> Pretty.T
    24   val pretty_thm_without_context: thm -> Pretty.T
    25   val string_of_thm: Proof.context -> thm -> string
    25   val string_of_thm: Proof.context -> thm -> string
    66         else if oracle then "!"
    66         else if oracle then "!"
    67         else if unfinished then "?"
    67         else if unfinished then "?"
    68         else ""
    68         else ""
    69       end;
    69       end;
    70 
    70 
    71 fun pretty_thm_raw pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
    71 fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps', show_status} raw_th =
    72   let
    72   let
    73     val th = Thm.strip_shyps raw_th;
    73     val th = Thm.strip_shyps raw_th;
    74     val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
    74     val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
    75     val xshyps = Thm.extra_shyps th;
    75     val xshyps = Thm.extra_shyps th;
    76     val tags = Thm.get_tags th;
    76     val tags = Thm.get_tags th;
    77 
    77 
    78     val q = if quote then Pretty.quote else I;
    78     val q = if quote then Pretty.quote else I;
    79     val prt_term = q o Pretty.term pp;
    79     val prt_term = q o Syntax.pretty_term ctxt;
    80 
    80 
       
    81     val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
    81     val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    82     val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    82     val status = display_status show_status th;
    83     val status = display_status show_status th;
    83 
    84 
    84     val hlen = length xshyps + length hyps' + length tpairs;
    85     val hlen = length xshyps + length hyps' + length tpairs;
    85     val hsymbs =
    86     val hsymbs =
    86       if hlen = 0 andalso status = "" then []
    87       if hlen = 0 andalso status = "" then []
    87       else if ! show_hyps orelse show_hyps' then
    88       else if ! show_hyps orelse show_hyps' then
    88         [Pretty.brk 2, Pretty.list "[" "]"
    89         [Pretty.brk 2, Pretty.list "[" "]"
    89           (map (q o Display_Goal.pretty_flexpair pp) tpairs @ map prt_term hyps' @
    90           (map (q o Display_Goal.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
    90            map (Pretty.sort pp) xshyps @
    91            map (Syntax.pretty_sort ctxt) xshyps @
    91             (if status = "" then [] else [Pretty.str status]))]
    92             (if status = "" then [] else [Pretty.str status]))]
    92       else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
    93       else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
    93     val tsymbs =
    94     val tsymbs =
    94       if null tags orelse not (! show_tags) then []
    95       if null tags orelse not (! show_tags) then []
    95       else [Pretty.brk 1, pretty_tags tags];
    96       else [Pretty.brk 1, pretty_tags tags];
    96   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    97   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    97 
    98 
    98 fun pretty_thm_aux ctxt show_status th =
    99 fun pretty_thm_aux ctxt show_status =
    99   let
   100   pretty_thm_raw ctxt {quote = false, show_hyps = true, show_status = show_status};
   100     val flags = {quote = false, show_hyps = true, show_status = show_status};
       
   101     val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
       
   102   in pretty_thm_raw (Syntax.pp ctxt) flags asms th end;
       
   103 
       
   104 
   101 
   105 fun pretty_thm ctxt = pretty_thm_aux ctxt true;
   102 fun pretty_thm ctxt = pretty_thm_aux ctxt true;
   106 
   103 
   107 fun pretty_thm_global thy th =
   104 fun pretty_thm_global thy =
   108   pretty_thm_raw (Syntax.pp_global thy)
   105   pretty_thm_raw (Syntax.init_pretty_global thy)
   109     {quote = false, show_hyps = false, show_status = true} [] th;
   106     {quote = false, show_hyps = false, show_status = true};
   110 
   107 
   111 fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th;
   108 fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th;
   112 
   109 
   113 val string_of_thm = Pretty.string_of oo pretty_thm;
   110 val string_of_thm = Pretty.string_of oo pretty_thm;
   114 val string_of_thm_global = Pretty.string_of oo pretty_thm_global;
   111 val string_of_thm_global = Pretty.string_of oo pretty_thm_global;