equal
deleted
inserted
replaced
123 toks''') |
123 toks''') |
124 else ("", tok :: toks''') |
124 else ("", tok :: toks''') |
125 end) |
125 end) |
126 val txt = spc ^ implode (transform_cmts toks') |
126 val txt = spc ^ implode (transform_cmts toks') |
127 in |
127 in |
128 txt |> split_lines |> OutputFN.output |
128 OutputTutorial.output (split_lines txt) |
129 end; |
129 end; |
130 |
130 |
131 val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk; |
131 val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk; |
132 |
132 |
133 end; |
133 end; |