--- a/NEWS Mon Jun 22 18:55:47 2015 +0200
+++ b/NEWS Mon Jun 22 19:22:48 2015 +0200
@@ -75,6 +75,9 @@
show A by simp
qed
+* Method "sleep" succeeds after a real-time delay (in seconds). This is
+occasionally useful for demonstration and testing purposes.
+
*** Pure ***
--- a/src/Doc/Isar_Ref/Generic.thy Mon Jun 22 18:55:47 2015 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Mon Jun 22 19:22:48 2015 +0200
@@ -67,11 +67,14 @@
@{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\
@{method_def intro} & : & @{text method} \\
@{method_def elim} & : & @{text method} \\
+ @{method_def fail} & : & @{text method} \\
@{method_def succeed} & : & @{text method} \\
- @{method_def fail} & : & @{text method} \\
+ @{method_def sleep} & : & @{text method} \\
\end{matharray}
@{rail \<open>
+ @@{method sleep} @{syntax real}
+ ;
(@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs}
;
(@@{method erule} | @@{method drule} | @@{method frule})
@@ -114,13 +117,17 @@
this allows fine-tuned decomposition of a proof problem, in contrast
to common automated tools.
+ \item @{method fail} yields an empty result sequence; it is the
+ identity of the ``@{text "|"}'' method combinator (cf.\
+ \secref{sec:proof-meth}).
+
\item @{method succeed} yields a single (unchanged) result; it is
the identity of the ``@{text ","}'' method combinator (cf.\
\secref{sec:proof-meth}).
- \item @{method fail} yields an empty result sequence; it is the
- identity of the ``@{text "|"}'' method combinator (cf.\
- \secref{sec:proof-meth}).
+ \item @{method sleep}~@{text s} succeeds after a real-time delay of @{text
+ s} seconds. This is occasionally useful for demonstration and testing
+ purposes.
\end{description}
--- a/src/Pure/Isar/method.ML Mon Jun 22 18:55:47 2015 +0200
+++ b/src/Pure/Isar/method.ML Mon Jun 22 19:22:48 2015 +0200
@@ -69,6 +69,7 @@
val method_cmd: Proof.context -> Token.src -> Proof.context -> method
val detect_closure_state: thm -> bool
val RUNTIME: cases_tactic -> cases_tactic
+ val sleep: Time.time -> cases_tactic
val evaluate: text -> Proof.context -> method
type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
val modifier: attribute -> Position.T -> modifier
@@ -431,6 +432,8 @@
fun RUNTIME (tac: cases_tactic) st =
if detect_closure_state st then Seq.empty else tac st;
+fun sleep t = RUNTIME (fn st => (OS.Process.sleep t; Seq.single ([], st)));
+
(* evaluate method text *)
@@ -670,6 +673,8 @@
val _ = Theory.setup
(setup @{binding fail} (Scan.succeed (K fail)) "force failure" #>
setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #>
+ setup @{binding sleep} (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s)))
+ "succeed after delay (in seconds)" #>
setup @{binding "-"} (Scan.succeed (K insert_facts))
"do nothing (insert current facts only)" #>
setup @{binding insert} (Attrib.thms >> (K o insert))