equal
deleted
inserted
replaced
3 struct |
3 struct |
4 |
4 |
5 (* rebuilding the output function from ThyOutput in order to *) |
5 (* rebuilding the output function from ThyOutput in order to *) |
6 (* enable the options [gray, linenos] *) |
6 (* enable the options [gray, linenos] *) |
7 |
7 |
8 val gray = ref false |
8 val gray = Unsynchronized.ref false |
9 val linenos = ref false |
9 val linenos = Unsynchronized.ref false |
10 |
10 |
11 |
11 |
12 fun output txt = |
12 fun output txt = |
13 let |
13 let |
14 val prts = map Pretty.str txt |
14 val prts = map Pretty.str txt |