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" } })