887 str "i"])) args) |
887 str "i"])) args) |
888 (Pretty.block [str "if ", |
888 (Pretty.block [str "if ", |
889 mk_app false (str "testf") (map (str o fst) args), |
889 mk_app false (str "testf") (map (str o fst) args), |
890 Pretty.brk 1, str "then NONE", |
890 Pretty.brk 1, str "then NONE", |
891 Pretty.brk 1, str "else ", |
891 Pretty.brk 1, str "else ", |
892 Pretty.block [str "SOME ", Pretty.block (str "[" :: |
892 Pretty.block [str "SOME ", |
893 Pretty.commas (map (fn (s, _) => str (s ^ "_t ()")) args) @ |
893 Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]), |
894 [str "]"])]]), |
|
895 str ");"]) ^ |
894 str ");"]) ^ |
896 "\n\nend;\n"; |
895 "\n\nend;\n"; |
897 val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s; |
896 val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s; |
898 val dummy_report = ([], false) |
897 val dummy_report = ([], false) |
899 in (fn size => (! test_fn size, dummy_report)) end; |
898 in (fn size => (! test_fn size, dummy_report)) end; |