# HG changeset patch
# User haftmann
# Date 1420881870 -3600
# Node ID f0141b991c8f4fb6bda61d034fd96b69998f9ce9
# Parent  4ef80efc36c8758c9a5dd50a828e6a0a6240014e
avoid writing into source

diff -r 4ef80efc36c8 -r f0141b991c8f src/Doc/Codegen/Evaluation.thy
--- a/src/Doc/Codegen/Evaluation.thy	Fri Jan 09 21:20:07 2015 +0100
+++ b/src/Doc/Codegen/Evaluation.thy	Sat Jan 10 10:24:30 2015 +0100
@@ -326,7 +326,7 @@
   functions Fract
     "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
     "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
-  file "examples/rat.ML"
+  file "$ISABELLE_TMP/examples/rat.ML"
 
 text {*
   \noindent This merely generates the referenced code to the given
diff -r 4ef80efc36c8 -r f0141b991c8f src/Doc/Codegen/Introduction.thy
--- a/src/Doc/Codegen/Introduction.thy	Fri Jan 09 21:20:07 2015 +0100
+++ b/src/Doc/Codegen/Introduction.thy	Sat Jan 10 10:24:30 2015 +0100
@@ -66,7 +66,7 @@
 text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *}
 
 export_code %quote empty dequeue enqueue in SML
-  module_name Example file "examples/example.ML"
+  module_name Example file "$ISABELLE_TMP/examples/example.ML"
 
 text {* \noindent resulting in the following code: *}
 
@@ -87,7 +87,7 @@
 *}
 
 export_code %quote empty dequeue enqueue in Haskell
-  module_name Example file "examples/"
+  module_name Example file "$ISABELLE_TMP/examples/"
 
 text {*
   \noindent This is the corresponding code:
diff -r 4ef80efc36c8 -r f0141b991c8f src/Doc/Codegen/Setup.thy
--- a/src/Doc/Codegen/Setup.thy	Fri Jan 09 21:20:07 2015 +0100
+++ b/src/Doc/Codegen/Setup.thy	Sat Jan 10 10:24:30 2015 +0100
@@ -7,10 +7,9 @@
   "~~/src/HOL/Library/IArray"
 begin
 
-(* FIXME avoid writing into source directory *)
-ML {*
-  Isabelle_System.mkdirs (Path.append (Resources.master_directory @{theory}) (Path.basic "examples"))
-*}
+ML \<open>
+  Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))
+\<close>
 
 ML_file "../antiquote_setup.ML"
 ML_file "../more_antiquote.ML"
diff -r 4ef80efc36c8 -r f0141b991c8f src/Doc/Codegen/document/build
--- a/src/Doc/Codegen/document/build	Fri Jan 09 21:20:07 2015 +0100
+++ b/src/Doc/Codegen/document/build	Sat Jan 10 10:24:30 2015 +0100
@@ -5,6 +5,12 @@
 FORMAT="$1"
 VARIANT="$2"
 
+# ad-hoc patching of temporary path from sources
+perl -i -pe 's/\\isakeyword\{module\{\\isacharunderscore\}name\}\\ Example\\ \\isakeyword\{file\}\\ \{\\isachardoublequoteopen\}.*\{\\isacharslash\}/\\isakeyword{module{\\isacharunderscore}name}\\ Example\\ \\isakeyword{file}\\ {\\isachardoublequoteopen}examples{\\isacharslash}/g' \
+  Introduction.tex
+
 "$ISABELLE_TOOL" logo Isar
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
 
+# clean up afterwards
+rm -rf "${ISABELLE_TMP}/examples"