aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-08 20:44:51 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-08 20:44:51 +0000
commit6254115b358899886163da4a4add6d419a55b1e9 (patch)
tree5f37a3928443adaea1f5a8dd561cb35ea6ecdd08 /ide
parente7e52a4c56954f148a5ded1a2f7c2794b115a166 (diff)
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
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml490
-rw-r--r--ide/coq.mli122
-rw-r--r--ide/coqide.ml860
-rw-r--r--ide/coqide.mli6
-rw-r--r--ide/coqide_main.ml423
-rw-r--r--ide/ideutils.ml201
-rw-r--r--ide/ideutils.mli22
-rw-r--r--ide/wg_Command.ml38
-rw-r--r--ide/wg_ScriptView.ml166
-rw-r--r--ide/wg_ScriptView.mli4
10 files changed, 979 insertions, 953 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 7f927042e..01c6c36b7 100644
--- a/ide/coq.ml
+++ b/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)
diff --git a/ide/coq.mli b/ide/coq.mli
index 43a040822..041485237 100644
--- a/ide/coq.mli
+++ b/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
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 596ef25d9..f12ea9a24 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -60,7 +60,6 @@ let logfile = ref None
class type _analyzed_view =
object
-
method filename : string option
method update_stats : unit
method changed_on_disk : bool
@@ -68,22 +67,22 @@ object
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,51 +591,7 @@ 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
@@ -660,25 +599,46 @@ object(self)
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,16 +778,38 @@ 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
@@ -834,52 +817,39 @@ object(self)
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,9 +1373,7 @@ 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
@@ -1420,8 +1381,9 @@ let coq_makefile _ =
|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".
diff --git a/ide/coqide.mli b/ide/coqide.mli
index ca5396950..f9e711455 100644
--- a/ide/coqide.mli
+++ b/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
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 282dfce99..a9b10e60c 100644
--- a/ide/coqide_main.ml4
+++ b/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
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 9b7dcd67a..35a5a2477 100644
--- a/ide/ideutils.ml
+++ b/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,59 +258,6 @@ let rec print_list print fmt = function
let requote cmd = if Sys.os_type = "Win32" then "\""^cmd^"\"" else cmd
-let browse f url =
- let com = Util.subst_command_placeholder current.cmd_browse url in
- let _ = Unix.open_process_out com in ()
-(* This beautiful message will wait for twt ...
- if s = 127 then
- f ("Could not execute\n\""^com^
- "\"\ncheck your preferences for setting a valid browser command\n")
-*)
-let doc_url () =
- if current.doc_url = use_default_doc_url || current.doc_url = "" then
- let addr = List.fold_left Filename.concat (Coq_config.docdir)
- ["html";"refman";"index.html"]
- in
- if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman
- else current.doc_url
-
-let url_for_keyword =
- let ht = Hashtbl.create 97 in
- lazy (
- begin try
- let cin =
- try let index_urls = Filename.concat (List.find
- (fun x -> Sys.file_exists (Filename.concat x "index_urls.txt"))
- (Minilib.coqide_config_dirs ())) "index_urls.txt" in
- open_in index_urls
- with Not_found ->
- let doc_url = doc_url () in
- let n = String.length doc_url in
- if n > 8 && String.sub doc_url 0 7 = "file://" then
- open_in (String.sub doc_url 7 (n-7) ^ "index_urls.txt")
- else
- raise Exit
- in
- try while true do
- let s = input_line cin in
- try
- let i = String.index s ',' in
- let k = String.sub s 0 i in
- let u = String.sub s (i + 1) (String.length s - i - 1) in
- Hashtbl.add ht k u
- with _ ->
- Minilib.log "Warning: Cannot parse documentation index file."
- done with End_of_file ->
- close_in cin
- with _ ->
- Minilib.log "Warning: Cannot find documentation index file."
- end;
- Hashtbl.find ht : string -> string)
-
-let browse_keyword f text =
- try let u = Lazy.force url_for_keyword text in browse f (doc_url() ^ u)
- with Not_found -> f ("No documentation found for \""^text^"\".\n")
-
let textview_width (view : #GText.view) =
let rect = view#visible_rect in
let pixel_width = Gdk.Rectangle.width rect in
@@ -344,6 +265,8 @@ let textview_width (view : #GText.view) =
let char_width = GPango.to_pixels metrics#approx_char_width in
pixel_width / char_width
+type logger = Interface.message_level -> string -> unit
+
let default_logger level message =
let level = match level with
| Interface.Debug _ -> `DEBUG
@@ -367,15 +290,119 @@ let stat f =
| Unix.Unix_error (Unix.ENOENT,_,_) -> NoSuchFile
| _ -> OtherError
+(** I/O utilities
+
+ Note: In a mono-thread coqide, we use the same buffer for
+ different read operations *)
+
+let maxread = 1024
+
+let read_string = String.create maxread
+let read_buffer = Buffer.create maxread
+
(** Read the content of file [f] and add it to buffer [b].
I/O Exceptions are propagated. *)
let read_file name buf =
let ic = open_in name in
- let s = String.create 1024 and len = ref 0 in
+ let len = ref 0 in
try
- while len := input ic s 0 1024; !len > 0 do
- Buffer.add_substring buf s 0 !len
+ while len := input ic read_string 0 maxread; !len > 0 do
+ Buffer.add_substring buf read_string 0 !len
done;
close_in ic
with e -> close_in ic; raise e
+
+(** Read a gtk asynchronous channel *)
+
+let io_read_all chan =
+ Buffer.clear read_buffer;
+ let rec loop () =
+ let len = Glib.Io.read ~buf:read_string ~pos:0 ~len:maxread chan in
+ Buffer.add_substring read_buffer read_string 0 len;
+ if len < maxread then Buffer.contents read_buffer
+ else loop ()
+ in loop ()
+
+(** Run an external command asynchronously *)
+
+let run_command display finally cmd =
+ let cin = Unix.open_process_in cmd in
+ let io_chan = Glib.Io.channel_of_descr (Unix.descr_of_in_channel cin) in
+ let all_conds = [`ERR; `HUP; `IN; `NVAL; `PRI] in (* all except `OUT *)
+ let rec has_errors = function
+ | [] -> false
+ | (`IN | `PRI) :: conds -> has_errors conds
+ | e :: _ -> true
+ in
+ let handle_end () = finally (Unix.close_process_in cin); false
+ in
+ let handle_input conds =
+ if has_errors conds then handle_end ()
+ else
+ let s = io_read_all io_chan in
+ if s = "" then handle_end ()
+ else (display (try_convert s); true)
+ in
+ ignore (Glib.Io.add_watch ~cond:all_conds ~callback:handle_input io_chan)
+
+(** Web browsing *)
+
+let browse prerr url =
+ let com = Util.subst_command_placeholder current.cmd_browse url in
+ let finally = function
+ | Unix.WEXITED 127 ->
+ prerr
+ ("Could not execute:\n"^com^"\n"^
+ "check your preferences for setting a valid browser command\n")
+ | _ -> ()
+ in
+ run_command (fun _ -> ()) finally com
+
+let doc_url () =
+ if current.doc_url = use_default_doc_url || current.doc_url = ""
+ then
+ let addr = List.fold_left Filename.concat (Coq_config.docdir)
+ ["html";"refman";"index.html"]
+ in
+ if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman
+ else current.doc_url
+
+let url_for_keyword =
+ let ht = Hashtbl.create 97 in
+ lazy (
+ begin try
+ let cin =
+ try let index_urls = Filename.concat (List.find
+ (fun x -> Sys.file_exists (Filename.concat x "index_urls.txt"))
+ (Minilib.coqide_config_dirs ())) "index_urls.txt" in
+ open_in index_urls
+ with Not_found ->
+ let doc_url = doc_url () in
+ let n = String.length doc_url in
+ if n > 8 && String.sub doc_url 0 7 = "file://" then
+ open_in (String.sub doc_url 7 (n-7) ^ "index_urls.txt")
+ else
+ raise Exit
+ in
+ try while true do
+ let s = input_line cin in
+ try
+ let i = String.index s ',' in
+ let k = String.sub s 0 i in
+ let u = String.sub s (i + 1) (String.length s - i - 1) in
+ Hashtbl.add ht k u
+ with _ ->
+ Minilib.log "Warning: Cannot parse documentation index file."
+ done with End_of_file ->
+ close_in cin
+ with _ ->
+ Minilib.log "Warning: Cannot find documentation index file."
+ end;
+ Hashtbl.find ht : string -> string)
+
+let browse_keyword prerr text =
+ try
+ let u = Lazy.force url_for_keyword text in
+ browse prerr (doc_url() ^ u)
+ with Not_found -> prerr ("No documentation found for \""^text^"\".\n")
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index eb5cf1a56..2598dee33 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -6,12 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-val async : ('a -> unit) -> 'a -> unit
-val sync : ('a -> 'b) -> 'a -> 'b
-
-(* avoid running two instances of a function concurrently *)
-val mutex : string -> ('a -> unit) -> 'a -> unit
-
val doc_url : unit -> string
val browse : (string -> unit) -> string -> unit
val browse_keyword : (string -> unit) -> string -> unit
@@ -49,6 +43,7 @@ val coqtop_path : unit -> string
val status : GMisc.statusbar
val push_info : string -> unit
val pop_info : unit -> unit
+val clear_info : unit -> unit
val flash_info : ?delay:int -> string -> unit
val set_location : (string -> unit) ref
@@ -63,10 +58,12 @@ val requote : string -> string
val textview_width : #GText.view -> int
(** Returns an approximate value of the character width of a textview *)
+type logger = Interface.message_level -> string -> unit
+
val default_logger : Interface.message_level -> string -> unit
(** Default logger. It logs messages that the casual user should not see. *)
-(** {6 File operations} *)
+(** {6 I/O operations} *)
(** A customized [stat] function. Exceptions are catched. *)
@@ -77,3 +74,14 @@ val stat : string -> stats
I/O Exceptions are propagated. *)
val read_file : string -> Buffer.t -> unit
+
+(** Read the available content on some gtk asynchronous input channel *)
+
+val io_read_all : Glib.Io.channel -> string
+
+(** [run_command display finally cmd] allow to run a command
+ asynchronously, calling [display] on any output of this command
+ and [finally] when the command has returned. *)
+
+val run_command :
+ (string -> unit) -> (Unix.process_status -> unit) -> string -> unit
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 2e4ce364d..98ce63faf 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -111,18 +111,16 @@ object(self)
if String.get com (String.length com - 1) = '.'
then com ^ " " else com ^ " " ^ entry#text ^" . "
in
- let insert level message =
- result#buffer#insert message;
- result#buffer#insert "\n"
+ let log level message = result#buffer#insert (message^"\n")
in
- let process handle =
- let answer = match Coq.interp handle insert ~raw:true phrase with
- | Interface.Fail (l,str) ->
- "Error while interpreting "^phrase^":\n"^str
- | Interface.Good results | Interface.Unsafe results ->
- "Result for command " ^ phrase ^ ":\n" ^ results
- in
- result#buffer#insert answer
+ let process h k =
+ Coq.interp ~logger:log ~raw:true phrase h (function
+ |Interface.Fail (l,str) ->
+ result#buffer#insert ("Error while interpreting "^phrase^":\n"^str);
+ k ()
+ |Interface.Good res | Interface.Unsafe res ->
+ result#buffer#insert ("Result for command " ^ phrase ^ ":\n" ^ res);
+ k ())
in
result#buffer#set_text "";
Coq.try_grab coqtop process ignore
@@ -130,17 +128,13 @@ object(self)
ignore (combo#entry#connect#activate ~callback:(on_activate callback));
ignore (ok_b#connect#clicked ~callback:(on_activate callback));
- begin match command,term with
- | None,None -> ()
- | Some c, None ->
- combo#entry#set_text c;
-
- | Some c, Some t ->
- combo#entry#set_text c;
- entry#set_text t
-
- | None , Some t ->
- entry#set_text t
+ begin match command with
+ | None -> ()
+ | Some c -> combo#entry#set_text c
+ end;
+ begin match term with
+ | None -> ()
+ | Some t -> entry#set_text t
end;
on_activate callback ();
entry#misc#grab_focus ();
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 82dd77344..0ab946d65 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -42,7 +42,7 @@ end
module Proposals = Set.Make(StringOrd)
-let get_completion (buffer : GText.buffer) coqtop w =
+let get_completion (buffer : GText.buffer) coqtop w handle_res =
let rec get_aux accu (iter : GText.iter) =
match iter#forward_search w with
| None -> accu
@@ -56,23 +56,23 @@ let get_completion (buffer : GText.buffer) coqtop w =
else get_aux accu stop
in
let get_semantic accu =
- let ans = ref accu in
let flags = [Interface.Name_Pattern ("^" ^ w), true] in
- let query handle = match Coq.search handle flags with
- | Interface.Good l ->
- let fold accu elt =
- let rec last accu = function
- | [] -> accu
- | [basename] -> Proposals.add basename accu
- | _ :: l -> last accu l
- in
- last accu elt.Interface.coq_object_qualid
- in
- ans := (List.fold_left fold accu l)
- | _ -> ()
+ let query h k =
+ Coq.search flags h
+ (function
+ | Interface.Good l ->
+ let fold accu elt =
+ let rec last accu = function
+ | [] -> accu
+ | [basename] -> Proposals.add basename accu
+ | _ :: l -> last accu l
+ in
+ last accu elt.Interface.coq_object_qualid
+ in
+ handle_res (List.fold_left fold accu l) k
+ | _ -> handle_res accu k)
in
Coq.try_grab coqtop query ignore;
- !ans
in
get_semantic (get_aux Proposals.empty buffer#start_iter)
@@ -88,8 +88,6 @@ object (self)
(* this variable prevents CoqIDE from autocompleting when we have deleted something *)
val mutable is_auto_completing = false
- val undo_lock = Mutex.create ()
-
method auto_complete = auto_complete
method set_auto_complete flag =
@@ -142,51 +140,35 @@ object (self)
self#buffer#insert_interactive ~iter s
method undo () =
- if Mutex.try_lock undo_lock then begin
- Minilib.log "UNDO";
- let effective = self#process_action history in
- if effective then self#backward ();
- Mutex.unlock undo_lock;
- effective
- end else
- (Minilib.log "UNDO DISCARDED"; true)
+ Minilib.log "UNDO";
+ let effective = self#process_action history in
+ if effective then self#backward ()
method redo () =
- if Mutex.try_lock undo_lock then begin
- Minilib.log "REDO";
- let effective = self#process_action redo in
- if effective then self#forward ();
- Mutex.unlock undo_lock;
- effective
- end else
- (Minilib.log "REDO DISCARDED"; true)
+ Minilib.log "REDO";
+ let effective = self#process_action redo in
+ if effective then self#forward ()
method private handle_insert iter s =
(* we're inserting, so we may autocomplete *)
is_auto_completing <- true;
(* Save the insert action *)
- if Mutex.try_lock undo_lock then begin
- let action = Insert (s, iter#offset, Glib.Utf8.length s) in
- history <- action :: history;
- redo <- [];
- self#dump_debug ();
- Mutex.unlock undo_lock
- end
+ let action = Insert (s, iter#offset, Glib.Utf8.length s) in
+ history <- action :: history;
+ redo <- [];
+ self#dump_debug ()
method private handle_delete ~start ~stop =
(* disable autocomplete *)
is_auto_completing <- false;
(* Save the delete action *)
- if Mutex.try_lock undo_lock then begin
- let start_offset = start#offset in
- let stop_offset = stop#offset in
- let s = self#buffer#get_text ~start ~stop () in
- let action = Delete (s, start_offset, stop_offset - start_offset) in
- history <- action :: history;
- redo <- [];
- self#dump_debug ();
- Mutex.unlock undo_lock
- end
+ let start_offset = start#offset in
+ let stop_offset = stop#offset in
+ let s = self#buffer#get_text ~start ~stop () in
+ let action = Delete (s, start_offset, stop_offset - start_offset) in
+ history <- action :: history;
+ redo <- [];
+ self#dump_debug ();
method private do_auto_complete () =
let iter = self#buffer#get_iter `INSERT in
@@ -197,33 +179,35 @@ object (self)
if String.length w >= auto_complete_length then begin
Minilib.log ("Completion of prefix: '" ^ w ^ "'");
let (off, prefix, proposals) = last_completion in
- let new_proposals =
- (* check whether we have the last request in cache *)
- if (start#offset = off) && (0 <= is_substring prefix w) then
- Proposals.filter (fun p -> 0 < is_substring w p) proposals
- else
- let ans = get_completion self#buffer ct w in
- let () = last_completion <- (start#offset, w, ans) in
- ans
- in
- let prop =
- try Some (Proposals.choose new_proposals)
- with Not_found -> None
- in
- match prop with
- | None -> ()
- | Some proposal ->
- let suffix =
- let len1 = String.length proposal in
- let len2 = String.length w in
- String.sub proposal len2 (len1 - len2)
+ let handle_proposals isnew new_proposals k =
+ if isnew then last_completion <- (start#offset, w, new_proposals);
+ let prop =
+ try Some (Proposals.choose new_proposals)
+ with Not_found -> None
in
- let offset = iter#offset in
- ignore (self#buffer#delete_selection ());
- ignore (self#buffer#insert_interactive suffix);
- let ins = self#buffer#get_iter (`OFFSET offset) in
- let sel = self#buffer#get_iter `INSERT in
- self#buffer#select_range sel ins
+ match prop with
+ | None -> k ()
+ | Some proposal ->
+ let suffix =
+ let len1 = String.length proposal in
+ let len2 = String.length w in
+ String.sub proposal len2 (len1 - len2)
+ in
+ let offset = iter#offset in
+ ignore (self#buffer#delete_selection ());
+ ignore (self#buffer#insert_interactive suffix);
+ let ins = self#buffer#get_iter (`OFFSET offset) in
+ let sel = self#buffer#get_iter `INSERT in
+ self#buffer#select_range sel ins;
+ k ()
+ in
+ (* check whether we have the last request in cache *)
+ if (start#offset = off) && (0 <= is_substring prefix w) then
+ handle_proposals false
+ (Proposals.filter (fun p -> 0 < is_substring w p) proposals)
+ (fun () -> ())
+ else
+ get_completion self#buffer ct w (handle_proposals true)
end
end
@@ -340,8 +324,10 @@ object (self)
(* Install auto-completion *)
ignore (self#buffer#connect#after#end_user_action ~callback:self#may_auto_complete);
(* HACK: Redirect the undo/redo signals of the underlying GtkSourceView *)
- ignore (self#connect#undo (fun _ -> ignore (self#undo ()); GtkSignal.stop_emit()));
- ignore (self#connect#redo (fun _ -> ignore (self#redo ()); GtkSignal.stop_emit()));
+ ignore (self#connect#undo
+ ~callback:(fun _ -> ignore (self#undo ()); GtkSignal.stop_emit()));
+ ignore (self#connect#redo
+ ~callback:(fun _ -> ignore (self#redo ()); GtkSignal.stop_emit()));
(* HACK: Redirect the move_line signal of the underlying GtkSourceView *)
let move_line_marshal = GtkSignal.marshal2
Gobject.Data.boolean Gobject.Data.int "move_line_marshal"
@@ -360,9 +346,11 @@ object (self)
(* do we forward the signal? *)
let proceed =
if not b && i = 1 then
- iter#editable true && iter#forward_line#editable true
+ iter#editable ~default:true &&
+ iter#forward_line#editable ~default:true
else if not b && i = -1 then
- iter#editable true && iter#backward_line#editable true
+ iter#editable ~default:true &&
+ iter#backward_line#editable ~default:true
else false
in
if not proceed then GtkSignal.stop_emit ()
@@ -376,11 +364,13 @@ let script_view ct ?(source_buffer:GSourceView2.source_buffer option) ?draw_spa
GtkSourceView2.SourceView.make_params [] ~cont:(
GtkText.View.make_params ~cont:(
GContainer.pack_container ~create:
- (fun pl -> let w = match source_buffer with
- | None -> GtkSourceView2.SourceView.new_ ()
- | Some buf -> GtkSourceView2.SourceView.new_with_buffer
- (Gobject.try_cast buf#as_buffer "GtkSourceBuffer") in
- let w = Gobject.unsafe_cast w in
- Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl;
- Gaux.may (GtkSourceView2.SourceView.set_draw_spaces w) draw_spaces;
- ((new script_view w ct) : script_view))))
+ (fun pl ->
+ let w = match source_buffer with
+ | None -> GtkSourceView2.SourceView.new_ ()
+ | Some buf -> GtkSourceView2.SourceView.new_with_buffer
+ (Gobject.try_cast buf#as_buffer "GtkSourceBuffer")
+ in
+ let w = Gobject.unsafe_cast w in
+ Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl;
+ Gaux.may ~f:(GtkSourceView2.SourceView.set_draw_spaces w) draw_spaces;
+ ((new script_view w ct) : script_view))))
diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli
index e94ce4904..efe33f54d 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/wg_ScriptView.mli
@@ -13,8 +13,8 @@ type source_view = [ Gtk.text_view | `sourceview ] Gtk.obj
class script_view : source_view -> Coq.coqtop ->
object
inherit GSourceView2.source_view
- method undo : unit -> bool
- method redo : unit -> bool
+ method undo : unit -> unit
+ method redo : unit -> unit
method clear_undo : unit -> unit
method auto_complete : bool
method set_auto_complete : bool -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 20:49:06 +0000