src/Pure/display.ML
changeset 17475 d008d04068a1
parent 17468 7c040a5fd171
child 17704 f776b3bf4126
equal deleted inserted replaced
17474:e4cdb9f061fb 17475:d008d04068a1
    75 
    75 
    76     val q = if quote then Pretty.quote else I;
    76     val q = if quote then Pretty.quote else I;
    77     val prt_term = q o (Pretty.term pp);
    77     val prt_term = q o (Pretty.term pp);
    78 
    78 
    79     val hyps' = if ! show_hyps then hyps else fold (remove (op aconv)) asms hyps;
    79     val hyps' = if ! show_hyps then hyps else fold (remove (op aconv)) asms hyps;
       
    80     val ora' = ora andalso (! show_hyps orelse not (! quick_and_dirty));
    80     val hlen = length xshyps + length hyps' + length tpairs;
    81     val hlen = length xshyps + length hyps' + length tpairs;
    81     val hsymbs =
    82     val hsymbs =
    82       if hlen = 0 andalso not ora then []
    83       if hlen = 0 andalso not ora' then []
    83       else if ! show_hyps orelse show_hyps' then
    84       else if ! show_hyps orelse show_hyps' then
    84         [Pretty.brk 2, Pretty.list "[" "]"
    85         [Pretty.brk 2, Pretty.list "[" "]"
    85           (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
    86           (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
    86            map (Pretty.sort pp) xshyps @
    87            map (Pretty.sort pp) xshyps @
    87             (if ora then [Pretty.str "!"] else []))]
    88             (if ora' then [Pretty.str "!"] else []))]
    88       else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
    89       else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
    89         (if ora then "!" else "") ^ "]")];
    90         (if ora' then "!" else "") ^ "]")];
    90     val tsymbs =
    91     val tsymbs =
    91       if null tags orelse not (! show_tags) then []
    92       if null tags orelse not (! show_tags) then []
    92       else [Pretty.brk 1, pretty_tags tags];
    93       else [Pretty.brk 1, pretty_tags tags];
    93   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    94   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    94 
    95