diff options
| author | gareuselesinge | 2013-09-12 16:32:07 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-09-12 16:32:07 +0000 |
| commit | de0357106fb2ce8918f666d2f237d04dd3636491 (patch) | |
| tree | 8de54d98a0c2e0ee1b81db360468cd8d43adc915 /toplevel | |
| parent | 774159f7805bfddeb253e39bcd8271c58038ca39 (diff) | |
CoqIDE: show number of proofs being checked in background
good test: Nijmegen/QArithSternBrocot/Zaux.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16773 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/stm.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 67e855327b..9310591416 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -631,7 +631,9 @@ end = struct (* {{{ *) let build_proof_here (id,valid) eop = Future.create (fun () -> !reach_known_state ~cache:false eop; - Proof_global.return_proof ~fix_exn:(State.exn_on id ~valid)) + let p = Proof_global.return_proof ~fix_exn:(State.exn_on id ~valid) in + Pp.feedback (Interface.InProgress ~-1); + p) let slave_respond msg = match msg with @@ -680,6 +682,7 @@ end = struct (* {{{ *) build_proof_here exn_info stop else let f, assign = Future.create_delegate () in + Pp.feedback (Interface.InProgress 1); TQueue.push queue (TaskBuildProof(exn_info,start,stop,assign)); f |