src/Tools/Code/code_ml.ML
changeset 52138 e21426f244aa
parent 51143 0a2371e7ced3
child 52435 6646bb548c6b
     1.1 --- a/src/Tools/Code/code_ml.ML	Fri May 24 23:57:24 2013 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Fri May 24 23:57:24 2013 +0200
     1.3 @@ -698,7 +698,7 @@
     1.4  
     1.5  (** SML/OCaml generic part **)
     1.6  
     1.7 -fun ml_program_of_program labelled_name reserved module_alias program =
     1.8 +fun ml_program_of_program ctxt symbol_of module_name reserved identifiers program =
     1.9    let
    1.10      fun namify_const upper base (nsp_const, nsp_type) =
    1.11        let
    1.12 @@ -729,7 +729,8 @@
    1.13        | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as { vs, ... })) =
    1.14            (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
    1.15        | ml_binding_of_stmt (name, _) =
    1.16 -          error ("Binding block containing illegal statement: " ^ labelled_name name)
    1.17 +          error ("Binding block containing illegal statement: " ^ 
    1.18 +            (Code_Symbol.quote_symbol ctxt o symbol_of) name)
    1.19      fun modify_fun (name, stmt) =
    1.20        let
    1.21          val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
    1.22 @@ -769,21 +770,22 @@
    1.23        | modify_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
    1.24            modify_funs stmts
    1.25        | modify_stmts stmts = error ("Illegal mutual dependencies: " ^
    1.26 -          (Library.commas o map (labelled_name o fst)) stmts);
    1.27 +          (Library.commas o map (Code_Symbol.quote_symbol ctxt o symbol_of o fst)) stmts);
    1.28    in
    1.29 -    Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
    1.30 +    Code_Namespace.hierarchical_program ctxt symbol_of {
    1.31 +      module_name = module_name, reserved = reserved, identifiers = identifiers,
    1.32        empty_nsp = (reserved, reserved), namify_module = pair, namify_stmt = namify_stmt,
    1.33        cyclic_modules = false, empty_data = (), memorize_data = K I, modify_stmts = modify_stmts } program
    1.34    end;
    1.35  
    1.36 -fun serialize_ml print_ml_module print_ml_stmt with_signatures
    1.37 -    { labelled_name, reserved_syms, includes, module_alias,
    1.38 +fun serialize_ml print_ml_module print_ml_stmt with_signatures ctxt
    1.39 +    { symbol_of, module_name, reserved_syms, identifiers, includes,
    1.40        class_syntax, tyco_syntax, const_syntax } program =
    1.41    let
    1.42  
    1.43      (* build program *)
    1.44      val { deresolver, hierarchical_program = ml_program } =
    1.45 -      ml_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
    1.46 +      ml_program_of_program ctxt symbol_of module_name (Name.make_context reserved_syms) identifiers program;
    1.47  
    1.48      (* print statements *)
    1.49      fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt