# HG changeset patch # User haftmann # Date 1283260084 -7200 # Node ID 0e6f54c9d201aca7788e7c2b42bed7970065475b # Parent 544f4702d621658dd8699b5cbfd8f5e1e922d1cb dropped single_module parameter diff -r 544f4702d621 -r 0e6f54c9d201 src/Tools/Code/code_eval.ML --- a/src/Tools/Code/code_eval.ML Tue Aug 31 14:43:27 2010 +0200 +++ b/src/Tools/Code/code_eval.ML Tue Aug 31 15:08:04 2010 +0200 @@ -59,7 +59,7 @@ |> fold (curry Graph.add_edge value_name) deps; val (value_code, [SOME value_name']) = Code_Target.produce_code_for thy (the_default target some_target) NONE (SOME "") [] naming program ([value_name], []); - val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name' + val sml_code = "let\n" ^ value_code ^ "\nin " ^ Long_Name.base_name value_name' ^ space_implode " " (map (enclose "(" ")") args) ^ " end"; in ML_Context.evaluate ctxt false reff sml_code end; in Code_Thingol.dynamic_eval_value thy postproc evaluator t end; diff -r 544f4702d621 -r 0e6f54c9d201 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Tue Aug 31 14:43:27 2010 +0200 +++ b/src/Tools/Code/code_haskell.ML Tue Aug 31 15:08:04 2010 +0200 @@ -314,7 +314,7 @@ in (deresolver, hs_program) end; fun serialize_haskell module_prefix string_classes { labelled_name, - reserved_syms, includes, single_module, module_alias, + reserved_syms, includes, module_alias, class_syntax, tyco_syntax, const_syntax, program, names, presentation_names } = let @@ -350,7 +350,7 @@ fun serialize_module1 (module_name', (deps, (stmts, _))) = let val stmt_names = map fst stmts; - val qualified = not single_module; + val qualified = null presentation_names; val imports = subtract (op =) stmt_names deps |> distinct (op =) |> map_filter (try deresolver) diff -r 544f4702d621 -r 0e6f54c9d201 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Tue Aug 31 14:43:27 2010 +0200 +++ b/src/Tools/Code/code_ml.ML Tue Aug 31 15:08:04 2010 +0200 @@ -903,7 +903,7 @@ in (deresolver, nodes) end; fun serialize_ml target print_module print_stmt with_signatures { labelled_name, - reserved_syms, includes, single_module, module_alias, class_syntax, tyco_syntax, + reserved_syms, includes, module_alias, class_syntax, tyco_syntax, const_syntax, program, names, presentation_names } = let val is_cons = Code_Thingol.is_cons program; @@ -927,8 +927,7 @@ o rev o flat o Graph.strong_conn) nodes |> split_list |> (fn (decls, body) => (flat decls, body)) - val names' = map (try (deresolver [])) names - |> single_module ? (map o Option.map) Long_Name.base_name; + val names' = map (try (deresolver [])) names; 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; diff -r 544f4702d621 -r 0e6f54c9d201 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Tue Aug 31 14:43:27 2010 +0200 +++ b/src/Tools/Code/code_scala.ML Tue Aug 31 15:08:04 2010 +0200 @@ -413,7 +413,7 @@ in (deresolver, sca_program) end; -fun serialize_scala { labelled_name, reserved_syms, includes, single_module, +fun serialize_scala { labelled_name, reserved_syms, includes, module_alias, class_syntax, tyco_syntax, const_syntax, program, names, presentation_names } = let diff -r 544f4702d621 -r 0e6f54c9d201 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Tue Aug 31 14:43:27 2010 +0200 +++ b/src/Tools/Code/code_target.ML Tue Aug 31 15:08:04 2010 +0200 @@ -105,7 +105,6 @@ labelled_name: string -> string, reserved_syms: string list, includes: (string * Pretty.T) list, - single_module: bool, module_alias: string -> string option, class_syntax: string -> string option, tyco_syntax: string -> Code_Printer.tyco_syntax option, @@ -314,7 +313,6 @@ labelled_name = Code_Thingol.labelled_name thy proto_program, reserved_syms = reserved, includes = includes, - single_module = is_some module_name, module_alias = if is_some module_name then K module_name else Symtab.lookup module_alias, class_syntax = Symtab.lookup class_syntax, tyco_syntax = Symtab.lookup tyco_syntax,