--- 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;
--- 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)
--- 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;
--- 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
--- 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,