more robust -- avoid race condition wrt. Haskell output in $ISABELLE_TMP/examples/
authorwenzelm
Wed May 31 11:43:37 2017 +0200 (2017-05-31)
changeset 65981e2c25346b156
parent 65980 3bec939bd808
child 65982 5b8fafde7d64
more robust -- avoid race condition wrt. Haskell output in $ISABELLE_TMP/examples/
src/Doc/Codegen/Further.thy
src/Doc/Codegen/Introduction.thy
     1.1 --- a/src/Doc/Codegen/Further.thy	Tue May 30 22:39:18 2017 +0200
     1.2 +++ b/src/Doc/Codegen/Further.thy	Wed May 31 11:43:37 2017 +0200
     1.3 @@ -48,7 +48,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 "$ISABELLE_TMP/examples/rat.ML"
     1.8 +  file "$ISABELLE_TMP/rat.ML"
     1.9  
    1.10  text \<open>
    1.11    \noindent This merely generates the referenced code to the given
     2.1 --- a/src/Doc/Codegen/Introduction.thy	Tue May 30 22:39:18 2017 +0200
     2.2 +++ b/src/Doc/Codegen/Introduction.thy	Wed May 31 11:43:37 2017 +0200
     2.3 @@ -70,7 +70,7 @@
     2.4  text \<open>\noindent Then we can generate code e.g.~for @{text SML} as follows:\<close>
     2.5  
     2.6  export_code %quote empty dequeue enqueue in SML
     2.7 -  module_name Example file "$ISABELLE_TMP/examples/example.ML"
     2.8 +  module_name Example file "$ISABELLE_TMP/example.ML"
     2.9  
    2.10  text \<open>\noindent resulting in the following code:\<close>
    2.11