src/Tools/Code/code_haskell.ML
changeset 38966 68853347ba37
parent 38928 0e6f54c9d201
child 39034 ebeb48fd653b
     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" } })