# HG changeset patch # User haftmann # Date 1283255754 -7200 # Node ID fcd1d0457e27e9651b28e4a490c663d9c1e677b8 # Parent 79d7f2b4cf713ca8321845f65987f3101d293488 removed serializer interface redundancies diff -r 79d7f2b4cf71 -r fcd1d0457e27 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Tue Aug 31 13:29:38 2010 +0200 +++ b/src/Tools/Code/code_haskell.ML Tue Aug 31 13:55:54 2010 +0200 @@ -313,8 +313,8 @@ handle Option => error ("Unknown statement name: " ^ labelled_name name); in (deresolver, hs_program) end; -fun serialize_haskell module_prefix module_name string_classes labelled_name - raw_reserved includes module_alias +fun serialize_haskell module_prefix string_classes labelled_name + raw_reserved includes single_module module_alias class_syntax tyco_syntax const_syntax program (stmt_names, presentation_stmt_names) = let @@ -350,7 +350,7 @@ fun serialize_module1 (module_name', (deps, (stmts, _))) = let val stmt_names = map fst stmts; - val qualified = is_none module_name; + val qualified = not single_module; val imports = subtract (op =) stmt_names deps |> distinct (op =) |> map_filter (try deresolver) @@ -465,11 +465,11 @@ (** Isar setup **) -fun isar_serializer module_name = +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 module_name string_classes)); + serialize_haskell module_prefix string_classes)); val _ = Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl ( diff -r 79d7f2b4cf71 -r fcd1d0457e27 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Tue Aug 31 13:29:38 2010 +0200 +++ b/src/Tools/Code/code_ml.ML Tue Aug 31 13:55:54 2010 +0200 @@ -718,7 +718,7 @@ in -fun ml_node_of_program labelled_name module_name reserved module_alias program = +fun ml_node_of_program labelled_name reserved module_alias program = let val reserved = Name.make_context reserved; val empty_module = ((reserved, reserved), Graph.empty); @@ -902,13 +902,13 @@ error ("Unknown statement name: " ^ labelled_name name); in (deresolver, nodes) end; -fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name - reserved includes module_alias _ tyco_syntax const_syntax program +fun serialize_ml target print_module print_stmt with_signatures labelled_name + reserved includes single_module module_alias _ tyco_syntax const_syntax program (stmt_names, presentation_stmt_names) = let val is_cons = Code_Thingol.is_cons program; val is_presentation = not (null presentation_stmt_names); - val (deresolver, nodes) = ml_node_of_program labelled_name module_name + val (deresolver, nodes) = ml_node_of_program labelled_name reserved module_alias program; val reserved = make_vars reserved; fun print_node prefix (Dummy _) = @@ -927,8 +927,8 @@ o rev o flat o Graph.strong_conn) nodes |> split_list |> (fn (decls, body) => (flat decls, body)) - val stmt_names' = (map o try) - (deresolver (if is_some module_name then the_list module_name else [])) stmt_names; + val stmt_names' = map (try (deresolver [])) stmt_names + |> single_module ? (map o Option.map) Long_Name.base_name; val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes)); fun write width NONE = writeln_pretty width | write width (SOME p) = File.write p o string_of_pretty width; @@ -941,15 +941,15 @@ (** Isar setup **) -fun isar_serializer_sml module_name = +val isar_serializer_sml = 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 module_name with_signatures)); + print_sml_module print_sml_stmt with_signatures)); -fun isar_serializer_ocaml module_name = +val isar_serializer_ocaml = 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 module_name with_signatures)); + print_ocaml_module print_ocaml_stmt with_signatures)); val setup = Code_Target.add_target diff -r 79d7f2b4cf71 -r fcd1d0457e27 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Tue Aug 31 13:29:38 2010 +0200 +++ b/src/Tools/Code/code_scala.ML Tue Aug 31 13:55:54 2010 +0200 @@ -413,7 +413,7 @@ in (deresolver, sca_program) end; -fun serialize_scala labelled_name raw_reserved includes module_alias +fun serialize_scala labelled_name raw_reserved includes _ module_alias _ tyco_syntax const_syntax program (stmt_names, presentation_stmt_names) = let @@ -513,9 +513,8 @@ (** Isar setup **) -fun isar_serializer _ = - Code_Target.parse_args (Scan.succeed ()) - #> (fn () => serialize_scala); +val isar_serializer = + Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala; val setup = Code_Target.add_target diff -r 79d7f2b4cf71 -r fcd1d0457e27 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Tue Aug 31 13:29:38 2010 +0200 +++ b/src/Tools/Code/code_target.ML Tue Aug 31 13:55:54 2010 +0200 @@ -101,12 +101,11 @@ Symtab.join (K snd) (const1, const2)) ); -type serializer = - string option (*module name*) - -> Token.T list (*arguments*) +type serializer = Token.T list (*arguments*) -> (string -> string) (*labelled_name*) -> string list (*reserved symbols*) -> (string * Pretty.T) list (*includes*) + -> bool (*singleton module*) -> (string -> string option) (*module aliasses*) -> (string -> string option) (*class syntax*) -> (string -> Code_Printer.tyco_syntax option) @@ -279,8 +278,8 @@ val _ = if null empty_funs then () else error ("No code equations for " ^ commas (map (Sign.extern_const thy) empty_funs)); in - serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes - (if is_some module_name then K module_name else Symtab.lookup module_alias) + serializer args (Code_Thingol.labelled_name thy program2) reserved includes + (is_some module_name) (if is_some module_name then K module_name else Symtab.lookup module_alias) (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const') program4 (names1, presentation_names) width end;