equal
deleted
inserted
replaced
177 |
177 |
178 (FIXME Mention how to work with @{ML_ind debug in Toplevel} and |
178 (FIXME Mention how to work with @{ML_ind debug in Toplevel} and |
179 @{ML_ind profiling in Toplevel}.) |
179 @{ML_ind profiling in Toplevel}.) |
180 *} |
180 *} |
181 |
181 |
182 (* |
182 (* FIXME |
183 ML {* reset Toplevel.debug *} |
183 ML {* reset Toplevel.debug *} |
184 |
184 |
185 ML {* fun dodgy_fun () = (raise TYPE ("",[],[]); 1) *} |
185 ML {* fun dodgy_fun () = (raise TYPE ("",[],[]); 1) *} |
186 |
186 |
187 ML {* fun innocent () = dodgy_fun () *} |
187 ML {* fun innocent () = dodgy_fun () *} |
829 therefore we are not interested in them in this Tutorial, except in |
829 therefore we are not interested in them in this Tutorial, except in |
830 Appendix \ref{rec:docantiquotations} where we show how to implement your |
830 Appendix \ref{rec:docantiquotations} where we show how to implement your |
831 own document antiquotations. |
831 own document antiquotations. |
832 *} |
832 *} |
833 |
833 |
|
834 (* |
|
835 section {* Do Not Try This At Home! *} |
|
836 |
|
837 ML {* val my_thms = ref ([]: thm list) *} |
|
838 |
|
839 attribute_setup my_thm_bad = |
|
840 {* Scan.succeed (Thm.declaration_attribute (fn th => fn ctxt => |
|
841 (my_thms := th :: ! my_thms; ctxt))) *} "bad attribute" |
|
842 |
|
843 declare sym [my_thm_bad] |
|
844 declare refl [my_thm_bad] |
|
845 |
|
846 ML "!my_thms" |
|
847 *) |
834 end |
848 end |