--- a/ProgTutorial/Recipes/TimeLimit.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/TimeLimit.thy Fri May 17 10:38:01 2019 +0200
@@ -21,25 +21,25 @@
Now the call
- @{ML_matchresult_fake_both [display,gray] "ackermann (4, 12)" "\<dots>"}
+ @{ML_matchresult_fake_both [display,gray] \<open>ackermann (4, 12)\<close> \<open>\<dots>\<close>}
takes a bit of time before it finishes. To avoid this, the call can be encapsulated
in a time limit of five seconds. For this you have to write
@{ML_matchresult_fake_both [display,gray]
-"Timeout.apply (Time.fromSeconds 5) ackermann (4, 12)
- handle TIMEOUT => ~1"
-"~1"}
+\<open>Timeout.apply (Time.fromSeconds 5) ackermann (4, 12)
+ handle TIMEOUT => ~1\<close>
+\<open>~1\<close>}
where \<open>TimeOut\<close> is the exception raised when the time limit
is reached.
- Note that @{ML "apply" in Timeout} is only meaningful when you use PolyML 5.2.1
+ Note that @{ML \<open>apply\<close> in Timeout} is only meaningful when you use PolyML 5.2.1
or later, because this version of PolyML has the infrastructure for multithreaded
- programming on which @{ML "apply" in Timeout} relies.
+ programming on which @{ML \<open>apply\<close> in Timeout} relies.
\begin{readmore}
- The function @{ML "apply" in Timeout} is defined in the structure
+ The function @{ML \<open>apply\<close> in Timeout} is defined in the structure
@{ML_structure Timeout} which can be found in the file
@{ML_file "Pure/concurrent/timeout.ML"}.
\end{readmore}