equal
deleted
inserted
replaced
38 #> Chunks.transform_cmts |
38 #> Chunks.transform_cmts |
39 #> implode |
39 #> implode |
40 #> string_explode ""; |
40 #> string_explode ""; |
41 |
41 |
42 (* output function *) |
42 (* output function *) |
43 fun output_fn txt = Chunks.output (map Pretty.str txt) |
43 fun output_fn txt = OutputFN.output txt |
44 |
44 |
45 (* checks and prints open expressions *) |
45 (* checks and prints open expressions *) |
46 fun output_ml {context = ctxt, ...} (txt, ovars) = |
46 fun output_ml {context = ctxt, ...} (txt, ovars) = |
47 (eval_fn ctxt (ml_val_open ovars txt); |
47 (eval_fn ctxt (ml_val_open ovars txt); |
48 output_fn (transform_cmts_str txt)) |
48 output_fn (transform_cmts_str txt)) |