equal
deleted
inserted
replaced
1091 in output (map_filter deresolv cs, p) end; |
1091 in output (map_filter deresolv cs, p) end; |
1092 |
1092 |
1093 fun isar_seri_sml module file = |
1093 fun isar_seri_sml module file = |
1094 let |
1094 let |
1095 val output = case file |
1095 val output = case file |
1096 of NONE => use_text "generated code" Output.ml_output false o code_output |
1096 of NONE => use_text (1, "generated code") Output.ml_output false o code_output |
1097 | SOME "-" => PrintMode.setmp [] writeln o code_output |
1097 | SOME "-" => PrintMode.setmp [] writeln o code_output |
1098 | SOME file => File.write (Path.explode file) o code_output; |
1098 | SOME file => File.write (Path.explode file) o code_output; |
1099 in |
1099 in |
1100 parse_args (Scan.succeed ()) |
1100 parse_args (Scan.succeed ()) |
1101 #> (fn () => seri_ml pr_sml pr_sml_modl module (output o snd)) |
1101 #> (fn () => seri_ml pr_sml pr_sml_modl module (output o snd)) |