src/Tools/Code/code_target.ML
changeset 48371 3a5a5a992519
parent 47576 b32aae03e3d6
child 48426 7b03314ee2ac
equal deleted inserted replaced
48358:04fed0cf775a 48371:3a5a5a992519
   371   in mounted_serializer prepared_program end;
   371   in mounted_serializer prepared_program end;
   372 
   372 
   373 fun assert_module_name "" = error ("Empty module name not allowed.")
   373 fun assert_module_name "" = error ("Empty module name not allowed.")
   374   | assert_module_name module_name = module_name;
   374   | assert_module_name module_name = module_name;
   375 
   375 
       
   376 fun using_master_directory thy = Option.map (Path.append (Thy_Load.master_directory thy));
       
   377 
   376 in
   378 in
   377 
   379 
   378 fun export_code_for thy some_path target some_width module_name args =
   380 fun export_code_for thy some_path target some_width module_name args =
   379   export some_path ooo invoke_serializer thy target some_width module_name args;
   381   export (using_master_directory thy some_path)
       
   382   ooo invoke_serializer thy target some_width module_name args;
   380 
   383 
   381 fun produce_code_for thy target some_width module_name args =
   384 fun produce_code_for thy target some_width module_name args =
   382   let
   385   let
   383     val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
   386     val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
   384   in fn naming => fn program => fn names =>
   387   in fn naming => fn program => fn names =>