From 9d631dff827b656516d735159d39c72c0fddfc5f Mon Sep 17 00:00:00 2001 From: monate Date: Mon, 26 May 2003 08:16:17 +0000 Subject: configure pour CoqIde repare git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4076 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/FAQ | 21 ++++++++++++--------- ide/blaster_window.ml | 43 ++++++++++++++++++++++++++----------------- ide/coqide.ml | 2 +- ide/utf8.v | 4 ++++ 4 files changed, 43 insertions(+), 27 deletions(-) (limited to 'ide') diff --git a/ide/FAQ b/ide/FAQ index 2dcbd1dfd..9f533cdfc 100644 --- a/ide/FAQ +++ b/ide/FAQ @@ -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 "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). -- cgit v1.2.3