diff options
| author | Johan van Selst <johans@FreeBSD.org> | 2010-11-09 07:09:26 +0000 |
|---|---|---|
| committer | Johan van Selst <johans@FreeBSD.org> | 2010-11-09 07:09:26 +0000 |
| commit | 51ccf06067fd968b4524d3b22ded0ae6b6134340 (patch) | |
| tree | f23fe4be0c2a87789313a56e9fefe396300cf975 /math/coq/files | |
| parent | 155dbbd53b20e861f0010d2a3b52fd1b34344399 (diff) | |
| download | ports-51ccf06067fd968b4524d3b22ded0ae6b6134340.tar.gz ports-51ccf06067fd968b4524d3b22ded0ae6b6134340.zip | |
Notes
Diffstat (limited to 'math/coq/files')
| -rw-r--r-- | math/coq/files/ide-coqide.diff | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/math/coq/files/ide-coqide.diff b/math/coq/files/ide-coqide.diff new file mode 100644 index 000000000000..34d8affdbd18 --- /dev/null +++ b/math/coq/files/ide-coqide.diff @@ -0,0 +1,47 @@ +--- coq-8.3/ide/coqide.ml 2010-07-24 17:57:30.000000000 +0200 ++++ coq-8.3/ide/coqide.ml 2010-11-04 23:09:29.000000000 +0100 +@@ -251,27 +251,29 @@ + end + + let do_if_not_computing text f x = +- if Mutex.try_lock coq_computing then +- let threaded_task () = +- prerr_endline "Getting lock"; +- try +- f x; +- prerr_endline "Releasing lock"; +- Mutex.unlock coq_computing; +- with e -> +- prerr_endline "Releasing lock (on error)"; +- Mutex.unlock coq_computing; +- raise e +- in ++ let threaded_task () = ++ if Mutex.try_lock coq_computing then ++ begin ++ prerr_endline "Getting lock"; ++ try ++ f x; ++ prerr_endline "Releasing lock"; ++ Mutex.unlock coq_computing; ++ with e -> ++ prerr_endline "Releasing lock (on error)"; ++ Mutex.unlock coq_computing; ++ raise e ++ end ++ else ++ prerr_endline ++ "Discarded order (computations are ongoing)" ++ in + prerr_endline ("Launching thread " ^ text); + ignore (Glib.Timeout.add ~ms:300 ~callback: + (fun () -> if Mutex.try_lock coq_computing + then (Mutex.unlock coq_computing; false) + else (pbar#pulse (); true))); + ignore (Thread.create threaded_task ()) +- else +- prerr_endline +- "Discarded order (computations are ongoing)" + + (* XXX - 1 appel *) + let kill_input_view i = |