--- 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 (
--- 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
--- 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
--- 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;