src/Pure/display.ML
changeset 30711 952fdbee1b48
parent 30409 6037cac149a1
child 30723 a3adc9a96a16
equal deleted inserted replaced
30710:77d4b1284d4c 30711:952fdbee1b48
    55 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    55 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    56 
    56 
    57 fun pretty_flexpair pp (t, u) = Pretty.block
    57 fun pretty_flexpair pp (t, u) = Pretty.block
    58   [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
    58   [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
    59 
    59 
       
    60 fun display_status th =
       
    61   let
       
    62     val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
       
    63     val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
       
    64   in
       
    65     if failed then "!!"
       
    66     else if oracle andalso unfinished then "!?"
       
    67     else if oracle then "!"
       
    68     else if unfinished then "?"
       
    69     else ""
       
    70   end;
       
    71 
    60 fun pretty_thm_aux pp quote show_hyps' asms raw_th =
    72 fun pretty_thm_aux pp quote show_hyps' asms raw_th =
    61   let
    73   let
    62     val th = Thm.strip_shyps raw_th;
    74     val th = Thm.strip_shyps raw_th;
    63     val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
    75     val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
    64     val xshyps = Thm.extra_shyps th;
    76     val xshyps = Thm.extra_shyps th;
    66 
    78 
    67     val q = if quote then Pretty.quote else I;
    79     val q = if quote then Pretty.quote else I;
    68     val prt_term = q o Pretty.term pp;
    80     val prt_term = q o Pretty.term pp;
    69 
    81 
    70     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;
    71 (* FIXME
    83     val status = display_status th;
    72     val ora' = Thm.oracle_of th andalso (! show_hyps orelse not (! quick_and_dirty)); *)
       
    73     val ora' = false;
       
    74 
    84 
    75     val hlen = length xshyps + length hyps' + length tpairs;
    85     val hlen = length xshyps + length hyps' + length tpairs;
    76     val hsymbs =
    86     val hsymbs =
    77       if hlen = 0 andalso not ora' then []
    87       if hlen = 0 andalso status = "" then []
    78       else if ! show_hyps orelse show_hyps' then
    88       else if ! show_hyps orelse show_hyps' then
    79         [Pretty.brk 2, Pretty.list "[" "]"
    89         [Pretty.brk 2, Pretty.list "[" "]"
    80           (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
    90           (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
    81            map (Pretty.sort pp) xshyps @
    91            map (Pretty.sort pp) xshyps @
    82             (if ora' then [Pretty.str "!"] else []))]
    92             (if status = "" then [] else [Pretty.str status]))]
    83       else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
    93       else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
    84         (if ora' then "!" else "") ^ "]")];
       
    85     val tsymbs =
    94     val tsymbs =
    86       if null tags orelse not (! show_tags) then []
    95       if null tags orelse not (! show_tags) then []
    87       else [Pretty.brk 1, pretty_tags tags];
    96       else [Pretty.brk 1, pretty_tags tags];
    88   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    97   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    89 
    98