--- a/src/Tools/Code/code_runtime.ML Thu Jan 26 16:06:19 2017 +0100
+++ b/src/Tools/Code/code_runtime.ML Thu Jan 26 16:25:32 2017 +0100
@@ -419,14 +419,14 @@
first_occurrence: bool,
generated_code: {
code: string,
- consts_map: (string * string) list
+ name_for_const: string -> string
} lazy
};
val empty: T = { named_consts = [],
first_occurrence = true,
generated_code = Lazy.value {
code = "",
- consts_map = []
+ name_for_const = I
}
};
fun init _ = empty;
@@ -439,7 +439,7 @@
val program = Code_Thingol.consts_program ctxt consts;
val (code, (_, consts_map)) =
runtime_code ctxt Code_Target.generatedN program [] consts
- in { code = code, consts_map = consts_map } end);
+ in { code = code, name_for_const = the o AList.lookup (op =) consts_map } end);
fun register_const const ctxt =
let
@@ -455,10 +455,10 @@
fun print_code is_first_occ const ctxt =
let
- val { code, consts_map } = (Lazy.force o #generated_code o Code_Antiq_Data.get) ctxt;
- val effective_code = if is_first_occ then code else "";
- val body = ML_Context.struct_name ctxt ^ "." ^ the (AList.lookup (op =) consts_map const);
- in (effective_code, body) end;
+ val { code, name_for_const } = (Lazy.force o #generated_code o Code_Antiq_Data.get) ctxt;
+ val context_code = if is_first_occ then code else "";
+ val body_code = ML_Context.struct_name ctxt ^ "." ^ name_for_const const;
+ in (context_code, body_code) end;
in