equal
deleted
inserted
replaced
2 imports Main LaTeXsugar |
2 imports Main LaTeXsugar |
3 uses |
3 uses |
4 "output_tutorial.ML" |
4 "output_tutorial.ML" |
5 "antiquote_setup.ML" |
5 "antiquote_setup.ML" |
6 begin |
6 begin |
|
7 |
|
8 (* rebinding of writeln and tracing so that it can *) |
|
9 (* be compared in intiquotations *) |
|
10 ML {* |
|
11 fun writeln s = (Output.writeln s; s) |
|
12 fun tracing s = (Output.tracing s; s) |
|
13 *} |
7 |
14 |
8 (* re-definition of various ML antiquotations *) |
15 (* re-definition of various ML antiquotations *) |
9 (* to have a special tag for text enclosed in ML *) |
16 (* to have a special tag for text enclosed in ML *) |
10 |
17 |
11 ML {* |
18 ML {* |