# HG changeset patch
# User haftmann
# Date 1278600117 -7200
# Node ID 0af0d45257be947baaba74853542272b1e4fc14e
# Parent  3a699743bcbae129e8d35a35e9dc3a9fcbc62582
dropped ancient in-place compilation of SML

diff -r 3a699743bcba -r 0af0d45257be src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Thu Jul 08 16:28:18 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Jul 08 16:41:57 2010 +0200
@@ -390,7 +390,7 @@
           ^ code_of_pretty content)
       end
   in
-    Code_Target.mk_serialization target NONE
+    Code_Target.mk_serialization target
       (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
         (write_module (check_destination file)))
       (rpair [] o cat_lines o map (code_of_pretty o snd))
diff -r 3a699743bcba -r 0af0d45257be src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Jul 08 16:28:18 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Jul 08 16:41:57 2010 +0200
@@ -907,7 +907,7 @@
         error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, nodes) end;
 
-fun serialize_ml target compile print_module print_stmt raw_module_name with_signatures labelled_name
+fun serialize_ml target print_module print_stmt raw_module_name with_signatures labelled_name
   reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
   let
     val is_cons = Code_Thingol.is_cons program;
@@ -938,7 +938,6 @@
     val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
   in
     Code_Target.mk_serialization target
-      (case compile of SOME compile => SOME (compile o code_of_pretty) | NONE => NONE)
       (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
       (rpair stmt_names' o code_of_pretty) p destination
   end;
@@ -950,7 +949,7 @@
 
 fun evaluation_code_of thy target struct_name =
   Code_Target.serialize_custom thy (target, (fn _ => fn [] =>
-    serialize_ml target (SOME (K ())) print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
+    serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
 
 
 (** formal checking of compiled code **)
@@ -969,12 +968,11 @@
 fun isar_seri_sml module_name =
   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   >> (fn with_signatures => serialize_ml target_SML
-      (SOME (use_text ML_Env.local_context (1, "generated code") false))
       print_sml_module print_sml_stmt module_name with_signatures));
 
 fun isar_seri_ocaml module_name =
   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
-  >> (fn with_signatures => serialize_ml target_OCaml NONE
+  >> (fn with_signatures => serialize_ml target_OCaml
       print_ocaml_module print_ocaml_stmt module_name with_signatures));
 
 val setup =
diff -r 3a699743bcba -r 0af0d45257be src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Jul 08 16:28:18 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Jul 08 16:41:57 2010 +0200
@@ -382,7 +382,7 @@
         val _ = File.mkdir_leaf (Path.dir pathname);
       in File.write pathname (code_of_pretty content) end
   in
-    Code_Target.mk_serialization target NONE
+    Code_Target.mk_serialization target
       (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
         (write_module (check_destination file)))
       (rpair [] o cat_lines o map (code_of_pretty o snd))
diff -r 3a699743bcba -r 0af0d45257be src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Jul 08 16:28:18 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Jul 08 16:41:57 2010 +0200
@@ -21,8 +21,7 @@
   type serialization
   val parse_args: 'a parser -> Token.T list -> 'a
   val stmt_names_of_destination: destination -> string list
-  val mk_serialization: string -> ('a -> unit) option
-    -> (Path.T option -> 'a -> unit)
+  val mk_serialization: string -> (Path.T option -> 'a -> unit)
     -> ('a -> string * string option list)
     -> 'a -> serialization
   val serialize: theory -> string -> int option -> string option -> Token.T list
@@ -30,7 +29,6 @@
   val serialize_custom: theory -> string * (serializer * literals)
     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
   val the_literals: theory -> string -> literals
-  val compile: serialization -> unit
   val export: serialization -> unit
   val file: Path.T -> serialization -> unit
   val string: string list -> serialization -> string
@@ -64,10 +62,9 @@
 
 (** basics **)
 
-datatype destination = Compile | Export | File of Path.T | String of string list;
+datatype destination = Export | File of Path.T | String of string list;
 type serialization = destination -> (string * string option list) option;
 
-fun compile f = (f Compile; ());
 fun export f = (f Export; ());
 fun file p f = (f (File p); ());
 fun string stmts f = fst (the (f (String stmts)));
@@ -75,11 +72,9 @@
 fun stmt_names_of_destination (String stmts) = stmts
   | stmt_names_of_destination _ = [];
 
-fun mk_serialization target (SOME comp) _ _ code Compile = (comp code; NONE)
-  | mk_serialization target NONE _ _ _ Compile = error (target ^ ": no internal compilation")
-  | mk_serialization target _ output _ code Export = (output NONE code ; NONE)
-  | mk_serialization target _ output _ code (File file) = (output (SOME file) code; NONE)
-  | mk_serialization target _ _ string code (String _) = SOME (string code);
+fun mk_serialization target output _ code Export = (output NONE code ; NONE)
+  | mk_serialization target output _ code (File file) = (output (SOME file) code; NONE)
+  | mk_serialization target _ string code (String _) = SOME (string code);
 
 
 (** theory data **)
@@ -382,9 +377,8 @@
   let
     val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
     fun mk_seri_dest dest = case dest
-     of NONE => compile
-      | SOME "-" => export
-      | SOME f => file (Path.explode f)
+     of "-" => export
+      | f => file (Path.explode f)
     val _ = map (fn (((target, module), dest), args) =>
       (mk_seri_dest dest (serialize thy target NONE module args naming program cs'))) seris;
   in () end;
@@ -530,7 +524,7 @@
   (Scan.repeat1 Parse.term_group
   -- Scan.repeat (Parse.$$$ inK |-- Parse.name
      -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
-     -- Scan.option (Parse.$$$ fileK |-- Parse.name)
+     --| Parse.$$$ fileK -- Parse.name
      -- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []
   ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));