src/Pure/Isar/proof_context.ML
changeset 6721 dcee829f8e21
parent 6560 1436349f8b28
child 6762 a9a515a43ae0
equal deleted inserted replaced
6720:353bd9b74b1f 6721:dcee829f8e21
   111 
   111 
   112 fun print_items prt name items =
   112 fun print_items prt name items =
   113   let
   113   let
   114     fun pretty_itms (name, [x]) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt x]
   114     fun pretty_itms (name, [x]) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt x]
   115       | pretty_itms (name, xs) = Pretty.big_list (name ^ ":") (map prt xs);
   115       | pretty_itms (name, xs) = Pretty.big_list (name ^ ":") (map prt xs);
   116   in Pretty.writeln (Pretty.big_list name (map pretty_itms items)) end;
   116   in
       
   117     if null items andalso not (! verbose) then ()
       
   118     else Pretty.writeln (Pretty.big_list name (map pretty_itms items))
       
   119   end;
   117 
   120 
   118 
   121 
   119 (* term bindings *)
   122 (* term bindings *)
   120 
   123 
   121 fun print_binds (Context {thy, binds, ...}) =
   124 fun print_binds (Context {thy, binds, ...}) =
   126       (case try Syntax.dest_binding x of
   129       (case try Syntax.dest_binding x of
   127         None => Syntax.string_of_vname (x, i)
   130         None => Syntax.string_of_vname (x, i)
   128       | Some x' => if i = 0 then "??" ^ x' else Syntax.string_of_vname (x, i));
   131       | Some x' => if i = 0 then "??" ^ x' else Syntax.string_of_vname (x, i));
   129     fun pretty_bind (xi, (t, T)) = Pretty.block
   132     fun pretty_bind (xi, (t, T)) = Pretty.block
   130       [Pretty.str (fix_var xi), Pretty.str " ==", Pretty.brk 1, prt_term t];
   133       [Pretty.str (fix_var xi), Pretty.str " ==", Pretty.brk 1, prt_term t];
   131   in Pretty.writeln (Pretty.big_list "Term bindings:" (map pretty_bind (Vartab.dest binds))) end;
   134   in
       
   135     if Vartab.is_empty binds andalso not (! verbose) then ()
       
   136     else Pretty.writeln (Pretty.big_list "Term bindings:" (map pretty_bind (Vartab.dest binds)))
       
   137   end;
   132 
   138 
   133 
   139 
   134 (* local theorems *)
   140 (* local theorems *)
   135 
   141 
   136 fun print_thms (Context {thms, ...}) =
   142 fun print_thms (Context {thms, ...}) =
   167 
   173 
   168     val prt_defT = prt_atom prt_var prt_typ;
   174     val prt_defT = prt_atom prt_var prt_typ;
   169     val prt_defS = prt_atom prt_varT prt_sort;
   175     val prt_defS = prt_atom prt_varT prt_sort;
   170   in
   176   in
   171     verb Pretty.writeln pretty_thy;
   177     verb Pretty.writeln pretty_thy;
   172     Pretty.writeln (Pretty.big_list "Fixed variables:" (map prt_fix (rev fixes)));
   178     if null fixes andalso not (! verbose) then ()
       
   179     else Pretty.writeln (Pretty.big_list "Fixed variables:" (map prt_fix (rev fixes)));
   173     print_items (prt_term o #prop o Thm.rep_thm) "Assumptions:" assumes;
   180     print_items (prt_term o #prop o Thm.rep_thm) "Assumptions:" assumes;
   174     verb print_binds ctxt;
   181     verb print_binds ctxt;
   175     verb print_thms ctxt;
   182     verb print_thms ctxt;
   176     verb Pretty.writeln (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types)));
   183     verb Pretty.writeln (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types)));
   177     verb Pretty.writeln (Pretty.big_list "Default sorts:" (map prt_defS (Vartab.dest sorts)));
   184     verb Pretty.writeln (Pretty.big_list "Default sorts:" (map prt_defS (Vartab.dest sorts)));