diff options
| -rw-r--r-- | Makefile.build | 10 | ||||
| -rw-r--r-- | _tags | 4 | ||||
| -rw-r--r-- | ide/coq.ml | 490 | ||||
| -rw-r--r-- | ide/coq.mli | 122 | ||||
| -rw-r--r-- | ide/coqide.ml | 860 | ||||
| -rw-r--r-- | ide/coqide.mli | 6 | ||||
| -rw-r--r-- | ide/coqide_main.ml4 | 23 | ||||
| -rw-r--r-- | ide/ideutils.ml | 201 | ||||
| -rw-r--r-- | ide/ideutils.mli | 22 | ||||
| -rw-r--r-- | ide/wg_Command.ml | 38 | ||||
| -rw-r--r-- | ide/wg_ScriptView.ml | 166 | ||||
| -rw-r--r-- | ide/wg_ScriptView.mli | 4 | ||||
| -rw-r--r-- | myocamlbuild.ml | 4 |
13 files changed, 988 insertions, 962 deletions
diff --git a/Makefile.build b/Makefile.build index c3768528e..24f024df4 100644 --- a/Makefile.build +++ b/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 @@ -8,7 +8,7 @@ <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 @@ -16,7 +16,7 @@ ## tags for ide -<ide/**/*.{ml,mli}>: thread, ide +<ide/**/*.{ml,mli}>: ide ## tags for grammar.cm* 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 diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 793522f84..b08e54673 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -308,9 +308,9 @@ let extra_rules () = begin flag ["ocaml"; "ide"; "compile"] lablgtkincl; flag ["ocaml"; "ide"; "link"] lablgtkincl; flag ["ocaml"; "ide"; "link"; "byte"] - (S [A"lablgtk.cma"; A"lablgtksourceview2.cma"; A"gtkThread.cmo"]); + (S [A"lablgtk.cma"; A"lablgtksourceview2.cma"]); flag ["ocaml"; "ide"; "link"; "native"] - (S [A"lablgtk.cmxa"; A"lablgtksourceview2.cmxa"; A"gtkThread.cmx"]); + (S [A"lablgtk.cmxa"; A"lablgtksourceview2.cmxa"]); (** C code for the VM *) |