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