Permalink
Browse files

Coqide: get rid of threads, use gtk asynchronous i/o instead

 Threads were only there to handle blocking dialogs with the different
 coqtops. But programming with threads have drawbacks : complex mutex
 infrastructure, possible deadlocks, etc. In particular gtk functions
 are not meant to be called from a thread which isn't the gtk main loop,
 (unless some gtk mutex have been taken). This seem to pose problem
 specifically in win32 (and macosx ?), hence the use of the
 GtkThread.(a)sync hack for scheduling code for execution in the gtk
 main loop.

 Instead, we now use the Glib.Io module to install a callback that will
 be runned when some answer of coqtop is available on the channel.
 This implies using now a continuation-passing style: for instance,
 instead of two sequential requests to coqtop, we'll now have the
 2nd request inside the callback handling the answer to the 1st request.

 Remarks:

 - Also use asynchronous i/o for external commands (editor, coqc, make...).
   Launching an external editor or browser won't freeze coqide anymore.

 - Reworked handling of coqtop process, especially when closing them.
   A responsive coqtop should now hara-kiri immediatly when its input
   channel is closed. Otherwise we try later a soft kill, then some
   hard kills if necessary. If nothing work we warns the user.
   When quitting coqide, all this might induce a small delay (2s at worse).

 - Be careful now to avoid "long" computations (or blocking i/o) in
   a coqide function. Experimentally, it seems that loading/saving a .v
   file is quick enough. If necessary, we could use asynchronous i/o
   also for writing the .v, but for loading I've no clue.

 - In the Coqide module, we ensure that the current continuation k
   will indeed be run at the end thanks to an abstract return type
   (void = opaque copy of unit).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16049 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent e7e52a4 commit 6254115b358899886163da4a4add6d419a55b1e9 letouzey committed Dec 8, 2012
Showing with 988 additions and 962 deletions.
  1. +5 −5 Makefile.build
  2. +2 −2 _tags
  3. +263 −227 ide/coq.ml
  4. +72 −50 ide/coq.mli
  5. +405 −455 ide/coqide.ml
  6. +5 −1 ide/coqide.mli
  7. +9 −14 ide/coqide_main.ml4
  8. +114 −87 ide/ideutils.ml
  9. +15 −7 ide/ideutils.mli
  10. +16 −22 ide/wg_Command.ml
  11. +78 −88 ide/wg_ScriptView.ml
  12. +2 −2 ide/wg_ScriptView.mli
  13. +2 −2 myocamlbuild.ml
View
10 Makefile.build
@@ -302,7 +302,7 @@ plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ))
# target to build CoqIde
coqide:: coqide-files coqide-binaries theories/Init/Prelude.vo
-COQIDEFLAGS=-thread $(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
+COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
.SUFFIXES:.vo
@@ -317,8 +317,8 @@ coqide-files: $(IDEFILES)
ifeq ($(HASCOQIDE),opt)
$(COQIDE): $(LINKIDEOPT) | $(COQTOPEXE)
$(SHOW)'OCAMLOPT -o $@'
- $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa \
- lablgtk.cmxa lablgtksourceview2.cmxa $(IDEOPTFLAGS) gtkThread.cmx \
+ $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa \
+ lablgtk.cmxa lablgtksourceview2.cmxa $(IDEOPTFLAGS) \
str.cmxa $(LINKIDEOPT)
$(STRIP) $@
else
@@ -328,8 +328,8 @@ endif
$(COQIDEBYTE): $(LINKIDE) | $(COQTOPBYTE)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma\
- lablgtksourceview2.cma gtkThread.cmo str.cma $(LINKIDE)
+ $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma lablgtk.cma \
+ lablgtksourceview2.cma str.cma $(LINKIDE)
# install targets
View
4 _tags
@@ -8,15 +8,15 @@
<tools/coq_tex.{native,byte}> : use_str
<tools/coq_makefile.{native,byte}> : use_str, use_unix
<tools/coqdoc/main.{native,byte}> : use_str
-<ide/coqide_main.{native,byte}> : use_str, use_unix, thread, ide
+<ide/coqide_main.{native,byte}> : use_str, use_unix, ide
<checker/main.{native,byte}> : use_str, use_unix
<plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix
<tools/mkwinapp.{native,byte}> : use_unix
<tools/fake_ide.{native,byte}> : use_unix
## tags for ide
-<ide/**/*.{ml,mli}>: thread, ide
+<ide/**/*.{ml,mli}>: ide
## tags for grammar.cm*
View
490 ide/coq.ml
@@ -158,65 +158,127 @@ let check_connection args =
(** Useful stuff *)
-let atomically mtx f arg =
- Mutex.lock mtx;
- try
- let ans = f arg in
- Mutex.unlock mtx;
- ans
- with err ->
- Mutex.unlock mtx;
- raise err
-
let ignore_error f arg =
try ignore (f arg) with _ -> ()
+(** An abstract copy of unit.
+ This will help ensuring that we do not forget to finally call
+ continuations when building tasks in other modules. *)
+
+type void = Void
+
+(** ccb : existential type for a (call + callback) type.
+
+ Reference: http://alan.petitepomme.net/cwn/2004.01.13.html
+ To rewrite someday with GADT. *)
+
+type 'a poly_ccb = 'a Serialize.call * ('a Interface.value -> void)
+type 't scoped_ccb = { bind_ccb : 'a. 'a poly_ccb -> 't }
+type ccb = { open_ccb : 't. 't scoped_ccb -> 't }
+
+let mk_ccb poly = { open_ccb = fun scope -> scope.bind_ccb poly }
+let with_ccb ccb e = ccb.open_ccb e
+
+let interrupter = ref (fun pid -> Unix.kill pid Sys.sigint)
+let soft_killer = ref (fun pid -> Unix.kill pid Sys.sigterm)
+let killer = ref (fun pid -> Unix.kill pid Sys.sigkill)
+
+(** Handling old processes *)
+
+type unix_process_id = int
+type retry = int
+
+let zombies = ref ([] : (unix_process_id * retry) list)
+
+let pr_zombies ?(full=false) l =
+ let pr (pid,retries) =
+ string_of_int pid ^
+ if full then "["^string_of_int retries^"]" else ""
+ in
+ String.concat ", " (List.map pr l)
+
+let is_buried pid =
+ try fst (Unix.waitpid [Unix.WNOHANG] pid) <> 0
+ with Unix.Unix_error _ -> false
+
+let max_retry = 3 (* one soft then two hard kill attempts *)
+
+let countdown = ref None
+let final_countdown () = (countdown := Some max_retry)
+
+let check_zombies () =
+ (* First, do [waitpid] on our zombies and try to kill the survivors *)
+ let handle_zombie others (pid,retries) =
+ if is_buried pid then others
+ else
+ let () = match retries with
+ | 0 -> () (* freshly closed coqtop, leave it some time *)
+ | 1 -> ignore_error !soft_killer pid
+ | _ -> ignore_error !killer pid
+ in (pid,retries+1) :: others
+ in
+ let zs = List.fold_left handle_zombie [] !zombies
+ in
+ if zs <> [] then
+ Minilib.log ("Remaining zombies: "^ pr_zombies ~full:true zs);
+ (* Second, we warn the user about old zombies that refuses to die
+ (except in the middle of the final countdown) *)
+ let chk_old = !countdown = None || !countdown = Some 0 in
+ let old_zombies, new_zombies =
+ List.partition (fun (_,n) -> chk_old && n >= max_retry) zs
+ in
+ if old_zombies <> [] then begin
+ let msg1 = "Some coqtop processes are still running.\n" in
+ let msg2 = "You may have to kill them manually.\nPids: " in
+ let msg3 = pr_zombies old_zombies in
+ let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.close
+ ~message_type:`ERROR ~message:(msg1 ^ msg2 ^ msg3) ()
+ in
+ ignore (popup#run ());
+ ignore (popup#destroy ())
+ end;
+ zombies := new_zombies;
+ (* Finally, we might end coqide if the final countdown has started *)
+ if !countdown = Some 0 || (!countdown <> None && zs = []) then exit 0;
+ countdown := Option.map pred !countdown;
+ true
+
+let _ = Glib.Timeout.add ~ms:300 ~callback:check_zombies
+
(** * The structure describing a coqtop sub-process *)
type handle = {
- pid : int;
- (* Unix process id *)
- cout : in_channel;
+ pid : unix_process_id;
+ cout : Unix.file_descr;
cin : out_channel;
mutable alive : bool;
- xml_parser : Xml_parser.t;
+ mutable waiting_for : (ccb * logger) option; (* last call + callback + log *)
}
-type coqtop = {
- (* lock managing coqtop access *)
- lock : Mutex.t;
- (* non quoted command-line arguments of coqtop *)
- sup_args : string list;
- (* actual coqtop process *)
- mutable handle : handle;
- (* trigger called whenever coqtop dies abruptly *)
- trigger : handle -> unit;
- (* whether coqtop may be relaunched *)
- mutable is_closed : bool;
- (* whether coqtop is computing *)
- mutable is_computing : bool;
- (* whether coqtop is waiting to be resetted *)
- mutable is_to_reset : bool;
-}
-
-(** Invariants:
- - any outside request takes the coqtop.lock and is discarded when
- [is_closed = true].
- - coqtop.handle may be written ONLY when toplvl_ctr_mtx AND coqtop.lock is
- taken.
+(** Coqtop process status :
+ - New : a process has been spawned, but not initialized via [init_coqtop].
+ It will reject tasks given via [try_grab].
+ - Ready : no current task, accepts new tasks via [try_grab].
+ - Busy : has accepted a task via [init_coqtop] or [try_grab],
+ It will reject other tasks for the moment
+ - Closed : the coqide buffer has been closed, we discard any further task.
*)
-type logger = Interface.message_level -> string -> unit
+type status = New | Ready | Busy | Closed
-exception DeadCoqtop
+type task = handle -> (unit -> void) -> void
-(** * Count of all active coqtops *)
+type reset_kind = Planned | Unexpected
-let toplvl_ctr = ref 0
-
-let toplvl_ctr_mtx = Mutex.create ()
-
-let coqtop_zombies () = !toplvl_ctr
+type coqtop = {
+ (* non quoted command-line arguments of coqtop *)
+ sup_args : string list;
+ (* called whenever coqtop dies *)
+ mutable reset_handler : reset_kind -> task;
+ (* actual coqtop process and its status *)
+ mutable handle : handle;
+ mutable status : status;
+}
(** * Starting / signaling / ending a real coqtop sub-process *)
@@ -259,201 +321,174 @@ let open_process_pid prog args =
assert (pid <> 0);
Unix.close ide2top_r;
Unix.close top2ide_w;
- let oc = Unix.out_channel_of_descr ide2top_w in
- let ic = Unix.in_channel_of_descr top2ide_r in
- set_binary_mode_out oc true;
- set_binary_mode_in ic true;
- (pid,ic,oc)
+ (pid,top2ide_r,Unix.out_channel_of_descr ide2top_w)
+
+exception TubeError
+exception AnswerWithoutRequest
+
+let install_input_watch handle respawner =
+ let io_chan = Glib.Io.channel_of_descr handle.cout in
+ let all_conds = [`ERR; `HUP; `IN; `NVAL; `PRI] in (* all except `OUT *)
+ let rec check_errors = function
+ | [] -> ()
+ | (`IN | `PRI) :: conds -> check_errors conds
+ | e :: _ -> raise TubeError
+ in
+ let handle_intermediate_message logger xml =
+ let message = Serialize.to_message xml in
+ let level = message.Interface.message_level in
+ let content = message.Interface.message_content in
+ logger level content
+ in
+ let handle_final_answer ccb xml =
+ Minilib.log "Handling coqtop answer";
+ handle.waiting_for <- None;
+ with_ccb ccb { bind_ccb = fun (c,f) -> f (Serialize.to_answer xml c) }
+ in
+ let unsafe_handle_input conds =
+ check_errors conds;
+ let s = io_read_all io_chan in
+ if s = "" then raise TubeError;
+ match handle.waiting_for with
+ |None -> raise AnswerWithoutRequest
+ |Some (ccb,logger) ->
+ let p = Xml_parser.make (Xml_parser.SString s) in
+ let rec loop () =
+ let xml = Xml_parser.parse p in
+ if Serialize.is_message xml then
+ (handle_intermediate_message logger xml; loop ())
+ else
+ ignore (handle_final_answer ccb xml)
+ in
+ try loop ()
+ with Xml_parser.Error (Xml_parser.Empty, _) -> () (* end of s *)
+ in
+ let print_exception = function
+ | Xml_parser.Error e -> Xml_parser.error e
+ | Serialize.Marshal_error -> "Protocol violation"
+ | e -> Printexc.to_string e
+ in
+ let handle_input conds =
+ if not handle.alive then false (* coqtop already terminated *)
+ else
+ try unsafe_handle_input conds; true
+ with e ->
+ Minilib.log ("Coqtop reader failed, resetting: "^print_exception e);
+ respawner ();
+ false
+ in
+ ignore (Glib.Io.add_watch ~cond:all_conds ~callback:handle_input io_chan)
(** This launches a fresh handle from its command line arguments. *)
-let unsafe_spawn_handle args =
+let spawn_handle args =
let prog = coqtop_path () in
let args = Array.of_list (prog :: "-ideslave" :: args) in
- let (pid, ic, oc) = open_process_pid prog args in
- let p = Xml_parser.make (Xml_parser.SChannel ic) in
- Xml_parser.check_eof p false;
- incr toplvl_ctr;
+ let (pid, in_fd, oc) = open_process_pid prog args in
{
pid = pid;
cin = oc;
- cout = ic;
+ cout = in_fd;
alive = true;
- xml_parser = p;
+ waiting_for = None;
}
(** This clears any potentially remaining open garbage. *)
-let unsafe_clear_handle coqtop =
- let handle = coqtop.handle in
- if handle.alive then begin
+let clear_handle h =
+ if h.alive then begin
(* invalidate the old handle *)
- handle.alive <- false;
- ignore_error close_out handle.cin;
- ignore_error close_in handle.cout;
- ignore_error (Unix.waitpid []) handle.pid;
- decr toplvl_ctr
+ h.alive <- false;
+ ignore_error close_out h.cin;
+ ignore_error Unix.close h.cout;
+ (* we monitor the death of the old process *)
+ zombies := (h.pid,0) :: !zombies
end
-let spawn_coqtop hook sup_args =
- let handle =
- atomically toplvl_ctr_mtx unsafe_spawn_handle sup_args
- in
+let mkready coqtop =
+ fun () -> coqtop.status <- Ready; Void
+
+let rec respawn_coqtop ?(why=Unexpected) coqtop =
+ clear_handle coqtop.handle;
+ ignore_error (fun () -> coqtop.handle <- spawn_handle coqtop.sup_args) ();
+ (* Normally, the handle is now a fresh one.
+ If not, there isn't much we can do ... *)
+ assert (coqtop.handle.alive = true);
+ coqtop.status <- New;
+ install_input_watch coqtop.handle (fun () -> respawn_coqtop coqtop);
+ ignore (coqtop.reset_handler why coqtop.handle (mkready coqtop))
+
+let spawn_coqtop sup_args =
+ let ct =
{
- handle = handle;
- lock = Mutex.create ();
+ handle = spawn_handle sup_args;
sup_args = sup_args;
- trigger = hook;
- is_closed = false;
- is_computing = false;
- is_to_reset = false;
+ reset_handler = (fun _ _ k -> k ());
+ status = New;
}
+ in
+ install_input_watch ct.handle (fun () -> respawn_coqtop ct);
+ ct
-let interrupter = ref (fun pid -> Unix.kill pid Sys.sigint)
-let killer = ref (fun pid -> Unix.kill pid Sys.sigkill)
+let set_reset_handler coqtop hook = coqtop.reset_handler <- hook
+
+let is_computing coqtop = (coqtop.status = Busy)
-let is_computing coqtop = coqtop.is_computing
+(* For closing a coqtop, we don't try to send it a Quit call anymore,
+ but rather close its channels:
+ - a listening coqtop will handle this just as a Quit call
+ - a busy coqtop will anyway have to be killed *)
-let is_closed coqtop = coqtop.is_closed
+let close_coqtop coqtop =
+ coqtop.status <- Closed;
+ clear_handle coqtop.handle
+
+let reset_coqtop coqtop = respawn_coqtop ~why:Planned coqtop
-(** These are asynchronous signals *)
let break_coqtop coqtop =
try !interrupter coqtop.handle.pid
with _ -> Minilib.log "Error while sending Ctrl-C"
-let kill_coqtop coqtop =
- try !killer coqtop.handle.pid
- with _ -> Minilib.log "Kill -9 failed. Process already terminated ?"
+let process_task coqtop task =
+ assert (coqtop.status = Ready || coqtop.status = New);
+ coqtop.status <- Busy;
+ try ignore (task coqtop.handle (mkready coqtop))
+ with e ->
+ Minilib.log ("Coqtop writer failed, resetting: " ^ Printexc.to_string e);
+ if coqtop.status <> Closed then respawn_coqtop coqtop
-let unsafe_process coqtop f =
- coqtop.is_computing <- true;
- try
- f coqtop.handle;
- coqtop.is_computing <- false;
- Mutex.unlock coqtop.lock
- with
- | DeadCoqtop ->
- coqtop.is_computing <- false;
- Mutex.lock toplvl_ctr_mtx;
- (* Coqtop died from an non natural cause, we have the lock, so it's our duty
- to relaunch it here. *)
- if not coqtop.is_closed && not coqtop.is_to_reset then begin
- ignore_error unsafe_clear_handle coqtop;
- let try_respawn () =
- coqtop.handle <- unsafe_spawn_handle coqtop.sup_args;
- in
- ignore_error try_respawn ();
- (* If respawning coqtop failed, there is not much we can do... *)
- assert (coqtop.handle.alive = true);
- (* Process the reset callback *)
- ignore_error coqtop.trigger coqtop.handle;
- end;
- Mutex.unlock toplvl_ctr_mtx;
- Mutex.unlock coqtop.lock;
- | err ->
- (* Another error occured, we propagate it. *)
- coqtop.is_computing <- false;
- Mutex.unlock coqtop.lock;
- raise err
-
-let grab coqtop f =
- Mutex.lock coqtop.lock;
- if not coqtop.is_closed && not coqtop.is_to_reset then unsafe_process coqtop f
- else Mutex.unlock coqtop.lock
-
-let try_grab coqtop f g =
- if Mutex.try_lock coqtop.lock then
- if not coqtop.is_closed && not coqtop.is_to_reset then unsafe_process coqtop f
- else Mutex.unlock coqtop.lock
- else g ()
+let try_grab coqtop task abort =
+ match coqtop.status with
+ |Closed -> ()
+ |Busy|New -> abort ()
+ |Ready -> process_task coqtop task
+
+let init_coqtop coqtop task =
+ assert (coqtop.status = New);
+ process_task coqtop task
(** * Calls to coqtop *)
(** Cf [Ide_intf] for more details *)
-let eval_call coqtop logger c =
- (** Retrieve the messages sent by coqtop until an answer has been received *)
- let rec loop () =
- let xml = Xml_parser.parse coqtop.xml_parser in
- if Serialize.is_message xml then
- let message = Serialize.to_message xml in
- let level = message.Interface.message_level in
- let content = message.Interface.message_content in
- let () = logger level content in
- loop ()
- else (Serialize.to_answer xml c)
- in
- try
- Xml_utils.print_xml coqtop.cin (Serialize.of_call c);
- flush coqtop.cin;
- loop ()
- with
- | Serialize.Marshal_error ->
- (* the protocol was not respected... *)
- raise Serialize.Marshal_error
- | err ->
- (* if anything else happens here, coqtop is most likely dead *)
- let msg = Printf.sprintf "Error communicating with pid [%i]: %s"
- coqtop.pid (Printexc.to_string err)
- in
- Minilib.log msg;
- raise DeadCoqtop
-
-let interp coqtop log ?(raw=false) ?(verbose=true) s =
- eval_call coqtop log (Serialize.interp (raw,verbose,s))
-let rewind coqtop i = eval_call coqtop default_logger (Serialize.rewind i)
-let inloadpath coqtop s = eval_call coqtop default_logger (Serialize.inloadpath s)
-let mkcases coqtop s = eval_call coqtop default_logger (Serialize.mkcases s)
-let status coqtop = eval_call coqtop default_logger Serialize.status
-let hints coqtop = eval_call coqtop default_logger Serialize.hints
-let search coqtop flags = eval_call coqtop default_logger (Serialize.search flags)
-
-let unsafe_close coqtop =
- if Mutex.try_lock coqtop.lock then begin
- let () =
- try
- match eval_call coqtop.handle default_logger Serialize.quit with
- | Interface.Good _ -> ()
- | _ -> raise Exit
- with err -> kill_coqtop coqtop
- in
- Mutex.unlock coqtop.lock
- end else begin
- (* bring me the chainsaw! *)
- kill_coqtop coqtop
- end
-
-let close_coqtop coqtop =
- (* wait for acquiring the process management lock *)
- atomically toplvl_ctr_mtx (fun _ -> coqtop.is_closed <- true) ();
- (* try to quit coqtop gently *)
- unsafe_close coqtop;
- (* Finalize the handle *)
- Mutex.lock coqtop.lock;
- Mutex.lock toplvl_ctr_mtx;
- ignore_error unsafe_clear_handle coqtop;
- Mutex.unlock toplvl_ctr_mtx;
- Mutex.unlock coqtop.lock
-
-let reset_coqtop coqtop hook =
- (* wait for acquiring the process management lock *)
- atomically toplvl_ctr_mtx (fun _ -> coqtop.is_to_reset <- true) ();
- (* try to quit coqtop gently *)
- unsafe_close coqtop;
- (* Reset the handle *)
- Mutex.lock coqtop.lock;
- Mutex.lock toplvl_ctr_mtx;
- ignore_error unsafe_clear_handle coqtop;
- let try_respawn () =
- coqtop.handle <- unsafe_spawn_handle coqtop.sup_args;
- in
- ignore_error try_respawn ();
- (* If respawning coqtop failed, there is not much we can do... *)
- assert (coqtop.handle.alive = true);
- (* Reset done *)
- coqtop.is_to_reset <- false;
- (* Process the reset callback with the given hook *)
- ignore_error hook coqtop.handle;
- Mutex.unlock toplvl_ctr_mtx;
- Mutex.unlock coqtop.lock
+type 'a atask = handle -> ('a Interface.value -> void) -> void
+
+let eval_call ?(logger=default_logger) call handle k =
+ (** Send messages to coqtop and prepare the decoding of the answer *)
+ Minilib.log ("Start eval_call " ^ Serialize.pr_call call);
+ assert (handle.alive && handle.waiting_for = None);
+ handle.waiting_for <- Some (mk_ccb (call,k), logger);
+ Xml_utils.print_xml handle.cin (Serialize.of_call call);
+ flush handle.cin;
+ Minilib.log "End eval_call";
+ Void
+
+let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) s =
+ eval_call ~logger (Serialize.interp (raw,verbose,s))
+let rewind i = eval_call (Serialize.rewind i)
+let inloadpath s = eval_call (Serialize.inloadpath s)
+let mkcases s = eval_call (Serialize.mkcases s)
+let status = eval_call Serialize.status
+let hints = eval_call Serialize.hints
+let search flags = eval_call (Serialize.search flags)
module PrintOpt =
struct
@@ -473,26 +508,27 @@ struct
let state_hack = Hashtbl.create 11
let _ = List.iter (fun opt -> Hashtbl.add state_hack opt false)
- [ implicit; coercions; raw_matching; notations; all_basic; existential; universes ]
-
- let set coqtop options =
- let () = List.iter (fun (name, v) -> Hashtbl.replace state_hack name v) options in
- let options = List.map (fun (name, v) -> (name, Interface.BoolValue v)) options in
- let options = (width, Interface.IntValue !width_ref):: options in
- match eval_call coqtop default_logger (Serialize.set_options options) with
- | Interface.Good () -> ()
- | _ -> raise (Failure "Cannot set options.")
-
- let enforce_hack coqtop =
- let elements = Hashtbl.fold (fun opt v acc -> (opt, v) :: acc) state_hack [] in
- set coqtop elements
+ [ implicit; coercions; raw_matching; notations;
+ all_basic; existential; universes ]
+
+ let set opts h k =
+ List.iter (fun (name, v) -> Hashtbl.replace state_hack name v) opts;
+ let opts = List.map (fun (n, v) -> (n, Interface.BoolValue v)) opts in
+ let opts = (width, Interface.IntValue !width_ref):: opts in
+ eval_call (Serialize.set_options opts) h
+ (function
+ | Interface.Good () -> k ()
+ | _ -> failwith "Cannot set options. Resetting coqtop")
+
+ let enforce_hack h k =
+ let elements = Hashtbl.fold (fun opt v acc -> (opt, v) :: acc) state_hack []
+ in
+ set elements h k
end
-let goals coqtop =
- let () = PrintOpt.enforce_hack coqtop in
- eval_call coqtop default_logger Serialize.goals
+let goals h k =
+ PrintOpt.enforce_hack h (fun () -> eval_call Serialize.goals h k)
-let evars coqtop =
- let () = PrintOpt.enforce_hack coqtop in
- eval_call coqtop default_logger Serialize.evars
+let evars h k =
+ PrintOpt.enforce_hack h (fun () -> eval_call Serialize.evars h k)
View
122 ide/coq.mli
@@ -27,82 +27,104 @@ val check_connection : string list -> unit
(** * The structure describing a coqtop sub-process *)
(** Liveness management of coqtop is automatic. Whenever a Coqtop dies abruptly,
- this module is responsible for relaunching the whole process. The hook
+ this module is responsible for relaunching the whole process. The hook
passed as an argument in coqtop construction will be called after such an
- abrupt failure. In particular, it is NOT called when explicitely requesting
+ abrupt failure. In particular, it is NOT called when explicitely requesting
coqtop to close or to reset. *)
type coqtop
type handle
-(** Count of all active coqtops *)
-val coqtop_zombies : unit -> int
+(** * Coqtop tasks
+
+ A task is a group of sequential calls to be perform on a coqtop.
+ If a task is already sent to coqtop, it is considered busy
+ ([is_computing] will answer [true]), and other task submission
+ will be rejected.
+
+ A task is represented as a continuation, with a coqtop [handle]
+ as first argument, and a final inner continuation as 2nd argument.
+ This inner continuation should be runned at the end of the task.
+ Any exception occuring within the task will trigger a coqtop reset.
+*)
+
+type void
+type task = handle -> (unit->void) -> void
+
+(** Check if coqtop is computing, i.e. already has a current task *)
+val is_computing : coqtop -> bool
(** * Starting / signaling / ending a real coqtop sub-process *)
-(** Create a coqtop process out of a hook and some command-line arguments.
- The hook SHALL NOT use [grab] or its variants, otherwise you'll deadlock! *)
-val spawn_coqtop : (handle -> unit) -> string list -> coqtop
+(** Create a coqtop process with some command-line arguments. *)
+val spawn_coqtop : string list -> coqtop
-(** Interrupt the current computation of coqtop. Asynchronous. *)
+(** Register a handler called when a coqtop dies (badly or on purpose) *)
+type reset_kind = Planned | Unexpected
+val set_reset_handler : coqtop -> (reset_kind -> task) -> unit
+
+(** Finish initializing a freshly spawned coqtop, by running a first task on it.
+ The task should run its inner continuation at the end. *)
+val init_coqtop : coqtop -> task -> unit
+
+(** Interrupt the current computation of coqtop. *)
val break_coqtop : coqtop -> unit
(** Close coqtop. Subsequent requests will be discarded. Hook ignored. *)
val close_coqtop : coqtop -> unit
-(** Reset coqtop. Pending requests will be discarded. Default hook ignored,
- provided one used instead. *)
-val reset_coqtop : coqtop -> (handle -> unit) -> unit
+(** Reset coqtop. Pending requests will be discarded. The reset handler
+ of coqtop will be called with [Planned] as first argument *)
+val reset_coqtop : coqtop -> unit
-(** Last resort against a reluctant coqtop (a.k.a. chainsaw massacre).
- Asynchronous. *)
-val kill_coqtop : coqtop -> unit
+(** In win32, we'll use a different kill function than Unix.kill *)
-(** * Coqtop commmunication *)
+val killer : (int -> unit) ref
+val soft_killer : (int -> unit) ref
+val interrupter : (int -> unit) ref
-(** Start a coqtop dialogue and ensure that there is no interfering process.
- - If coqtop ever dies during the computation, this function restarts coqtop
- and calls the restart hook with the fresh coqtop.
- - If the argument function raises an exception, it is propagated.
- - The request may be discarded if a [close_coqtop] or [reset_coqtop] occurs
- before its completion.
-*)
-val grab : coqtop -> (handle -> unit) -> unit
+(** [set_final_countdown] triggers an exit of coqide after
+ some last cycles for closing remaining coqtop zombies *)
-(** As [grab], but applies the second callback if coqtop is already busy. Please
- consider using [try_grab] instead of [grab] except if you REALLY want
- something to happen. *)
-val try_grab : coqtop -> (handle -> unit) -> (unit -> unit) -> unit
+val final_countdown : unit -> unit
-(** Check if coqtop is computing. Does not take any lock. *)
-val is_computing : coqtop -> bool
+(** * Coqtop commmunication *)
-(** Check if coqtop is closed. Does not take any lock. *)
-val is_closed : coqtop -> bool
+(** Try to schedule a task on a coqtop. If coqtop is available, the task
+ callback is run (asynchronously), otherwise the [(unit->unit)] callback
+ is triggered.
+ - If coqtop ever dies during the computation, this function restarts coqtop
+ and calls the restart hook with the fresh coqtop.
+ - If the argument function raises an exception, a coqtop reset occurs.
+ - The task may be discarded if a [close_coqtop] or [reset_coqtop] occurs
+ before its completion.
+ - The task callback should run its inner continuation at the end. *)
-(** In win32, we'll use a different kill function than Unix.kill *)
+val try_grab : coqtop -> task -> (unit -> unit) -> unit
-val killer : (int -> unit) ref
-val interrupter : (int -> unit) ref
+(** * Atomic calls to coqtop
-(** * Calls to Coqtop, cf [Serialize] for more details *)
+ These atomic calls can be combined to form arbitrary multi-call tasks.
+ They correspond to the protocol calls (cf [Serialize] for more details).
+ Note that each call is asynchronous: it will return immediately,
+ but the inner callback will be executed later to handle the call answer
+ when this answer is available.
+ Except for interp, we use the default logger for any call. *)
-type logger = Interface.message_level -> string -> unit
-(** Except for interp, we use the default logger for any call. *)
+type 'a atask = handle -> ('a Interface.value -> void) -> void
-val interp :
- handle -> logger -> ?raw:bool -> ?verbose:bool -> string -> string Interface.value
-val rewind : handle -> int -> int Interface.value
-val status : handle -> Interface.status Interface.value
-val goals : handle -> Interface.goals option Interface.value
-val evars : handle -> Interface.evar list option Interface.value
-val hints : handle -> (Interface.hint list * Interface.hint) option Interface.value
-val inloadpath : handle -> string -> bool Interface.value
-val mkcases : handle -> string -> string list list Interface.value
-val search : handle -> Interface.search_flags -> string Interface.coq_object list Interface.value
+val interp : ?logger:Ideutils.logger -> ?raw:bool -> ?verbose:bool ->
+ string -> string atask
+val rewind : int -> int atask
+val status : Interface.status atask
+val goals : Interface.goals option atask
+val evars : Interface.evar list option atask
+val hints : (Interface.hint list * Interface.hint) option atask
+val inloadpath : string -> bool atask
+val mkcases : string -> string list list atask
+val search : Interface.search_flags -> string Interface.coq_object list atask
-(** A specialized version of [raw_interp] dedicated to
- set/unset options. *)
+(** A specialized version of [raw_interp] dedicated to set/unset options. *)
module PrintOpt :
sig
@@ -116,5 +138,5 @@ sig
val universes : t
val set_printing_width : int -> unit
- val set : handle -> (t * bool) list -> unit
+ val set : (t * bool) list -> task
end
View
860 ide/coqide.ml
@@ -60,30 +60,29 @@ let logfile = ref None
class type _analyzed_view =
object
-
method filename : string option
method update_stats : unit
method changed_on_disk : bool
method revert : unit
method auto_save : unit
method save : string -> bool
method save_as : string -> bool
- method go_to_insert : Coq.handle -> unit
- method find_next_occurrence : direction -> unit
- method tactic_wizard : Coq.handle -> string list -> unit
- method insert_message : string -> unit
- method process_next_phrase : Coq.handle -> bool -> unit
- method process_until_end_or_error : Coq.handle -> unit
method recenter_insert : unit
- method erroneous_reset_initial : Coq.handle -> unit
- method requested_reset_initial : Coq.handle -> unit
+ method insert_message : string -> unit
method set_message : string -> unit
- method raw_coq_query : Coq.handle -> string -> unit
- method show_goals : Coq.handle -> unit
- method backtrack_last_phrase : Coq.handle -> unit
+ method find_next_occurrence : direction -> unit
method help_for_keyword : unit -> unit
-end
+ method go_to_insert : Coq.task
+ method tactic_wizard : string list -> Coq.task
+ method process_next_phrase : Coq.task
+ method process_until_end_or_error : Coq.task
+ method handle_reset_initial : Coq.reset_kind -> Coq.task
+ method raw_coq_query : string -> Coq.task
+ method show_goals : Coq.task
+ method backtrack_last_phrase : Coq.task
+ method include_file_dir_in_path : Coq.task
+end
type viewable_script = {
script : Wg_ScriptView.script_view;
@@ -182,25 +181,12 @@ exception Unsuccessful
let force_reset_initial () =
Minilib.log "Reset Initial";
- let term = session_notebook#current_term in
- Coq.reset_coqtop term.toplvl term.analyzed_view#requested_reset_initial
+ Coq.reset_coqtop session_notebook#current_term.toplvl
let break () =
Minilib.log "User break received";
Coq.break_coqtop session_notebook#current_term.toplvl
-let do_if_not_computing term text f =
- let threaded_task () =
- let info () = Minilib.log ("Discarded query:" ^ text) in
- try Coq.try_grab term.toplvl f info
- with
- | e ->
- let msg = "Unknown error, please report:\n" ^ (Printexc.to_string e) in
- term.analyzed_view#set_message msg
- in
- Minilib.log ("Launching thread " ^ text);
- ignore (Thread.create threaded_task ())
-
let warn_image =
let img = GMisc.image () in
img#set_stock `DIALOG_WARNING;
@@ -409,7 +395,7 @@ object(self)
let do_revert f =
push_info "Reverting buffer";
try
- Coq.reset_coqtop mycoqtop self#requested_reset_initial;
+ Coq.reset_coqtop mycoqtop;
let b = Buffer.create 1024 in
Ideutils.read_file f b;
let s = try_convert (Buffer.contents b) in
@@ -520,16 +506,11 @@ object(self)
input_buffer#get_iter_at_mark `INSERT
method recenter_insert =
- (* BUG : to investigate further:
- FIXED : Never call GMain.* in thread !
- PLUS : GTK BUG ??? Cannot be called from a thread...
- ADDITION: using sync instead of async causes deadlock...*)
- ignore (GtkThread.async (
- input_view#scroll_to_mark
- ~use_align:false
- ~yalign:0.75
- ~within_margin:0.25)
- `INSERT)
+ input_view#scroll_to_mark
+ ~use_align:false ~yalign:0.75 ~within_margin:0.25 `INSERT
+
+ method help_for_keyword () =
+ browse_keyword (self#insert_message) (get_current_word ())
(* go to the next occurrence of the current word, forward or backward *)
method find_next_occurrence dir =
@@ -546,32 +527,34 @@ object(self)
(b#place_cursor start;
self#recenter_insert)
- method show_goals handle =
+ method show_goals h k =
Coq.PrintOpt.set_printing_width proof_view#width;
- match Coq.goals handle with
- | Interface.Fail (l, str) ->
- self#set_message ("Error in coqtop:\n"^str)
- | Interface.Good goals | Interface.Unsafe goals ->
- begin match Coq.evars handle with
- | Interface.Fail (l, str)->
- self#set_message ("Error in coqtop:\n"^str)
- | Interface.Good evs | Interface.Unsafe evs ->
- proof_view#set_goals goals;
- proof_view#set_evars evs;
- proof_view#refresh ()
- end
+ Coq.goals h (function
+ |Interface.Fail (l, str) ->
+ (self#set_message ("Error in coqtop:\n"^str); k())
+ |Interface.Good goals | Interface.Unsafe goals ->
+ Coq.evars h (function
+ |Interface.Fail (l, str)->
+ (self#set_message ("Error in coqtop:\n"^str); k())
+ |Interface.Good evs | Interface.Unsafe evs ->
+ proof_view#set_goals goals;
+ proof_view#set_evars evs;
+ proof_view#refresh ();
+ k()))
(* This method is intended to perform stateless commands *)
- method raw_coq_query handle phrase =
+ method raw_coq_query phrase h k =
let () = Minilib.log "raw_coq_query starting now" in
let display_error s =
if not (Glib.Utf8.validate s) then
flash_info "This error is so nasty that I can't even display it."
else self#insert_message s;
in
- match Coq.interp handle self#push_message ~raw:true ~verbose:false phrase with
- | Interface.Fail (_, err) -> sync display_error err
- | Interface.Good msg | Interface.Unsafe msg -> sync self#insert_message msg
+ Coq.interp ~logger:self#push_message ~raw:true ~verbose:false phrase h
+ (function
+ | Interface.Fail (_, err) -> display_error err; k ()
+ | Interface.Good msg | Interface.Unsafe msg ->
+ self#insert_message msg; k ())
method private find_phrase_starting_at (start:GText.iter) =
try
@@ -608,77 +591,54 @@ object(self)
in
try loop 0 self#get_start_of_input with Exit -> ()
- method private process_command_queue ?(verbose = false) queue handle =
- let error = ref None in
- let info = ref [] in
- let current_flags = ref [] in
- let push_info level message = info := (level, message) :: !info in
- (* First, process until error *)
- Minilib.log "Begin command processing";
- while not (Queue.is_empty queue) && !error = None do
- let sentence = Queue.peek queue in
- (* If the line is not a comment, we interpret it. *)
- if not (List.mem `COMMENT sentence.flags) then begin
- let start = input_buffer#get_iter_at_mark sentence.start in
- let stop = input_buffer#get_iter_at_mark sentence.stop in
- let phrase = start#get_slice ~stop in
- match Coq.interp handle push_info ~verbose phrase with
- | Interface.Fail (loc, msg) ->
- error := Some (phrase, loc, msg);
- | Interface.Good msg ->
- push_info Interface.Notice msg;
- current_flags := []
- | Interface.Unsafe msg ->
- current_flags := [`UNSAFE]
- end;
- (* If there is no error, then we mark it done *)
- if !error = None then begin
- (* We reget the iters here because Gtk is unable to warranty that they
- were not modified meanwhile. Not really necessary but who knows... *)
- let start = input_buffer#get_iter_at_mark sentence.start in
- let stop = input_buffer#get_iter_at_mark sentence.stop in
- let sentence = { sentence with
- flags = !current_flags @ sentence.flags
- } in
- let tag =
- if List.mem `UNSAFE !current_flags then Tags.Script.unjustified
- else Tags.Script.processed
- in
- input_buffer#move_mark ~where:stop (`NAME "start_of_input");
- input_buffer#apply_tag tag ~start ~stop;
- input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
- (* Discard the old stack info and put it were it belongs *)
- ignore (Queue.pop queue);
- Stack.push sentence cmd_stack;
- end;
- done;
- (* Then clear all irrelevant commands *)
+ method private discard_command_queue queue =
while not (Queue.is_empty queue) do
let sentence = Queue.pop queue in
let start = input_buffer#get_iter_at_mark sentence.start in
let stop = input_buffer#get_iter_at_mark sentence.stop in
input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
input_buffer#delete_mark sentence.start;
input_buffer#delete_mark sentence.stop;
- done;
- (* Return the list of info messages and the error *)
- (List.rev !info, !error)
+ done
- method private show_error phrase loc msg = match loc with
- | None ->
- message_view#clear ();
- message_view#push Interface.Error msg
- | Some (start, stop) ->
- let soi = self#get_start_of_input in
- let start = soi#forward_chars (byte_offset_to_char_offset phrase start) in
- let stop = soi#forward_chars (byte_offset_to_char_offset phrase stop) in
- input_buffer#apply_tag Tags.Script.error ~start ~stop;
- input_buffer#place_cursor ~where:start;
+ method private commit_queue_transaction queue sentence newflags =
+ (* A queued command has been successfully done, we push it to [cmd_stack].
+ We reget the iters here because Gtk is unable to warranty that they
+ were not modified meanwhile. Not really necessary but who knows... *)
+ let start = input_buffer#get_iter_at_mark sentence.start in
+ let stop = input_buffer#get_iter_at_mark sentence.stop in
+ let sentence = { sentence with flags = newflags @ sentence.flags } in
+ let tag =
+ if List.mem `UNSAFE newflags then Tags.Script.unjustified
+ else Tags.Script.processed
+ in
+ input_buffer#move_mark ~where:stop (`NAME "start_of_input");
+ input_buffer#apply_tag tag ~start ~stop;
+ input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
+ ignore (Queue.pop queue);
+ Stack.push sentence cmd_stack
+
+ method private process_error queue phrase loc msg h k =
+ let position_error = function
+ | None -> ()
+ | Some (start, stop) ->
+ let soi = self#get_start_of_input in
+ let start =
+ soi#forward_chars (byte_offset_to_char_offset phrase start) in
+ let stop =
+ soi#forward_chars (byte_offset_to_char_offset phrase stop) in
+ input_buffer#apply_tag Tags.Script.error ~start ~stop;
+ input_buffer#place_cursor ~where:start
+ in
+ self#discard_command_queue queue;
+ pop_info ();
+ position_error loc;
message_view#clear ();
- message_view#push Interface.Error msg
+ message_view#push Interface.Error msg;
+ self#show_goals h k
(** Compute the phrases until [until] returns [true]. *)
- method private process_until until finish handle verbose =
+ method private process_until until verbose h k =
let queue = Queue.create () in
(* Lock everything and fill the waiting queue *)
push_info "Coq is computing";
@@ -687,37 +647,54 @@ object(self)
self#fill_command_queue until queue;
(* Now unlock and process asynchronously *)
input_view#set_editable true;
- let (msg, error) = self#process_command_queue ~verbose queue handle in
- pop_info ();
- (* Display the goal and any error *)
- self#show_goals handle;
- match error with
- | None ->
- if verbose then
- List.iter (fun (lvl, msg) -> self#push_message lvl msg) msg;
- finish ();
- self#recenter_insert
- | Some (phrase, loc, msg) ->
- self#show_error phrase loc msg
-
- method process_next_phrase handle verbose =
+ let push_info lvl msg = if verbose then self#push_message lvl msg
+ in
+ Minilib.log "Begin command processing";
+ let rec loop () =
+ if Queue.is_empty queue then
+ let () = pop_info () in
+ let () = self#recenter_insert in
+ self#show_goals h k
+ else
+ let sentence = Queue.peek queue in
+ if List.mem `COMMENT sentence.flags then
+ (self#commit_queue_transaction queue sentence []; loop ())
+ else
+ (* If the line is not a comment, we interpret it. *)
+ let start = input_buffer#get_iter_at_mark sentence.start in
+ let stop = input_buffer#get_iter_at_mark sentence.stop in
+ let phrase = start#get_slice ~stop in
+ let commit_and_continue msg flags =
+ push_info Interface.Notice msg;
+ self#commit_queue_transaction queue sentence flags;
+ loop ()
+ in
+ Coq.interp ~logger:push_info ~verbose phrase h
+ (function
+ |Interface.Good msg -> commit_and_continue msg []
+ |Interface.Unsafe msg -> commit_and_continue msg [`UNSAFE]
+ |Interface.Fail (loc, msg) ->
+ self#process_error queue phrase loc msg h k)
+ in
+ loop ()
+
+ method process_next_phrase h k =
let until len start stop = 1 <= len in
- let finish () = input_buffer#place_cursor self#get_start_of_input in
- self#process_until until finish handle verbose
+ self#process_until until true h
+ (fun () -> input_buffer#place_cursor ~where:self#get_start_of_input; k())
- method private process_until_iter handle iter =
+ method private process_until_iter iter h k =
let until len start stop =
if prefs.stop_before then stop#compare iter > 0
else start#compare iter >= 0
in
- let finish () = () in
- self#process_until until finish handle false
+ self#process_until until false h k
- method process_until_end_or_error handle =
- self#process_until_iter handle input_buffer#end_iter
+ method process_until_end_or_error h k =
+ self#process_until_iter input_buffer#end_iter h k
- (** Clear the command stack until [until] returns [true]. Returns the number
- of commands sent to Coqtop to backtrack. *)
+ (** Clear the command stack until [until] returns [true].
+ Returns the number of commands sent to Coqtop to backtrack. *)
method private clear_command_stack until =
let rec loop len real_len =
if Stack.is_empty cmd_stack then real_len
@@ -741,73 +718,57 @@ object(self)
loop 0 0
(** Actually performs the undoing *)
- method private undo_command_stack handle n =
- match Coq.rewind handle n with
- | Interface.Good n | Interface.Unsafe n ->
- let until _ len _ _ = n <= len in
- (* Coqtop requested [n] more ACTUAL backtrack *)
- ignore (self#clear_command_stack until)
- | Interface.Fail (l, str) ->
- self#set_message
- ("Error while backtracking: " ^ str ^
- "\nCoqIDE and coqtop may be out of sync, you may want to use Restart.")
+ method private undo_command_stack n h k =
+ Coq.rewind n h (function
+ |Interface.Good n | Interface.Unsafe n ->
+ let until _ len _ _ = n <= len in
+ (* Coqtop requested [n] more ACTUAL backtrack *)
+ ignore (self#clear_command_stack until);
+ k ()
+ |Interface.Fail (l, str) ->
+ self#set_message
+ ("Error while backtracking: " ^ str ^
+ "\nCoqIDE and coqtop may be out of sync," ^
+ "you may want to use Restart.");
+ k ())
(** Wrapper around the raw undo command *)
- method private backtrack_until until finish handle =
+ method private backtrack_until until h k =
push_info "Coq is undoing";
message_view#clear ();
(* Lock everything *)
input_view#set_editable false;
let to_undo = self#clear_command_stack until in
- self#undo_command_stack handle to_undo;
- input_view#set_editable true;
- pop_info ();
- finish ()
+ self#undo_command_stack to_undo h
+ (fun () -> input_view#set_editable true; pop_info (); k ())
- method private backtrack_to_iter handle iter =
+ method private backtrack_to_iter iter h k =
let until _ _ _ stop = iter#compare stop >= 0 in
- let finish () = () in
- self#backtrack_until until finish handle;
- (* We may have backtracked too much: let's replay *)
- self#process_until_iter handle iter
+ self#backtrack_until until h
+ (* We may have backtracked too much: let's replay *)
+ (fun () -> self#process_until_iter iter h k)
- method backtrack_last_phrase handle =
+ method backtrack_last_phrase h k =
let until len _ _ _ = 1 <= len in
- let finish () = input_buffer#place_cursor self#get_start_of_input in
- self#backtrack_until until finish handle;
- self#show_goals handle
+ self#backtrack_until until h
+ (fun () ->
+ input_buffer#place_cursor ~where:self#get_start_of_input;
+ self#show_goals h k)
- method go_to_insert handle =
+ method go_to_insert h k =
let point = self#get_insert in
if point#compare self#get_start_of_input >= 0
- then self#process_until_iter handle point
- else self#backtrack_to_iter handle point
+ then self#process_until_iter point h k
+ else self#backtrack_to_iter point h k
- method private send_to_coq handle phrase =
- let display_error (loc, s) =
- if not (Glib.Utf8.validate s) then
- flash_info "This error is so nasty that I can't even display it."
- else self#insert_message s
- in
- Minilib.log "Send_to_coq starting now";
- match Coq.interp handle default_logger ~verbose:false phrase with
- | Interface.Fail (l, str) -> sync display_error (l, str); None
- | Interface.Good msg -> sync self#insert_message msg; Some []
- | Interface.Unsafe msg -> sync self#insert_message msg; Some [`UNSAFE]
-
- method private insert_this_phrase_on_success handle coqphrase insertphrase =
- let mark_processed flags =
+ method tactic_wizard l h k =
+ let insert_phrase phrase tag =
let stop = self#get_start_of_input in
- if stop#starts_line then
- input_buffer#insert ~iter:stop insertphrase
- else input_buffer#insert ~iter:stop ("\n"^insertphrase);
+ let phrase' = if stop#starts_line then phrase else "\n"^phrase in
+ input_buffer#insert ~iter:stop phrase';
tag_on_insert (input_buffer :> GText.buffer);
let start = self#get_start_of_input in
input_buffer#move_mark ~where:stop (`NAME "start_of_input");
- let tag =
- if List.mem `UNSAFE flags then Tags.Script.unjustified
- else Tags.Script.processed
- in
input_buffer#apply_tag tag ~start ~stop;
if self#get_insert#compare stop <= 0 then
input_buffer#place_cursor ~where:stop;
@@ -817,69 +778,78 @@ object(self)
flags = [];
} in
Stack.push ide_payload cmd_stack;
- self#show_goals handle;
+ message_view#clear ();
+ self#show_goals h k;
in
- match self#send_to_coq handle coqphrase with
- | Some flags -> sync mark_processed flags; true
- | None ->
- sync (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase)) ();
- false
+ let display_error (loc, s) =
+ if not (Glib.Utf8.validate s) then
+ flash_info "This error is so nasty that I can't even display it."
+ else self#insert_message s
+ in
+ let try_phrase phrase stop more =
+ Minilib.log "Sending to coq now";
+ Coq.interp ~verbose:false phrase h
+ (function
+ |Interface.Fail (l, str) ->
+ display_error (l, str);
+ self#insert_message ("Unsuccessfully tried: "^phrase);
+ more ()
+ |Interface.Good msg ->
+ self#insert_message msg;
+ stop Tags.Script.processed
+ |Interface.Unsafe msg ->
+ self#insert_message msg;
+ stop Tags.Script.unjustified)
+ in
+ let rec loop l () = match l with
+ | [] -> k ()
+ | p :: l' ->
+ try_phrase ("progress "^p^".") (insert_phrase (p^".")) (loop l')
+ in
+ loop l ()
- method private generic_reset_initial handle =
- let start = input_buffer#start_iter in
+ method handle_reset_initial why h k =
+ if why = Coq.Unexpected then warning "Coqtop died badly. Resetting.";
(* clear the stack *)
while not (Stack.is_empty cmd_stack) do
let phrase = Stack.pop cmd_stack in
input_buffer#delete_mark phrase.start;
input_buffer#delete_mark phrase.stop
done;
(* reset the buffer *)
+ let start = input_buffer#start_iter in
+ let stop = input_buffer#end_iter in
input_buffer#move_mark ~where:start (`NAME "start_of_input");
- input_buffer#remove_tag Tags.Script.processed start input_buffer#end_iter;
- input_buffer#remove_tag Tags.Script.unjustified start input_buffer#end_iter;
- input_buffer#remove_tag Tags.Script.to_process start input_buffer#end_iter;
+ input_buffer#remove_tag Tags.Script.processed ~start ~stop;
+ input_buffer#remove_tag Tags.Script.unjustified ~start ~stop;
+ input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
tag_on_insert (input_buffer :> GText.buffer);
(* clear the views *)
message_view#clear ();
proof_view#clear ();
+ clear_info ();
+ push_info "Restarted";
(* apply the initial commands to coq *)
- self#include_file_dir_in_path handle;
-
- method erroneous_reset_initial handle =
- self#generic_reset_initial handle;
- (* warn the user *)
- warning "Coqtop died badly. Resetting."
-
- method requested_reset_initial handle =
- self#generic_reset_initial handle
-
- method tactic_wizard handle l =
- async message_view#clear ();
- ignore
- (List.exists
- (fun p ->
- self#insert_this_phrase_on_success handle
- ("progress "^p^".") (p^".")) l)
+ self#include_file_dir_in_path h k;
- method private include_file_dir_in_path handle =
+ method include_file_dir_in_path h k =
match filename with
- | None -> ()
- | Some f ->
- let dir = Filename.dirname f in
- match Coq.inloadpath handle dir with
- | Interface.Fail (_,s) ->
- self#set_message
- ("Could not determine lodpath, this might lead to problems:\n"^s)
- | Interface.Good true | Interface.Unsafe true -> ()
- | Interface.Good false | Interface.Unsafe false ->
- let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in
- match Coq.interp handle default_logger cmd with
- | Interface.Fail (l,str) ->
- self#set_message ("Couln't add loadpath:\n"^str)
- | Interface.Good _ | Interface.Unsafe _ -> ()
-
- method help_for_keyword () =
- browse_keyword (self#insert_message) (get_current_word ())
+ |None -> k ()
+ |Some f ->
+ let dir = Filename.dirname f in
+ Coq.inloadpath dir h (function
+ |Interface.Fail (_,s) ->
+ self#set_message
+ ("Could not determine lodpath, this might lead to problems:\n"^s);
+ k ()
+ |Interface.Good true |Interface.Unsafe true -> k ()
+ |Interface.Good false |Interface.Unsafe false ->
+ let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in
+ Coq.interp cmd h (function
+ |Interface.Fail (l,str) ->
+ self#set_message ("Couln't add loadpath:\n"^str);
+ k ()
+ |Interface.Good _ | Interface.Unsafe _ -> k ()))
(** NB: Events during text edition:
@@ -950,17 +920,25 @@ object(self)
| Some "insert" -> ()
| Some s -> Minilib.log (s^" moved")
| None -> ())
- in
- Coq.grab mycoqtop self#include_file_dir_in_path;
+ in ()
end
-let last_make = ref "";;
-let last_make_index = ref 0;;
+(** [last_make_buf] contains the output of the last make compilation.
+ [last_make] is the same, but as a string, refreshed only when searching
+ the next error.
+*)
+
+let last_make_buf = Buffer.create 1024
+let last_make = ref ""
+let last_make_index = ref 0
+let last_make_dir = ref ""
let search_compile_error_regexp =
Str.regexp
- "File \"\\([^\"]+\\)\", line \\([0-9]+\\), characters \\([0-9]+\\)-\\([0-9]+\\)";;
+ "File \"\\([^\"]+\\)\", line \\([0-9]+\\), characters \\([0-9]+\\)-\\([0-9]+\\)"
let search_next_error () =
+ if String.length !last_make <> Buffer.length last_make_buf
+ then last_make := Buffer.contents last_make_buf;
let _ =
Str.search_forward search_compile_error_regexp !last_make !last_make_index
in
@@ -971,80 +949,77 @@ let search_next_error () =
and msg_index = Str.match_beginning ()
in
last_make_index := Str.group_end 4;
- (f,l,b,e,
+ (Filename.concat !last_make_dir f, l, b, e,
String.sub !last_make msg_index (String.length !last_make - msg_index))
-
(**********************************************************************)
(* session creation and primitive handling *)
(**********************************************************************)
let create_session file =
- let script_buffer =
- GSourceView2.source_buffer
- ~tag_table:Tags.Script.table
- ~highlight_matching_brackets:true
- ?language:(lang_manager#language prefs.source_language)
- ?style_scheme:(style_manager#style_scheme prefs.source_style)
- ()
- in
- let proof = Wg_ProofView.proof_view () in
- let message = Wg_MessageView.message_view () in
let basename = match file with
- |None -> "*scratch*"
- |Some f -> Glib.Convert.filename_to_utf8 (Filename.basename f)
- in
- let get_args f =
- Project_file.args_from_project f
- !custom_project_files prefs.project_file_name
+ |None -> "*scratch*"
+ |Some f -> Glib.Convert.filename_to_utf8 (Filename.basename f)
in
let coqtop_args = match file with
|None -> !sup_args
- |Some the_file -> match prefs.read_project with
+ |Some the_file ->
+ let get_args f = Project_file.args_from_project f
+ !custom_project_files prefs.project_file_name
+ in
+ match prefs.read_project with
|Ignore_args -> !sup_args
|Append_args -> get_args the_file @ !sup_args
|Subst_args -> get_args the_file
in
- let reset = ref (fun _ -> ()) in
- let trigger handle = !reset handle in
- let ct = Coq.spawn_coqtop trigger coqtop_args in
- let script =
- Wg_ScriptView.script_view ct
- ~source_buffer:script_buffer
- ~show_line_numbers:true
- ~wrap_mode:`NONE () in
- let command = new Wg_Command.command_window ct in
- let finder = new Wg_Find.finder (script :> GText.view) in
- let legacy_av = new analyzed_view script proof message ct file in
- let () = reset := legacy_av#erroneous_reset_initial in
- let () = legacy_av#update_stats in
- let _ =
- script#buffer#create_mark ~name:"start_of_input" script#buffer#start_iter
+ let coqtop = Coq.spawn_coqtop coqtop_args
in
- let _ =
- script#buffer#create_mark ~name:"prev_insert" script#buffer#start_iter in
+ let buffer = GSourceView2.source_buffer
+ ~tag_table:Tags.Script.table
+ ~highlight_matching_brackets:true
+ ?language:(lang_manager#language prefs.source_language)
+ ?style_scheme:(style_manager#style_scheme prefs.source_style)
+ ()
+ in
+ let _ = buffer#create_mark ~name:"start_of_input" buffer#start_iter in
+ let _ = buffer#create_mark ~name:"prev_insert" buffer#start_iter in
+ let _ = buffer#place_cursor ~where:buffer#start_iter
+ in
+ let script = Wg_ScriptView.script_view coqtop ~source_buffer:buffer
+ ~show_line_numbers:true ~wrap_mode:`NONE ()
+ in
+ let _ = script#misc#set_name "ScriptWindow"
+ in
+ let proof = Wg_ProofView.proof_view () in
+ let _ = proof#misc#set_can_focus true in
let _ =
GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION]
in
- let () =
- let fold accu (opts, _, _, _, dflt) =
- List.fold_left (fun accu opt -> (opt, dflt) :: accu) accu opts
- in
- let options = List.fold_left fold [] print_items in
- Coq.grab ct (fun handle -> Coq.PrintOpt.set handle options)
+ let message = Wg_MessageView.message_view () in
+ let _ = message#misc#set_can_focus true
+ in
+ let command = new Wg_Command.command_window coqtop in
+ let finder = new Wg_Find.finder (script :> GText.view) in
+ let view = new analyzed_view script proof message coqtop file in
+ let _ = Coq.set_reset_handler coqtop view#handle_reset_initial in
+ let _ = view#update_stats in
+ let _ = Coq.init_coqtop coqtop
+ (fun h k ->
+ view#include_file_dir_in_path h
+ (fun () ->
+ let fold accu (opts, _, _, _, dflt) =
+ List.fold_left (fun accu opt -> (opt, dflt) :: accu) accu opts
+ in
+ let options = List.fold_left fold [] print_items in
+ Coq.PrintOpt.set options h k))
in
- script#misc#set_name "ScriptWindow";
- script#buffer#place_cursor ~where:script#buffer#start_iter;
- proof#misc#set_can_focus true;
- message#misc#set_can_focus true;
-
{ tab_label= GMisc.label ~text:basename ();
script=script;
proof_view=proof;
message_view=message;
- analyzed_view=legacy_av;
- toplvl=ct;
+ analyzed_view=view;
+ toplvl=coqtop;
command=command;
finder=finder;
}
@@ -1065,9 +1040,6 @@ let pr_exit_status = function
| Unix.WEXITED 0 -> " succeeded"
| _ -> " failed"
-let run_command av cmd =
- CUnix.run_command Ideutils.try_convert av#insert_message cmd
-
(** Auxiliary functions for the File operations *)
module FileAux = struct
@@ -1152,37 +1124,12 @@ let check_quit saveall =
| 2 -> ()
| _ -> raise DontQuit
end;
- let wait_w = GWindow.window ~modal:true ~wm_class:"CoqIde" ~wm_name:"CoqIde"
- ~kind:`POPUP ~title:"Terminating coqtops" () in
- let _ =
- GMisc.label ~text:"Terminating coqtops processes, please wait ..."
- ~packing:wait_w#add ()
- in
- let warn_w = GWindow.message_dialog ~message_type:`WARNING
- ~buttons:GWindow.Buttons.yes_no
- ~message:
- ("Some coqtops processes are still running.\n" ^
- "If you quit CoqIDE right now, you may have to kill them manually.\n" ^
- "Do you want to wait for those processes to terminate ?")
- ()
- in
- let () =
- List.iter (fun _ -> session_notebook#remove_page 0) session_notebook#pages
- in
- let nb_try = ref 0 in
- let () = wait_w#show () in
- let () =
- while (Coq.coqtop_zombies () <> 0) && (!nb_try <= 50) do
- incr nb_try;
- Thread.delay 0.1 ;
- done
- in
- if !nb_try = 50 then begin
- wait_w#misc#hide ();
- match warn_w#run () with
- | `YES -> warn_w#misc#hide (); raise DontQuit
- | `NO | `DELETE_EVENT -> ()
- end
+ List.iter (fun p -> Coq.close_coqtop p.toplvl) session_notebook#pages
+
+(* For MacOS, just to be sure, we close all coqtops (again?) *)
+let close_and_quit () =
+ List.iter (fun p -> Coq.close_coqtop p.toplvl) session_notebook#pages;
+ Coq.final_countdown ()
let crash_save exitcode =
Minilib.log "Starting emergency save of buffers in .crashcoqide files";
@@ -1246,7 +1193,8 @@ let revert_all _ =
session_notebook#pages
let quit _ =
- try FileAux.check_quit saveall; exit 0 with FileAux.DontQuit -> ()
+ try FileAux.check_quit saveall; Coq.final_countdown ()
+ with FileAux.DontQuit -> ()
let close_buffer _ =
let do_remove () =
@@ -1282,11 +1230,13 @@ let export kind _ =
| _ -> assert false
in
let cmd =
- local_cd f ^ prefs.cmd_coqdoc ^ " --" ^ kind ^
- " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef)
+ local_cd f ^ prefs.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^
+ (Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1"
in
- let st,_ = run_command av cmd in
- flash_info (cmd ^ pr_exit_status st)
+ av#set_message ("Running: "^cmd);
+ let finally st = flash_info (cmd ^ pr_exit_status st)
+ in
+ run_command av#insert_message finally cmd
let print _ =
let av = current_view () in
@@ -1315,13 +1265,13 @@ let print _ =
let ok = GButton.button ~stock:`PRINT ~label:"Print" ~packing:h#add ()
in
let callback_print () =
+ w#destroy ();
let cmd = e#text in
- let st,_ = run_command av cmd in
- flash_info (cmd ^ pr_exit_status st);
- w#destroy ()
+ let finally st = flash_info (cmd ^ pr_exit_status st) in
+ run_command ignore finally cmd
in
- ignore (ko#connect#clicked ~callback:w#destroy);
- ignore (ok#connect#clicked ~callback:callback_print);
+ let _ = ko#connect#clicked ~callback:w#destroy in
+ let _ = ok#connect#clicked ~callback:callback_print in
w#misc#show ()
let highlight _ =
@@ -1349,10 +1299,11 @@ let reset_autosave_timer () =
(** Export of functions used in [coqide_main] : *)
-let forbid_quit_to_save () =
+let forbid_quit () =
try FileAux.check_quit File.saveall; false
with FileAux.DontQuit -> true
+let close_and_quit = FileAux.close_and_quit
let crash_save = FileAux.crash_save
let do_load f = FileAux.load_file f
@@ -1367,33 +1318,45 @@ let compile _ =
match av#filename with
|None -> flash_info "Active buffer has no name"
|Some f ->
- let cmd = prefs.cmd_coqc ^ " -I "
- ^ (Filename.quote (Filename.dirname f))
- ^ " " ^ (Filename.quote f) in
- let st,res = run_command av cmd in
- if st = Unix.WEXITED 0 then
- flash_info (f ^ " successfully compiled")
- else begin
- flash_info (f ^ " failed to compile");
- Coq.try_grab v.toplvl av#process_until_end_or_error ignore;
- av#insert_message "Compilation output:\n";
- av#insert_message res
- end
+ let cmd = prefs.cmd_coqc ^ " -I " ^ (Filename.quote (Filename.dirname f))
+ ^ " " ^ (Filename.quote f) ^ " 2>&1"
+ in
+ let buf = Buffer.create 1024 in
+ av#set_message ("Running: "^cmd);
+ let display s =
+ av#insert_message s;
+ Buffer.add_string buf s
+ in
+ let finally st =
+ if st = Unix.WEXITED 0 then
+ flash_info (f ^ " successfully compiled")
+ else begin
+ flash_info (f ^ " failed to compile");
+ av#set_message "Compilation output:\n";
+ av#insert_message (Buffer.contents buf);
+ end
+ in
+ run_command display finally cmd
let make _ =
let av = current_view () in
match av#filename with
|None -> flash_info "Cannot make: this buffer has no name"
|Some f ->
- let cmd = local_cd f ^ prefs.cmd_make in
- (*
- save_f ();
- *)
- av#insert_message "Command output:\n";
- let st,res = run_command av cmd in
- last_make := res;
+ File.saveall ();
+ let cmd = local_cd f ^ prefs.cmd_make ^ " 2>&1" in
+ av#set_message "Compilation output:\n";
+ Buffer.reset last_make_buf;
+ last_make := "";
last_make_index := 0;
- flash_info (prefs.cmd_make ^ pr_exit_status st)
+ last_make_dir := Filename.dirname f;
+ let display s =
+ av#insert_message s;
+ Buffer.add_string last_make_buf s
+ in
+ let finally st = flash_info (current.cmd_make ^ pr_exit_status st)
+ in
+ run_command display finally cmd
let next_error _ =
try
@@ -1410,18 +1373,17 @@ let next_error _ =
v.script#misc#grab_focus ()
with Not_found ->
last_make_index := 0;
- let v = session_notebook#current_term in
- let av = v.analyzed_view in
- av#set_message "No more errors.\n"
+ (current_view ())#set_message "No more errors.\n"
let coq_makefile _ =
let av = current_view () in
match av#filename with
|None -> flash_info "Cannot make makefile: this buffer has no name"
|Some f ->
let cmd = local_cd f ^ prefs.cmd_coqmakefile in
- let st,res = run_command av cmd in
- flash_info (prefs.cmd_coqmakefile ^ pr_exit_status st)
+ let finally st = flash_info (current.cmd_coqmakefile ^ pr_exit_status st)
+ in
+ run_command ignore finally cmd
let editor _ =
let av = current_view () in
@@ -1431,61 +1393,55 @@ let editor _ =
File.save ();
let f = Filename.quote f in
let cmd = Util.subst_command_placeholder prefs.cmd_editor f in
- let _ = run_command av cmd in
- av#revert
+ run_command ignore (fun _ -> av#revert) cmd
end
(** Callbacks for the Navigation menu *)
-let do_or_activate f =
- let p = session_notebook#current_term in
- do_if_not_computing p "do_or_activate"
- (fun handle ->
- let av = p.analyzed_view in
- f handle av;
- pop_info ();
- let msg = match Coq.status handle with
- | Interface.Fail (l, str) ->
- "Oops, problem while fetching coq status."
- | Interface.Good status | Interface.Unsafe status ->
- let path = match status.Interface.status_path with
- | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
- | _ :: l -> " in " ^ String.concat "." l
- in
- let name = match status.Interface.status_proofname with
- | None -> ""
- | Some n -> ", proving " ^ n
- in
- "Ready" ^ path ^ name
+let update_status h k =
+ let display msg = pop_info (); push_info msg
+ in
+ Coq.status h (function
+ |Interface.Fail (l, str) ->
+ display "Oops, problem while fetching coq status."; k ()
+ |Interface.Good status | Interface.Unsafe status ->
+ let path = match status.Interface.status_path with
+ | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
+ | _ :: l -> " in " ^ String.concat "." l
+ in
+ let name = match status.Interface.status_proofname with
+ | None -> ""
+ | Some n -> ", proving " ^ n
in
- push_info msg)
+ display ("Ready" ^ path ^ name); k ())
-let do_if_active f =
- let p = session_notebook#current_term in
- do_if_not_computing p "do_if_active"
- (fun handle -> ignore (f handle p.analyzed_view))
+let send_to_coq f =
+ let term = session_notebook#current_term in
+ let av = term.analyzed_view in
+ let info () = Minilib.log ("Coq busy, discarding query") in
+ let f h k = f av h (fun () -> update_status h k) in
+ Coq.try_grab term.toplvl f info
module Nav = struct
- let forward_one _ = do_or_activate (fun h a -> a#process_next_phrase h true)
- let backward_one _ = do_or_activate (fun h a -> a#backtrack_last_phrase h)
- let goto _ = do_or_activate (fun h a -> a#go_to_insert h)
+ let forward_one _ = send_to_coq (fun a -> a#process_next_phrase)
+ let backward_one _ = send_to_coq (fun a -> a#backtrack_last_phrase)
+ let goto _ = send_to_coq (fun a -> a#go_to_insert)
let restart _ = force_reset_initial ()
- let goto_end _ = do_or_activate (fun h a -> a#process_until_end_or_error h)
+ let goto_end _ = send_to_coq (fun a -> a#process_until_end_or_error)
let interrupt _ = break ()
let previous_occ _ = (current_view ())#find_next_occurrence Up
let next_occ _ = (current_view ())#find_next_occurrence Down
end
-let tactic_wizard_callback l _ =
- do_if_active (fun h a -> a#tactic_wizard h l)
+let tactic_wizard_callback l _ = send_to_coq (fun a -> a#tactic_wizard l)
let printopts_callback opts v =
let b = v#get_active in
let opts = List.map (fun o -> (o,b)) opts in
- do_or_activate (fun h av ->
- Coq.PrintOpt.set h opts;
- av#show_goals h)
+ send_to_coq (fun av h k ->
+ Coq.PrintOpt.set opts h
+ (fun () -> av#show_goals h k))
(** Templates menu *)
@@ -1497,31 +1453,31 @@ let print_branches c cases =
Format.fprintf c "@[match var with@\n%aend@]@."
(print_list print_branch) cases
+let display_match k = function
+ |Interface.Fail _ -> flash_info "Not an inductive type"; k ()
+ |Interface.Good cases |Interface.Unsafe cases ->
+ let text =
+ let buf = Buffer.create 1024 in
+ let () = print_branches (Format.formatter_of_buffer buf) cases in
+ Buffer.contents buf
+ in
+ Minilib.log ("match template :\n" ^ text);
+ let b = current_buffer () in
+ let _ = b#delete_selection () in
+ let m = b#create_mark (b#get_iter_at_mark `INSERT) in
+ if b#insert_interactive text then begin
+ let i = b#get_iter (`MARK m) in
+ let _ = i#nocopy#forward_chars 9 in
+ let _ = b#place_cursor ~where:i in
+ b#move_mark ~where:(i#backward_chars 3) `SEL_BOUND
+ end;
+ b#delete_mark (`MARK m);
+ k ()
+
let match_callback _ =
let w = get_current_word () in
let coqtop = session_notebook#current_term.toplvl in
- try
- Coq.try_grab coqtop begin fun handle -> match Coq.mkcases handle w with
- | Interface.Fail _ -> raise Not_found
- | Interface.Good cases | Interface.Unsafe cases ->
- let text =
- let buf = Buffer.create 1024 in
- let () = print_branches (Format.formatter_of_buffer buf) cases in
- Buffer.contents buf
- in
- Minilib.log ("match template :\n" ^ text);
- let b = current_buffer () in
- let _ = b#delete_selection () in
- let m = b#create_mark (b#get_iter `INSERT) in
- if b#insert_interactive text then begin
- let i = b#get_iter (`MARK m) in
- let _ = i#nocopy#forward_chars 9 in
- let _ = b#place_cursor ~where:i in
- b#move_mark ~where:(i#backward_chars 3) `SEL_BOUND
- end;
- b#delete_mark (`MARK m)
- end ignore
- with Not_found -> flash_info "Not an inductive type"
+ Coq.try_grab coqtop (fun h k -> Coq.mkcases w h (display_match k)) ignore
(** Queries *)
@@ -1530,33 +1486,33 @@ module Query = struct
let searchabout () =
let word = get_current_word () in
let term = session_notebook#current_term in
- let query handle =
- let results = Coq.search handle [Interface.SubType_Pattern word, true] in
- let results = match results with | Interface.Good l -> l | _ -> [] in
- let buf = term.message_view#buffer in
- let insert result =
- let qualid = result.Interface.coq_object_qualid in
- let name = String.concat "." qualid in
- let tpe = result.Interface.coq_object_object in
- buf#insert ~tags:[Tags.Message.item] name;
- buf#insert "\n";
- buf#insert tpe;
- buf#insert "\n";
- in
+ let buf = term.message_view#buffer in
+ let insert result =
+ let qualid = result.Interface.coq_object_qualid in
+ let name = String.concat "." qualid in
+ let tpe = result.Interface.coq_object_object in
+ buf#insert ~tags:[Tags.Message.item] name;
+ buf#insert "\n";
+ buf#insert tpe;
+ buf#insert "\n";
+ in
+ let display_results k r =
term.message_view#clear ();
- List.iter insert results
+ List.iter insert (match r with Interface.Good l -> l | _ -> []);
+ k ()
in
- Coq.try_grab term.toplvl query ignore
+ let launch_query h k =
+ Coq.search [Interface.SubType_Pattern word, true] h (display_results k)
+ in
+ Coq.try_grab term.toplvl launch_query ignore
let otherquery command _ =
let word = get_current_word () in
let term = session_notebook#current_term in
- let f query handle = term.analyzed_view#raw_coq_query handle query in
- if not (word = "") then
+ if word <> "" then
let query = command ^ " " ^ word ^ "." in
term.message_view#clear ();
- try Coq.try_grab term.toplvl (f query) ignore
- with e -> term.message_view#push Interface.Error (Printexc.to_string e)
+ Coq.try_grab term.toplvl (term.analyzed_view#raw_coq_query query) ignore
let query command _ =
if command = "SearchAbout"
@@ -1831,13 +1787,9 @@ let build_ui () =
menu edit_menu [
item "Edit" ~label:"_Edit";
item "Undo" ~accel:"<Ctrl>u" ~stock:`UNDO
- ~callback:(fun _ ->
- let term = session_notebook#current_term in
- do_if_not_computing term "undo"
- (fun handle ->
- ignore (term.script#undo ())));
+ ~callback:(fun _ -> session_notebook#current_term.script#undo ());
item "Redo" ~stock:`REDO
- ~callback:(fun _ -> ignore (session_notebook#current_term.script#redo ()));
+ ~callback:(fun _ -> session_notebook#current_term.script#redo ());
item "Cut" ~stock:`CUT
~callback:(fun _ -> emit_to_focus GtkText.View.S.cut_clipboard);
item "Copy" ~stock:`COPY
@@ -2048,8 +2000,8 @@ let build_ui () =
let () = vbox#pack toolbar in
(* Reset on tab switch *)
- let _ = session_notebook#connect#switch_page
- (fun _ -> if prefs.reset_on_tab_switch then force_reset_initial ())
+ let _ = session_notebook#connect#switch_page ~callback:(fun _ ->
+ if prefs.reset_on_tab_switch then force_reset_initial ())
in
(* Vertical Separator between Scripts and Goals *)
@@ -2129,23 +2081,21 @@ let main files =
session_notebook#current_term.script#misc#grab_focus ();
Minilib.log "End of Coqide.main"
-(* This function check every half of second if GeoProof has send
+(* This function check every tenth of second if GeoProof has send
something on his private clipboard *)
-let rec check_for_geoproof_input () =
+let check_for_geoproof_input () =
let cb_Dr = GData.clipboard (Gdk.Atom.intern "_GeoProof") in
- while true do
- Thread.delay 0.1;
- let s = cb_Dr#text in
- (match s with
- Some s ->
- if s <> "Ack" then (current_buffer ())#insert (s^"\n");
- cb_Dr#set_text "Ack"
- | None -> ()
- );
- (* cb_Dr#clear does not work so i use : *)
- (* cb_Dr#set_text "Ack" *)
- done
+ let handler () = match cb_Dr#text with
+ |None -> true
+ |Some "Ack" -> true
+ |Some s ->
+ (current_buffer ())#insert (s^"\n");
+ (* cb_Dr#clear does not work so i use : *)
+ cb_Dr#set_text "Ack";
+ true
+ in
+ ignore (GMain.Timeout.add ~ms:100 ~callback:handler)
(** By default, the coqtop we try to launch is exactly the current coqide
full name, with the last occurrence of "coqide" replaced by "coqtop".
View
6 ide/coqide.mli
@@ -24,7 +24,11 @@ val main : string list -> unit
(** Function to save anything and kill all coqtops
@return [false] if you're allowed to quit. *)
-val forbid_quit_to_save : unit -> bool
+val forbid_quit : unit -> bool
+
+(** Terminate coqide after closing all coqtops and waiting
+ for their death *)
+val close_and_quit : unit -> unit
(** Function to load of a file. *)
val do_load : string -> unit
View
23 ide/coqide_main.ml4
@@ -84,22 +84,13 @@ let reroute_stdout_stderr () =
(* We also provide specific kill and interrupt functions. *)
-(* Since [win32_interrupt] involves some hack about the process console,
- only one should run at the same time, we simply skip execution of
- [win32_interrupt] if another instance is already running *)
-
-let ctrl_c_mtx = Mutex.create ()
-
-let ctrl_c_protect f i =
- if not (Mutex.try_lock ctrl_c_mtx) then ()
- else try f i; Mutex.unlock ctrl_c_mtx with _ -> Mutex.unlock ctrl_c_mtx
-
IFDEF WIN32 THEN
external win32_kill : int -> unit = "win32_kill"
external win32_interrupt : int -> unit = "win32_interrupt"
let () =
Coq.killer := win32_kill;
- Coq.interrupter := ctrl_c_protect win32_interrupt;
+ Coq.soft_killer := win32_kill;
+ Coq.interrupter := win32_interrupt;
set_win32_path ();
reroute_stdout_stderr ()
END
@@ -115,6 +106,9 @@ let () =
in
let _ = osx#connect#ns_application_block_termination
~callback:Coqide.forbid_quit_to_save
+ in
+ let _ = osx#connect#ns_application_will_terminate
+ ~callback:Coqide.close_and_quit
in ()
let os_specific_init () =
@@ -147,10 +141,11 @@ let () =
Coq.check_connection args;
Coqide.sup_args := args;
Coqide.main files;
- if !Coq_config.with_geoproof then
- ignore (Thread.create Coqide.check_for_geoproof_input ());
+ if !Coq_config.with_geoproof then Coqide.check_for_geoproof_input ();
os_specific_init ();
- try GtkThread.main ()
+ try
+ GMain.main ();
+ failwith "Gtk loop ended"
with e ->
Minilib.log ("CoqIde unexpected error:" ^ Printexc.to_string e);
Coqide.crash_save 127
View
201 ide/ideutils.ml
@@ -15,9 +15,12 @@ exception Forbidden
let status = GMisc.statusbar ()
-let push_info,pop_info =
+let push_info,pop_info,clear_info =
let status_context = status#new_context ~name:"Messages" in
- (fun s -> ignore (status_context#push s)),status_context#pop
+ let size = ref 0 in
+ (fun s -> incr size; ignore (status_context#push s)),
+ (fun () -> decr size; status_context#pop ()),
+ (fun () -> for i = 1 to !size do status_context#pop () done; size := 0)
let flash_info =
let flash_context = status#new_context ~name:"Flash" in
@@ -219,35 +222,6 @@ let find_tag_stop (tag :GText.tag) (it:GText.iter) =
let find_tag_limits (tag :GText.tag) (it:GText.iter) =
(find_tag_start tag it , find_tag_stop tag it)
-(* explanations: Win32 threads won't work if events are produced
- in a thread different from the thread of the Gtk loop. In this
- case we must use GtkThread.async to push a callback in the
- main thread. Beware that the synchronus version may produce
- deadlocks. *)
-let async =
- if Sys.os_type = "Win32" then GtkThread.async else (fun x -> x)
-let sync =
- if Sys.os_type = "Win32" then GtkThread.sync else (fun x -> x)
-
-let mutex text f =
- let m = Mutex.create() in
- fun x ->
- if Mutex.try_lock m
- then
- (try
- Minilib.log ("Got lock on "^text);
- f x;
- Mutex.unlock m;
- Minilib.log ("Released lock on "^text)
- with e ->
- Mutex.unlock m;
- Minilib.log ("Released lock on "^text^" (on error)");
- raise e)
- else
- Minilib.log
- ("Discarded call for "^text^": computations ongoing")
-
-
let stock_to_widget ?(size=`DIALOG) s =
let img = GMisc.image ()
in img#set_stock s;
@@ -284,66 +258,15 @@ let rec print_list print fmt = function
let requote cmd = if Sys.os_type = "Win32" then "\""^cmd^"\"" else cmd