equal
deleted
inserted
replaced
351 identifiers = identifiers, |
351 identifiers = identifiers, |
352 includes = includes, |
352 includes = includes, |
353 const_syntax = Code_Symbol.lookup_constant_data printings, |
353 const_syntax = Code_Symbol.lookup_constant_data printings, |
354 tyco_syntax = Code_Symbol.lookup_type_constructor_data printings, |
354 tyco_syntax = Code_Symbol.lookup_type_constructor_data printings, |
355 class_syntax = Code_Symbol.lookup_type_class_data printings }, |
355 class_syntax = Code_Symbol.lookup_type_class_data printings }, |
356 (syms_all, program)) |
356 (subtract (op =) syms_hidden syms, program)) |
357 end; |
357 end; |
358 |
358 |
359 fun mount_serializer ctxt target some_width module_name args program syms = |
359 fun mount_serializer ctxt target some_width module_name args program syms = |
360 let |
360 let |
361 val (default_width, data, modify) = activate_target ctxt target; |
361 val (default_width, data, modify) = activate_target ctxt target; |
372 let |
372 let |
373 val module_name = if raw_module_name = "" then "" |
373 val module_name = if raw_module_name = "" then "" |
374 else (check_name true raw_module_name; raw_module_name) |
374 else (check_name true raw_module_name; raw_module_name) |
375 val (mounted_serializer, (prepared_syms, prepared_program)) = |
375 val (mounted_serializer, (prepared_syms, prepared_program)) = |
376 mount_serializer ctxt target some_width module_name args program syms; |
376 mount_serializer ctxt target some_width module_name args program syms; |
377 in mounted_serializer prepared_program (if all_public then prepared_syms else []) end; |
377 in mounted_serializer prepared_program (if all_public then [] else prepared_syms) end; |
378 |
378 |
379 fun assert_module_name "" = error "Empty module name not allowed here" |
379 fun assert_module_name "" = error "Empty module name not allowed here" |
380 | assert_module_name module_name = module_name; |
380 | assert_module_name module_name = module_name; |
381 |
381 |
382 fun using_master_directory ctxt = |
382 fun using_master_directory ctxt = |