# HG changeset patch
# User haftmann
# Date 1342729319 -7200
# Node ID 3a5a5a992519c45124930e269a614011b38d73aa
# Parent  04fed0cf775a52fc10e970f82901ad605be31c65
export code relatively to master directory

diff -r 04fed0cf775a -r 3a5a5a992519 NEWS
--- a/NEWS	Thu Jul 19 20:52:17 2012 +0200
+++ b/NEWS	Thu Jul 19 22:21:59 2012 +0200
@@ -15,6 +15,11 @@
 
 *** Pure ***
 
+* Command "export_code": relative file names are interpreted
+relatively to master directory of current theory rather than
+the rather arbitrary current working directory.
+INCOMPATIBILITY.
+
 * Discontinued obsolete attribute "COMP".  Potential INCOMPATIBILITY,
 use regular rule composition via "OF" / "THEN", or explicit proof
 structure instead.  Note that Isabelle/ML provides a variety of
diff -r 04fed0cf775a -r 3a5a5a992519 src/Tools/Code/code_target.ML
--- 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