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_text_in (SOME ctxt) false Position.none exp |
36 ML_Context.eval_source_in (SOME ctxt) false |
|
37 {delimited = false, text = exp, pos = Position.none} |
37 |
38 |
38 (* checks and prints a possibly open expressions, no index *) |
39 (* checks and prints a possibly open expressions, no index *) |
39 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) = |
40 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) = |
40 (eval_fn ctxt (ml_val vs stru txt); |
41 (eval_fn ctxt (ml_val vs stru txt); |
41 output ctxt (split_lines txt)) |
42 output ctxt (split_lines txt)) |