src/Pure/display.ML
changeset 6889 adcf91ad5add
parent 6846 f2380295d4dd
child 6894 b92c2f0413b8
equal deleted inserted replaced
6888:d0c68ebdabc5 6889:adcf91ad5add
    42 (** print thm **)
    42 (** print thm **)
    43 
    43 
    44 val show_hyps = ref true;	(*false: print meta-hypotheses as dots*)
    44 val show_hyps = ref true;	(*false: print meta-hypotheses as dots*)
    45 val show_tags = ref false;	(*false: suppress tags*)
    45 val show_tags = ref false;	(*false: suppress tags*)
    46 
    46 
       
    47 local
       
    48 
    47 fun pretty_tag (name, args) = Pretty.strs (name :: args);
    49 fun pretty_tag (name, args) = Pretty.strs (name :: args);
    48 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    50 val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    49 
    51 
       
    52 fun is_oracle (Thm.Oracle _) = true
       
    53   | is_oracle _ = false;
       
    54 
       
    55 fun ex_oracle (Join (der, ders)) = is_oracle der orelse exists ex_oracle ders;
       
    56 
    50 fun pretty_thm_aux quote th =
    57 fun pretty_thm_aux quote th =
    51   let
    58   let
    52     val {sign, hyps, prop, ...} = rep_thm th;
    59     val {sign, hyps, prop, der, ...} = rep_thm th;
    53     val xshyps = Thm.extra_shyps th;
    60     val xshyps = Thm.extra_shyps th;
    54     val (_, tags) = Thm.get_name_tags th;
    61     val (_, tags) = Thm.get_name_tags th;
    55 
    62 
    56     val prt_term = (if quote then Pretty.quote else I) o Sign.pretty_term sign;
    63     val prt_term = (if quote then Pretty.quote else I) o Sign.pretty_term sign;
    57 
    64 
    58     val hlen = length xshyps + length hyps;
    65     val hlen = length xshyps + length hyps;
    59     val hsymbs =
    66     val hsymbs =
    60       if hlen = 0 then []
    67       if hlen = 0 then []
    61       else if ! show_hyps then
    68       else if ! show_hyps then
    62         [Pretty.brk 2, Pretty.list "[" "]"
    69         [Pretty.brk 2, Pretty.list "[" "]"
    63           (map prt_term hyps @ map (Sign.pretty_sort sign) xshyps)]
    70           (map prt_term hyps @ map (Sign.pretty_sort sign) xshyps @
    64       else
    71             (if ex_oracle der then [Pretty.str "!"] else []))]
    65         [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ "]")];
    72       else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
       
    73         (if ex_oracle der then "!" else "") ^ "]")];
    66     val tsymbs =
    74     val tsymbs =
    67       if null tags orelse not (! show_tags) then []
    75       if null tags orelse not (! show_tags) then []
    68       else [Pretty.brk 1, pretty_tags tags];
    76       else [Pretty.brk 1, pretty_tags tags];
    69   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    77   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    70 
    78 
       
    79 in
       
    80 
    71 val pretty_thm_no_quote = pretty_thm_aux false;
    81 val pretty_thm_no_quote = pretty_thm_aux false;
    72 val pretty_thm = pretty_thm_aux true;
    82 val pretty_thm = pretty_thm_aux true;
       
    83 
       
    84 end;
       
    85 
    73 
    86 
    74 val string_of_thm = Pretty.string_of o pretty_thm;
    87 val string_of_thm = Pretty.string_of o pretty_thm;
    75 val pprint_thm = Pretty.pprint o pretty_thm;
    88 val pprint_thm = Pretty.pprint o pretty_thm;
    76 
    89 
    77 fun pretty_thms [th] = pretty_thm th
    90 fun pretty_thms [th] = pretty_thm th