diff options
-rwxr-xr-x | configure | 13 | ||||
-rw-r--r-- | ide/FAQ | 21 | ||||
-rw-r--r-- | ide/blaster_window.ml | 43 | ||||
-rw-r--r-- | ide/coqide.ml | 2 | ||||
-rw-r--r-- | ide/utf8.v | 4 |
5 files changed, 50 insertions, 33 deletions
@@ -319,12 +319,13 @@ esac if [ "$coqide_spec" = "no" ] ; then if test -x ${CAMLLIB}/lablgtk2; then - if grep -q -w convert_with_fallback ${CAMLLIB}/lablgtk2/glib.mli; then - COQIDE=byte; - fi - # native threads - if test -f ${CAMLLIB}/threads/threads.cmxa; then - COQIDE=opt + if grep -q -w convert_with_fallbacks ${CAMLLIB}/lablgtk2/glib.mli; then + COQIDE=byte + # native threads + if test -f ${CAMLLIB}/threads/threads.cmxa; then + COQIDE=opt; + fi; + else COQIDE=no; fi else COQIDE=no @@ -22,11 +22,12 @@ Notation "∃ x : t | P" := (EXT x:t|P) (at level 1, x,t,P at level 10). ====================================================================== Copy/Paste of these lines from this file will not work outside of CoqIde. You need to load a file containing these lines or to enter the "∀" -using an input method (see Q5). As a convenience, you may put these lines in -a utf8.v file and start coqide with : - coqide -l utf8.v +using an input method (see Q5). To try it just use "Require utf8" from inside +CoqIde. +To enable these notations automatically start coqide with + coqide -l utf8 In the ide subdir of Coq library, you will find a sample utf8.v with some -pretty notations. +pretty simple notations. Q5) How to define an input method for non ASCII symbols? R5)-First solution : type "<CONTROL><SHIFT>2200" to enter a forall in the script widow. @@ -62,9 +63,11 @@ R7) Two solutions are offered: shortcut. Do not forget to save your preferences. Q8) What encoding should I use? What is this \x{iiii} in my file? -R8) The encoding option is related to the way files are saved. Keep it as UTF-8 until - it becomes important for you to exchange files with non UTF-8 aware applications. +R8) The encoding option is related to the way files are saved. + Keep it as UTF-8 until it becomes important for you to exchange files + with non UTF-8 aware applications. + If you choose something else than UTF-8, then missing characters will + be encoded by \x{....} or \x{........} where each dot is an hex. digit. + The number between braces is the hexadecimal UNICODE index for the + missing character. - If you choose something else than UTF-8, then missing characters will be encoded by - \x{....} or \x{........} where the dot is a digit. The number between braces is - the hexadecimal UNICODE index for the missing character. diff --git a/ide/blaster_window.ml b/ide/blaster_window.ml index 414b86c3b..63b6c0675 100644 --- a/ide/blaster_window.ml +++ b/ide/blaster_window.ml @@ -11,6 +11,8 @@ open Gobject.Data open Ideutils +exception Stop + class blaster_window (n:int) = let window = GWindow.window ~allow_grow:true ~allow_shrink:true @@ -68,6 +70,8 @@ object(self) val window = window val roots = Hashtbl.create 17 val tbl = Hashtbl.create 17 + val blaster_lock = Mutex.create () + method lock = blaster_lock method window = window method set root @@ -92,23 +96,28 @@ object(self) method blaster () = - view#expand_all (); - Hashtbl.iter - (fun k (nt,compute,on_click) -> - match compute () with - | Coq.Interrupted -> - prerr_endline "Interrupted" - | Coq.Failed -> - prerr_endline "Failed"; - model#set ~row:nt ~column:status false; - model#set ~row:nt ~column:nb_goals "N/A" - - | Coq.Success n -> - prerr_endline "Success"; - model#set ~row:nt ~column:status true; - model#set ~row:nt ~column:nb_goals (string_of_int n) - ) - tbl + if Mutex.try_lock blaster_lock then begin + view#expand_all (); + try Hashtbl.iter + (fun k (nt,compute,on_click) -> + match compute () with + | Coq.Interrupted -> + prerr_endline "Interrupted"; + raise Stop + | Coq.Failed -> + prerr_endline "Failed"; + model#set ~row:nt ~column:status false; + model#set ~row:nt ~column:nb_goals "N/A" + + | Coq.Success n -> + prerr_endline "Success"; + model#set ~row:nt ~column:status true; + model#set ~row:nt ~column:nb_goals (string_of_int n) + ) + tbl; + Mutex.unlock blaster_lock + with Stop -> Mutex.unlock blaster_lock + end else prerr_endline "blaster is till computing" initializer ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true)); diff --git a/ide/coqide.ml b/ide/coqide.ml index cbd5c1d11..719a8fcbe 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1226,7 +1226,7 @@ Please restart and report NOW."; else prerr_endline "undo_last_step discarded" - method blaster () = + method blaster () = prerr_endline "Blaster called"; let c = Blaster_window.blaster_window () in c#clear (); diff --git a/ide/utf8.v b/ide/utf8.v index 801aaa8c2..98c2e9638 100644 --- a/ide/utf8.v +++ b/ide/utf8.v @@ -1,5 +1,9 @@ (* Logic *) Notation "∀ x : t , P" := (x:t)P (at level 1, x,t,P at level 10). +Notation "∀ x y : t , P" := (x:t)(y:t)P (at level 1, x,y,t,P at level 10). +Notation "∀ x y z : t , P" := (x:t)(y:t)(z:t) P (at level 1, x,y,z,t,P at level 10). +Notation "∀ x y z u : t , P" := (x:t)(y:t)(z:t)(u:t)P (at level 1, x,y,z,u,t,P at level 10). + Notation "∃ x : t , P" := (EXT x:t|P) (at level 1, x,t,P at level 10). Notation "x ∨ y" := (x \/ y) (at level 1, y at level 10). Notation "x ∧ y" := (x /\ y) (at level 1, y at level 10). |