diff options
| author | Enrico Tassi | 2014-06-26 15:37:46 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-07-10 15:22:58 +0200 |
| commit | edee36d00147dfaa99acf52a7b4d7ebf329b013f (patch) | |
| tree | 0c2920b863f4016e0280ce479000306f696fee3f /tactics | |
| parent | c88f47195955beb615d15dd9d57e4de20e5e3a52 (diff) | |
check_for_interrupt: better (but slower) in threading mode
Experimenting with PIDE I discovered that yield is not sufficient
to have a rescheduling, hence the delay.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 8 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 |
2 files changed, 7 insertions, 3 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 171b1f75a8..2e9d30dfc4 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1213,9 +1213,13 @@ module Strategies = let try_ str : strategy = choice str id + let check_interrupt str e l c t r ev = + Control.check_for_interrupt (); + str e l c t r ev + let fix (f : strategy -> strategy) : strategy = - let rec aux env = f (fun env -> aux env) env in aux - + let rec aux env = f (fun env -> check_interrupt aux env) env in aux + let any (s : strategy) : strategy = fix (fun any -> try_ (seq s any)) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index fcce6e5eba..966d355d42 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -413,7 +413,7 @@ module New = struct let rec tclREPEAT0 t = tclINDEPENDENT begin tclIFCATCH t - (fun () -> tclREPEAT0 t) + (fun () -> tclCHECKINTERRUPT () <*> tclREPEAT0 t) (fun e -> catch_failerror e <*> tclUNIT ()) end let tclREPEAT t = |