1.1 --- a/src/Tools/Code/code_haskell.ML	Wed Sep 01 07:53:31 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Wed Sep 01 08:52:49 2010 +0200
     1.3 @@ -397,6 +397,12 @@
     1.4          @ map serialize_module (Symtab.dest hs_program))
     1.5    end;
     1.6  
     1.7 +val serializer : Code_Target.serializer =
     1.8 +  Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
     1.9 +    -- Scan.optional (Args.$$$ "string_classes" >> K true) false
    1.10 +    >> (fn (module_prefix, string_classes) =>
    1.11 +      serialize_haskell module_prefix string_classes));
    1.12 +
    1.13  val literals = let
    1.14    fun char_haskell c =
    1.15      let
    1.16 @@ -465,12 +471,6 @@
    1.17  
    1.18  (** Isar setup **)
    1.19  
    1.20 -val isar_serializer =
    1.21 -  Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
    1.22 -    -- Scan.optional (Args.$$$ "string_classes" >> K true) false
    1.23 -    >> (fn (module_prefix, string_classes) =>
    1.24 -      serialize_haskell module_prefix string_classes));
    1.25 -
    1.26  val _ =
    1.27    Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
    1.28      Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
    1.29 @@ -479,7 +479,7 @@
    1.30  
    1.31  val setup =
    1.32    Code_Target.add_target
    1.33 -    (target, { serializer = isar_serializer, literals = literals,
    1.34 +    (target, { serializer = serializer, literals = literals,
    1.35        check = { env_var = "EXEC_GHC", make_destination = I,
    1.36          make_command = fn ghc => fn module_name =>
    1.37            ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })

     2.1 --- a/src/Tools/Code/code_ml.ML	Wed Sep 01 07:53:31 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Wed Sep 01 08:52:49 2010 +0200
     2.3 @@ -935,26 +935,26 @@
     2.4  
     2.5  end; (*local*)
     2.6  
     2.7 -
     2.8 -(** Isar setup **)
     2.9 -
    2.10 -val isar_serializer_sml =
    2.11 +val serializer_sml : Code_Target.serializer =
    2.12    Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    2.13    >> (fn with_signatures => serialize_ml target_SML
    2.14        print_sml_module print_sml_stmt with_signatures));
    2.15  
    2.16 -val isar_serializer_ocaml =
    2.17 +val serializer_ocaml : Code_Target.serializer =
    2.18    Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    2.19    >> (fn with_signatures => serialize_ml target_OCaml
    2.20        print_ocaml_module print_ocaml_stmt with_signatures));
    2.21  
    2.22 +
    2.23 +(** Isar setup **)
    2.24 +
    2.25  val setup =
    2.26    Code_Target.add_target
    2.27 -    (target_SML, { serializer = isar_serializer_sml, literals = literals_sml,
    2.28 +    (target_SML, { serializer = serializer_sml, literals = literals_sml,
    2.29        check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
    2.30          make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
    2.31    #> Code_Target.add_target
    2.32 -    (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
    2.33 +    (target_OCaml, { serializer = serializer_ocaml, literals = literals_ocaml,
    2.34        check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
    2.35          make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
    2.36    #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>

     3.1 --- a/src/Tools/Code/code_scala.ML	Wed Sep 01 07:53:31 2010 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Wed Sep 01 08:52:49 2010 +0200
     3.3 @@ -488,6 +488,9 @@
     3.4  
     3.5  end; (*local*)
     3.6  
     3.7 +val serializer : Code_Target.serializer =
     3.8 +  Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
     3.9 +
    3.10  val literals = let
    3.11    fun char_scala c = if c = "'" then "\\'"
    3.12      else if c = "\"" then "\\\""
    3.13 @@ -513,12 +516,9 @@
    3.14  
    3.15  (** Isar setup **)
    3.16  
    3.17 -val isar_serializer =
    3.18 -  Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
    3.19 -
    3.20  val setup =
    3.21    Code_Target.add_target
    3.22 -    (target, { serializer = isar_serializer, literals = literals,
    3.23 +    (target, { serializer = serializer, literals = literals,
    3.24        check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
    3.25          make_command = fn scala_home => fn _ =>
    3.26            "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "