avoid writing into source
authorhaftmann
Sat Jan 10 10:24:30 2015 +0100 (2015-01-10)
changeset 59334f0141b991c8f
parent 59333 4ef80efc36c8
child 59335 e743ce816cf6
avoid writing into source
src/Doc/Codegen/Evaluation.thy
src/Doc/Codegen/Introduction.thy
src/Doc/Codegen/Setup.thy
src/Doc/Codegen/document/build
     1.1 --- a/src/Doc/Codegen/Evaluation.thy	Fri Jan 09 21:20:07 2015 +0100
     1.2 +++ b/src/Doc/Codegen/Evaluation.thy	Sat Jan 10 10:24:30 2015 +0100
     1.3 @@ -326,7 +326,7 @@
     1.4    functions Fract
     1.5      "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
     1.6      "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
     1.7 -  file "examples/rat.ML"
     1.8 +  file "$ISABELLE_TMP/examples/rat.ML"
     1.9  
    1.10  text {*
    1.11    \noindent This merely generates the referenced code to the given
     2.1 --- a/src/Doc/Codegen/Introduction.thy	Fri Jan 09 21:20:07 2015 +0100
     2.2 +++ b/src/Doc/Codegen/Introduction.thy	Sat Jan 10 10:24:30 2015 +0100
     2.3 @@ -66,7 +66,7 @@
     2.4  text {* \noindent Then we can generate code e.g.~for @{text SML} as follows: *}
     2.5  
     2.6  export_code %quote empty dequeue enqueue in SML
     2.7 -  module_name Example file "examples/example.ML"
     2.8 +  module_name Example file "$ISABELLE_TMP/examples/example.ML"
     2.9  
    2.10  text {* \noindent resulting in the following code: *}
    2.11  
    2.12 @@ -87,7 +87,7 @@
    2.13  *}
    2.14  
    2.15  export_code %quote empty dequeue enqueue in Haskell
    2.16 -  module_name Example file "examples/"
    2.17 +  module_name Example file "$ISABELLE_TMP/examples/"
    2.18  
    2.19  text {*
    2.20    \noindent This is the corresponding code:
     3.1 --- a/src/Doc/Codegen/Setup.thy	Fri Jan 09 21:20:07 2015 +0100
     3.2 +++ b/src/Doc/Codegen/Setup.thy	Sat Jan 10 10:24:30 2015 +0100
     3.3 @@ -7,10 +7,9 @@
     3.4    "~~/src/HOL/Library/IArray"
     3.5  begin
     3.6  
     3.7 -(* FIXME avoid writing into source directory *)
     3.8 -ML {*
     3.9 -  Isabelle_System.mkdirs (Path.append (Resources.master_directory @{theory}) (Path.basic "examples"))
    3.10 -*}
    3.11 +ML \<open>
    3.12 +  Isabelle_System.mkdirs (File.tmp_path (Path.basic "examples"))
    3.13 +\<close>
    3.14  
    3.15  ML_file "../antiquote_setup.ML"
    3.16  ML_file "../more_antiquote.ML"
     4.1 --- a/src/Doc/Codegen/document/build	Fri Jan 09 21:20:07 2015 +0100
     4.2 +++ b/src/Doc/Codegen/document/build	Sat Jan 10 10:24:30 2015 +0100
     4.3 @@ -5,6 +5,12 @@
     4.4  FORMAT="$1"
     4.5  VARIANT="$2"
     4.6  
     4.7 +# ad-hoc patching of temporary path from sources
     4.8 +perl -i -pe 's/\\isakeyword\{module\{\\isacharunderscore\}name\}\\ Example\\ \\isakeyword\{file\}\\ \{\\isachardoublequoteopen\}.*\{\\isacharslash\}/\\isakeyword{module{\\isacharunderscore}name}\\ Example\\ \\isakeyword{file}\\ {\\isachardoublequoteopen}examples{\\isacharslash}/g' \
     4.9 +  Introduction.tex
    4.10 +
    4.11  "$ISABELLE_TOOL" logo Isar
    4.12  "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
    4.13  
    4.14 +# clean up afterwards
    4.15 +rm -rf "${ISABELLE_TMP}/examples"