equal
deleted
inserted
replaced
34 |
34 |
35 end |
35 end |
36 |
36 |
37 code_printing |
37 code_printing |
38 constant Debug.trace \<rightharpoonup> (Eval) "Output.tracing" |
38 constant Debug.trace \<rightharpoonup> (Eval) "Output.tracing" |
39 | constant Debug.flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- \<open>note indirection via antiquotation\<close> |
39 | constant Debug.flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" \<comment> \<open>note indirection via antiquotation\<close> |
40 | constant Debug.timing \<rightharpoonup> (Eval) "Timing.timeap'_msg" |
40 | constant Debug.timing \<rightharpoonup> (Eval) "Timing.timeap'_msg" |
41 |
41 |
42 code_reserved Eval Output Timing |
42 code_reserved Eval Output Timing |
43 |
43 |
44 end |
44 end |