1.1 --- a/src/Tools/code/code_package.ML Wed May 28 11:05:47 2008 +0200
1.2 +++ b/src/Tools/code/code_package.ML Wed May 28 12:06:49 2008 +0200
1.3 @@ -97,9 +97,13 @@
1.4 fun code thy permissive cs seris =
1.5 let
1.6 val code = Program.get thy;
1.7 - val seris' = map (fn (((target, module), file), args) =>
1.8 - CodeTarget.get_serializer thy target permissive module file args cs) seris;
1.9 - in (map (fn f => f code) seris' : unit list; ()) end;
1.10 + fun mk_seri_dest file = case file
1.11 + of NONE => CodeTarget.compile
1.12 + | SOME "-" => writeln o CodeTarget.string
1.13 + | SOME f => CodeTarget.file (Path.explode f)
1.14 + val _ = map (fn (((target, module), file), args) =>
1.15 + (mk_seri_dest file (CodeTarget.serialize thy target permissive module args code cs))) seris;
1.16 + in () end;
1.17
1.18 (* evaluation machinery *)
1.19
1.20 @@ -145,7 +149,7 @@
1.21 val cs = map (CodeUnit.check_const thy) ts;
1.22 val (cs', code') = generate thy (CodeFuncgr.make thy cs)
1.23 (fold_map ooo ensure_const) cs;
1.24 - val code'' = CodeTarget.sml_of thy cs' code' ^ " ()";
1.25 + val code'' = CodeTarget.sml_of thy code' cs' ^ " ()";
1.26 in (("codevals", code''), (ctxt', args')) end;
1.27
1.28