1.1 --- a/src/Tools/Code/code_haskell.ML	Thu Jul 08 16:28:18 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Jul 08 16:41:57 2010 +0200
     1.3 @@ -390,7 +390,7 @@
     1.4            ^ code_of_pretty content)
     1.5        end
     1.6    in
     1.7 -    Code_Target.mk_serialization target NONE
     1.8 +    Code_Target.mk_serialization target
     1.9        (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
    1.10          (write_module (check_destination file)))
    1.11        (rpair [] o cat_lines o map (code_of_pretty o snd))

     2.1 --- a/src/Tools/Code/code_ml.ML	Thu Jul 08 16:28:18 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Thu Jul 08 16:41:57 2010 +0200
     2.3 @@ -907,7 +907,7 @@
     2.4          error ("Unknown statement name: " ^ labelled_name name);
     2.5    in (deresolver, nodes) end;
     2.6  
     2.7 -fun serialize_ml target compile print_module print_stmt raw_module_name with_signatures labelled_name
     2.8 +fun serialize_ml target print_module print_stmt raw_module_name with_signatures labelled_name
     2.9    reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
    2.10    let
    2.11      val is_cons = Code_Thingol.is_cons program;
    2.12 @@ -938,7 +938,6 @@
    2.13      val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
    2.14    in
    2.15      Code_Target.mk_serialization target
    2.16 -      (case compile of SOME compile => SOME (compile o code_of_pretty) | NONE => NONE)
    2.17        (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
    2.18        (rpair stmt_names' o code_of_pretty) p destination
    2.19    end;
    2.20 @@ -950,7 +949,7 @@
    2.21  
    2.22  fun evaluation_code_of thy target struct_name =
    2.23    Code_Target.serialize_custom thy (target, (fn _ => fn [] =>
    2.24 -    serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
    2.25 +    serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
    2.26  
    2.27  
    2.28  (** formal checking of compiled code **)
    2.29 @@ -969,12 +968,11 @@
    2.30  fun isar_seri_sml module_name =
    2.31    Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    2.32    >> (fn with_signatures => serialize_ml target_SML
    2.33 -      (SOME (use_text ML_Env.local_context (1, "generated code") false))
    2.34        print_sml_module print_sml_stmt module_name with_signatures));
    2.35  
    2.36  fun isar_seri_ocaml module_name =
    2.37    Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    2.38 -  >> (fn with_signatures => serialize_ml target_OCaml NONE
    2.39 +  >> (fn with_signatures => serialize_ml target_OCaml
    2.40        print_ocaml_module print_ocaml_stmt module_name with_signatures));
    2.41  
    2.42  val setup =

     3.1 --- a/src/Tools/Code/code_scala.ML	Thu Jul 08 16:28:18 2010 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Thu Jul 08 16:41:57 2010 +0200
     3.3 @@ -382,7 +382,7 @@
     3.4          val _ = File.mkdir_leaf (Path.dir pathname);
     3.5        in File.write pathname (code_of_pretty content) end
     3.6    in
     3.7 -    Code_Target.mk_serialization target NONE
     3.8 +    Code_Target.mk_serialization target
     3.9        (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
    3.10          (write_module (check_destination file)))
    3.11        (rpair [] o cat_lines o map (code_of_pretty o snd))

     4.1 --- a/src/Tools/Code/code_target.ML	Thu Jul 08 16:28:18 2010 +0200
     4.2 +++ b/src/Tools/Code/code_target.ML	Thu Jul 08 16:41:57 2010 +0200
     4.3 @@ -21,8 +21,7 @@
     4.4    type serialization
     4.5    val parse_args: 'a parser -> Token.T list -> 'a
     4.6    val stmt_names_of_destination: destination -> string list
     4.7 -  val mk_serialization: string -> ('a -> unit) option
     4.8 -    -> (Path.T option -> 'a -> unit)
     4.9 +  val mk_serialization: string -> (Path.T option -> 'a -> unit)
    4.10      -> ('a -> string * string option list)
    4.11      -> 'a -> serialization
    4.12    val serialize: theory -> string -> int option -> string option -> Token.T list
    4.13 @@ -30,7 +29,6 @@
    4.14    val serialize_custom: theory -> string * (serializer * literals)
    4.15      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    4.16    val the_literals: theory -> string -> literals
    4.17 -  val compile: serialization -> unit
    4.18    val export: serialization -> unit
    4.19    val file: Path.T -> serialization -> unit
    4.20    val string: string list -> serialization -> string
    4.21 @@ -64,10 +62,9 @@
    4.22  
    4.23  (** basics **)
    4.24  
    4.25 -datatype destination = Compile | Export | File of Path.T | String of string list;
    4.26 +datatype destination = Export | File of Path.T | String of string list;
    4.27  type serialization = destination -> (string * string option list) option;
    4.28  
    4.29 -fun compile f = (f Compile; ());
    4.30  fun export f = (f Export; ());
    4.31  fun file p f = (f (File p); ());
    4.32  fun string stmts f = fst (the (f (String stmts)));
    4.33 @@ -75,11 +72,9 @@
    4.34  fun stmt_names_of_destination (String stmts) = stmts
    4.35    | stmt_names_of_destination _ = [];
    4.36  
    4.37 -fun mk_serialization target (SOME comp) _ _ code Compile = (comp code; NONE)
    4.38 -  | mk_serialization target NONE _ _ _ Compile = error (target ^ ": no internal compilation")
    4.39 -  | mk_serialization target _ output _ code Export = (output NONE code ; NONE)
    4.40 -  | mk_serialization target _ output _ code (File file) = (output (SOME file) code; NONE)
    4.41 -  | mk_serialization target _ _ string code (String _) = SOME (string code);
    4.42 +fun mk_serialization target output _ code Export = (output NONE code ; NONE)
    4.43 +  | mk_serialization target output _ code (File file) = (output (SOME file) code; NONE)
    4.44 +  | mk_serialization target _ string code (String _) = SOME (string code);
    4.45  
    4.46  
    4.47  (** theory data **)
    4.48 @@ -382,9 +377,8 @@
    4.49    let
    4.50      val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
    4.51      fun mk_seri_dest dest = case dest
    4.52 -     of NONE => compile
    4.53 -      | SOME "-" => export
    4.54 -      | SOME f => file (Path.explode f)
    4.55 +     of "-" => export
    4.56 +      | f => file (Path.explode f)
    4.57      val _ = map (fn (((target, module), dest), args) =>
    4.58        (mk_seri_dest dest (serialize thy target NONE module args naming program cs'))) seris;
    4.59    in () end;
    4.60 @@ -530,7 +524,7 @@
    4.61    (Scan.repeat1 Parse.term_group
    4.62    -- Scan.repeat (Parse.$$$ inK |-- Parse.name
    4.63       -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
    4.64 -     -- Scan.option (Parse.$$$ fileK |-- Parse.name)
    4.65 +     --| Parse.$$$ fileK -- Parse.name
    4.66       -- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []
    4.67    ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
    4.68