20 in "val " ^ pat' ^ " = " ^ rhs end; |
20 in "val " ^ pat' ^ " = " ^ rhs end; |
21 |
21 |
22 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; |
22 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; |
23 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; |
23 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; |
24 |
24 |
|
25 val transform_cmts_str = |
|
26 Source.of_string #> ML_Lex.source #> Source.exhaust #> |
|
27 Chunks.transform_cmts #> implode; |
|
28 |
25 fun output_ml ml src ctxt ((txt,ovars),pos) = |
29 fun output_ml ml src ctxt ((txt,ovars),pos) = |
26 (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt); |
30 (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt); |
27 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt)) |
31 txt |> transform_cmts_str |> space_explode "\n" |> |
|
32 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt) |
28 |
33 |
29 fun output_ml_aux ml src ctxt (txt,pos) = |
34 fun output_ml_aux ml src ctxt (txt,pos) = |
30 output_ml (K ml) src ctxt ((txt,()),pos) |
35 output_ml (K ml) src ctxt ((txt,()),pos) |
31 |
36 |
32 fun add_response_indicator txt = |
37 fun add_response_indicator txt = |