equal
deleted
inserted
replaced
31 fun ml_type txt = |
31 fun ml_type txt = |
32 implode ["val _ = NONE : (", txt, ") option"]; |
32 implode ["val _ = NONE : (", txt, ") option"]; |
33 |
33 |
34 (* eval function *) |
34 (* eval function *) |
35 fun eval_fn ctxt exp = |
35 fun eval_fn ctxt exp = |
36 ML_Context.eval_source_in (SOME ctxt) false |
36 ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags |
37 {delimited = false, text = exp, pos = Position.none} |
37 {delimited = false, text = exp, pos = Position.none} |
38 |
38 |
39 (* checks and prints a possibly open expressions, no index *) |
39 (* checks and prints a possibly open expressions, no index *) |
40 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) = |
40 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) = |
41 (eval_fn ctxt (ml_val vs stru txt); |
41 (eval_fn ctxt (ml_val vs stru txt); |