--- a/src/Tools/Code/code_target.ML Thu Jul 19 20:52:17 2012 +0200
+++ b/src/Tools/Code/code_target.ML Thu Jul 19 22:21:59 2012 +0200
@@ -373,10 +373,13 @@
fun assert_module_name "" = error ("Empty module name not allowed.")
| assert_module_name module_name = module_name;
+fun using_master_directory thy = Option.map (Path.append (Thy_Load.master_directory thy));
+
in
fun export_code_for thy some_path target some_width module_name args =
- export some_path ooo invoke_serializer thy target some_width module_name args;
+ export (using_master_directory thy some_path)
+ ooo invoke_serializer thy target some_width module_name args;
fun produce_code_for thy target some_width module_name args =
let