tuned
authorhaftmann
Thu Jan 26 16:25:32 2017 +0100 (2017-01-26)
changeset 6495885b87da722ab
parent 64957 3faa9b31ff78
child 64959 9ca021bd718d
tuned
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu Jan 26 16:06:19 2017 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Jan 26 16:25:32 2017 +0100
     1.3 @@ -419,14 +419,14 @@
     1.4      first_occurrence: bool,
     1.5      generated_code: {
     1.6        code: string,
     1.7 -      consts_map: (string * string) list
     1.8 +      name_for_const: string -> string
     1.9      } lazy
    1.10    };
    1.11    val empty: T = { named_consts = [],
    1.12      first_occurrence = true,
    1.13      generated_code = Lazy.value {
    1.14        code = "",
    1.15 -      consts_map = []
    1.16 +      name_for_const = I
    1.17      }
    1.18    };
    1.19    fun init _ = empty;
    1.20 @@ -439,7 +439,7 @@
    1.21      val program = Code_Thingol.consts_program ctxt consts;
    1.22      val (code, (_, consts_map)) =
    1.23        runtime_code ctxt Code_Target.generatedN program [] consts
    1.24 -  in { code = code, consts_map = consts_map } end);
    1.25 +  in { code = code, name_for_const = the o AList.lookup (op =) consts_map } end);
    1.26  
    1.27  fun register_const const ctxt =
    1.28    let
    1.29 @@ -455,10 +455,10 @@
    1.30  
    1.31  fun print_code is_first_occ const ctxt =
    1.32    let
    1.33 -    val { code, consts_map } = (Lazy.force o #generated_code o Code_Antiq_Data.get) ctxt;
    1.34 -    val effective_code = if is_first_occ then code else "";
    1.35 -    val body = ML_Context.struct_name ctxt ^ "." ^ the (AList.lookup (op =) consts_map const);
    1.36 -  in (effective_code, body) end;
    1.37 +    val { code, name_for_const } = (Lazy.force o #generated_code o Code_Antiq_Data.get) ctxt;
    1.38 +    val context_code = if is_first_occ then code else "";
    1.39 +    val body_code = ML_Context.struct_name ctxt ^ "." ^ name_for_const const;
    1.40 +  in (context_code, body_code) end;
    1.41  
    1.42  in
    1.43