src/Pure/display.ML
changeset 26939 1035c89b4c02
parent 26928 ca87aff1ad2d
child 27302 8d12ac6a3e1c
equal deleted inserted replaced
26938:64e850c3da9e 26939:1035c89b4c02
    84       if null tags orelse not (! show_tags) then []
    84       if null tags orelse not (! show_tags) then []
    85       else [Pretty.brk 1, pretty_tags tags];
    85       else [Pretty.brk 1, pretty_tags tags];
    86   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    86   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    87 
    87 
    88 fun pretty_thm th =
    88 fun pretty_thm th =
    89   pretty_thm_aux (Sign.pp (Thm.theory_of_thm th)) true false [] th;
    89   pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th)) true false [] th;
    90 
    90 
    91 val string_of_thm = Pretty.string_of o pretty_thm;
    91 val string_of_thm = Pretty.string_of o pretty_thm;
    92 
    92 
    93 fun pretty_thms [th] = pretty_thm th
    93 fun pretty_thms [th] = pretty_thm th
    94   | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
    94   | pretty_thms ths = Pretty.block (Pretty.fbreaks (map pretty_thm ths));
   107 fun prths ths = (prthq (Seq.of_list ths); ths);
   107 fun prths ths = (prthq (Seq.of_list ths); ths);
   108 
   108 
   109 
   109 
   110 (* other printing commands *)
   110 (* other printing commands *)
   111 
   111 
   112 fun pretty_ctyp cT = Sign.pretty_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
   112 fun pretty_ctyp cT = Syntax.pretty_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
   113 fun string_of_ctyp cT = Sign.string_of_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
   113 fun string_of_ctyp cT = Syntax.string_of_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
   114 val print_ctyp = writeln o string_of_ctyp;
   114 val print_ctyp = writeln o string_of_ctyp;
   115 
   115 
   116 fun pretty_cterm ct = Sign.pretty_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
   116 fun pretty_cterm ct = Syntax.pretty_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
   117 fun string_of_cterm ct = Sign.string_of_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
   117 fun string_of_cterm ct = Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
   118 val print_cterm = writeln o string_of_cterm;
   118 val print_cterm = writeln o string_of_cterm;
   119 
   119 
   120 
   120 
   121 
   121 
   122 (** print theory **)
   122 (** print theory **)
   136     fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
   136     fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
   137     val prt_typ_no_tvars = prt_typ o Logic.unvarifyT;
   137     val prt_typ_no_tvars = prt_typ o Logic.unvarifyT;
   138     fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
   138     fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
   139     val prt_term_no_vars = prt_term o Logic.unvarify;
   139     val prt_term_no_vars = prt_term o Logic.unvarify;
   140     fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
   140     fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
   141     val prt_const' = Defs.pretty_const (Sign.pp thy);
   141     val prt_const' = Defs.pretty_const (Syntax.pp ctxt);
   142 
   142 
   143     fun pretty_classrel (c, []) = prt_cls c
   143     fun pretty_classrel (c, []) = prt_cls c
   144       | pretty_classrel (c, cs) = Pretty.block
   144       | pretty_classrel (c, cs) = Pretty.block
   145           (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 ::
   145           (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 ::
   146             Pretty.commas (map prt_cls cs));
   146             Pretty.commas (map prt_cls cs));
   324         (setmp show_sorts false pretty_gs))
   324         (setmp show_sorts false pretty_gs))
   325    (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   325    (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   326   end;
   326   end;
   327 
   327 
   328 fun pretty_goals n th =
   328 fun pretty_goals n th =
   329   pretty_goals_aux (Sign.pp (Thm.theory_of_thm th)) Markup.none (true, true) n th;
   329   pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
   330 
   330 
   331 val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
   331 val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
   332 
   332 
   333 end;
   333 end;
   334 
   334