# HG changeset patch
# User haftmann
# Date 1283323969 -7200
# Node ID 68853347ba37cf166b3b29a704c7d902a2114fa3
# Parent  45e4d3a855adafdcdbdf3b77967f626037ba6153
tuned internally and made smlnj happy

diff -r 45e4d3a855ad -r 68853347ba37 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Wed Sep 01 07:53:31 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Wed Sep 01 08:52:49 2010 +0200
@@ -397,6 +397,12 @@
         @ map serialize_module (Symtab.dest hs_program))
   end;
 
+val serializer : Code_Target.serializer =
+  Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
+    -- Scan.optional (Args.$$$ "string_classes" >> K true) false
+    >> (fn (module_prefix, string_classes) =>
+      serialize_haskell module_prefix string_classes));
+
 val literals = let
   fun char_haskell c =
     let
@@ -465,12 +471,6 @@
 
 (** Isar setup **)
 
-val isar_serializer =
-  Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
-    -- Scan.optional (Args.$$$ "string_classes" >> K true) false
-    >> (fn (module_prefix, string_classes) =>
-      serialize_haskell module_prefix string_classes));
-
 val _ =
   Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
     Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
@@ -479,7 +479,7 @@
 
 val setup =
   Code_Target.add_target
-    (target, { serializer = isar_serializer, literals = literals,
+    (target, { serializer = serializer, literals = literals,
       check = { env_var = "EXEC_GHC", make_destination = I,
         make_command = fn ghc => fn module_name =>
           ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
diff -r 45e4d3a855ad -r 68853347ba37 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Wed Sep 01 07:53:31 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Wed Sep 01 08:52:49 2010 +0200
@@ -935,26 +935,26 @@
 
 end; (*local*)
 
-
-(** Isar setup **)
-
-val isar_serializer_sml =
+val serializer_sml : Code_Target.serializer =
   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   >> (fn with_signatures => serialize_ml target_SML
       print_sml_module print_sml_stmt with_signatures));
 
-val isar_serializer_ocaml =
+val serializer_ocaml : Code_Target.serializer =
   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
   >> (fn with_signatures => serialize_ml target_OCaml
       print_ocaml_module print_ocaml_stmt with_signatures));
 
+
+(** Isar setup **)
+
 val setup =
   Code_Target.add_target
-    (target_SML, { serializer = isar_serializer_sml, literals = literals_sml,
+    (target_SML, { serializer = serializer_sml, literals = literals_sml,
       check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
         make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
   #> Code_Target.add_target
-    (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
+    (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
       check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
         make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
   #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
diff -r 45e4d3a855ad -r 68853347ba37 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Wed Sep 01 07:53:31 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Wed Sep 01 08:52:49 2010 +0200
@@ -488,6 +488,9 @@
 
 end; (*local*)
 
+val serializer : Code_Target.serializer =
+  Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
+
 val literals = let
   fun char_scala c = if c = "'" then "\\'"
     else if c = "\"" then "\\\""
@@ -513,12 +516,9 @@
 
 (** Isar setup **)
 
-val isar_serializer =
-  Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
-
 val setup =
   Code_Target.add_target
-    (target, { serializer = isar_serializer, literals = literals,
+    (target, { serializer = serializer, literals = literals,
       check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
         make_command = fn scala_home => fn _ =>
           "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "