# HG changeset patch
# User wenzelm
# Date 1434993768 -7200
# Node ID c0e1c121c7c081c22d6a43c79cf839c37342258c
# Parent  86fc6652c4df1db5cf90e3ab3195faa1f245bd7e
added method "sleep";

diff -r 86fc6652c4df -r c0e1c121c7c0 NEWS
--- 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 ***
 
diff -r 86fc6652c4df -r c0e1c121c7c0 src/Doc/Isar_Ref/Generic.thy
--- 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}
 
diff -r 86fc6652c4df -r c0e1c121c7c0 src/Pure/Isar/method.ML
--- 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))