src/Tools/Code/code_target.ML
changeset 49441 7b03314ee2ac
parent 49386 3a5a5a992519
child 49583 084cd758a8ab
equal deleted inserted replaced
49434:6d7b6e47f3ef 49441:7b03314ee2ac
   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));
   376 fun using_master_directory thy =
       
   377   Option.map (Path.append (File.pwd ()) o Path.append (Thy_Load.master_directory thy));
   377 
   378 
   378 in
   379 in
   379 
   380 
   380 fun export_code_for thy some_path target some_width module_name args =
   381 fun export_code_for thy some_path target some_width module_name args =
   381   export (using_master_directory thy some_path)
   382   export (using_master_directory thy some_path)