Coqide: avoid confusion of process when restarting coqtop + cosmetic

 When using "Goto start" while many phrases are evaluated,
 it's frequent with earlier code that the restart occurs
 between two phrases, and hence the second is sent to the new
 coqtop, triggering things like "Anomaly: NoCurrentProof".

 To avoid that, Coq.coqtop is now immutable (no silent switch
 of channels). In Coqide, toplvl and mycoqtop are now references,
 that are updated when using reset_coqtop.
 We organize things in order to have only one access to mycoqtop
 during code that does many sequential calls to coqtop. This way,
 when coqtop changes, the code speaks to the old one, and gets
 some exception when writing/reading on a close channel.

 By the way, some documentation, cleanup, etc etc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13942 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 186 insertions, 157 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index aea560eed3..3c7ee2de8e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -8,16 +8,11 @@
 
 open Ideutils
 
-type coqtop = {
-  mutable pid : int;
-  mutable cout : in_channel ;
-  mutable cin : out_channel ;
-  sup_args : string list;
-  mutable version : int ;
-}
-
 let prerr_endline s = if !debug then prerr_endline s else ()
 
+
+(** * Version and date *)
+
 let get_version_date () =
   let date =
     if Glib.Utf8.validate Coq_config.date
@@ -48,6 +43,9 @@ let version () =
       (Filename.basename Sys.executable_name)
       Coq_config.best
 
+
+(** * Initial checks by launching test coqtop processes *)
+
 let rec read_all_lines in_chan =
   try
     let arg = input_line in_chan in
@@ -110,25 +108,31 @@ let check_coqlib args =
       List.iter Pervasives.prerr_endline lines;
       exit 1
 
-let eval_call coqtop (c:'a Ide_intf.call) =
-  Marshal.to_channel coqtop.cin c [];
-  flush coqtop.cin;
-  (Marshal.from_channel: in_channel -> 'a Ide_intf.value) coqtop.cout
 
-let is_in_loadpath coqtop s = eval_call coqtop (Ide_intf.is_in_loadpath s)
- 
-let raw_interp coqtop s = eval_call coqtop (Ide_intf.raw_interp s)
+(** * The structure describing a coqtop sub-process *)
 
-let interp coqtop b s = eval_call coqtop (Ide_intf.interp (b,s))
+type coqtop = {
+  pid : int; (* Unix process id *)
+  cout : in_channel ;
+  cin : out_channel ;
+  sup_args : string list;
+}
 
-let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i)
- 
-let read_stdout coqtop = eval_call coqtop Ide_intf.read_stdout
+(** * Count of all active coqtops *)
 
 let toplvl_ctr = ref 0
 
 let toplvl_ctr_mtx = Mutex.create ()
 
+let coqtop_zombies () =
+  Mutex.lock toplvl_ctr_mtx;
+  let res = !toplvl_ctr in
+  Mutex.unlock toplvl_ctr_mtx;
+  res
+
+
+(** * Starting / signaling / ending a real coqtop sub-process *)
+
 (** We simulate a Unix.open_process that also returns the pid of
     the created process. Note: this uses Unix.create_process, which
     doesn't call bin/sh, so args shouldn't be quoted. The process
@@ -157,7 +161,7 @@ let spawn_coqtop sup_args =
     let (pid,ic,oc) = open_process_pid prog args in
     incr toplvl_ctr;
     Mutex.unlock toplvl_ctr_mtx;
-    { pid = pid; cin = oc; cout = ic ; sup_args = sup_args ; version = 0 }
+    { pid = pid; cin = oc; cout = ic ; sup_args = sup_args }
   with e ->
     Mutex.unlock toplvl_ctr_mtx;
     raise e
@@ -179,19 +183,31 @@ let blocking_kill pid =
 let kill_coqtop coqtop =
   ignore (Thread.create blocking_kill coqtop.pid)
 
-let coqtop_zombies =
-  (fun () ->
-     Mutex.lock toplvl_ctr_mtx;
-     let res = !toplvl_ctr in
-     Mutex.unlock toplvl_ctr_mtx;
-     res)
-
 let reset_coqtop coqtop =
   kill_coqtop coqtop;
-  let ni = spawn_coqtop coqtop.sup_args in
-  coqtop.cin <- ni.cin;
-  coqtop.cout <- ni.cout;
-  coqtop.pid <- ni.pid
+  spawn_coqtop coqtop.sup_args
+
+let process_exn = function
+  | End_of_file -> None, "Coqtop died"
+  | e -> None, Printexc.to_string e
+
+
+(** * Calls to coqtop *)
+
+(** Cf [Ide_intf] for more details *)
+
+let eval_call coqtop (c:'a Ide_intf.call) =
+  Marshal.to_channel coqtop.cin c [];
+  flush coqtop.cin;
+  (Marshal.from_channel: in_channel -> 'a Ide_intf.value) coqtop.cout
+
+let interp coqtop b s = eval_call coqtop (Ide_intf.interp (b,s))
+let raw_interp coqtop s = eval_call coqtop (Ide_intf.raw_interp s)
+let read_stdout coqtop = eval_call coqtop Ide_intf.read_stdout
+let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i)
+let is_in_loadpath coqtop s = eval_call coqtop (Ide_intf.is_in_loadpath s)
+let make_cases coqtop s = eval_call coqtop (Ide_intf.make_cases s)
+let current_status coqtop = eval_call coqtop Ide_intf.current_status
 
 module PrintOpt =
 struct
@@ -228,15 +244,8 @@ struct
     state_hack (Ide_intf.Good ())
 end
 
-let process_exn = function
-  | End_of_file -> None, "Coqtop died"
-  | e -> None, Printexc.to_string e
-
-let goals coqtop =
+let current_goals coqtop =
   match PrintOpt.enforce_hack coqtop with
     | Ide_intf.Good () -> eval_call coqtop Ide_intf.current_goals
     | Ide_intf.Fail str -> Ide_intf.Fail str
 
-let make_cases coqtop s = eval_call coqtop (Ide_intf.make_cases s)
-
-let current_status coqtop = eval_call coqtop Ide_intf.current_status
diff --git a/ide/coq.mli b/ide/coq.mli
index c34c8f5254..58bedca1b9 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -6,27 +6,53 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Coq : Interaction with the Coq toplevel *)
+
+(** * Version and date *)
+
 val short_version : unit -> string
 val version : unit -> string
+
+(** * Initial checks by launching test coqtop processes *)
+
 val filter_coq_opts : string list -> bool * string list
-(* A mock coqtop launch, checking in particular that initial.coq is found *)
+
+(** A mock coqtop launch, checking in particular that initial.coq is found *)
 val check_connection : string list -> unit
-(* Same, with less checks, but returning coqlib *)
+
+(** Same, with less checks, but returning coqlib *)
 val check_coqlib : string list -> string
 
+(** * The structure describing a coqtop sub-process *)
+
 type coqtop
 
-val spawn_coqtop : string list -> coqtop
+(** * Count of all active coqtops *)
 
-val kill_coqtop : coqtop -> unit
+val coqtop_zombies : unit -> int
 
+(** * Starting / signaling / ending a real coqtop sub-process *)
+
+val spawn_coqtop : string list -> coqtop
+val kill_coqtop : coqtop -> unit
 val break_coqtop : coqtop -> unit
+val reset_coqtop : coqtop -> coqtop
 
-val coqtop_zombies : unit -> int
+val process_exn : exn -> Ide_intf.location * string
 
-val reset_coqtop : coqtop -> unit
+(** * Calls to Coqtop, cf [Ide_intf] for more details *)
 
-val process_exn : exn -> Ide_intf.location * string
+val interp : coqtop -> bool -> string -> unit Ide_intf.value
+val raw_interp : coqtop -> string -> unit Ide_intf.value
+val read_stdout : coqtop -> string Ide_intf.value
+val rewind : coqtop -> int -> unit Ide_intf.value
+val is_in_loadpath : coqtop -> string -> bool Ide_intf.value
+val make_cases : coqtop -> string -> string list list Ide_intf.value
+val current_status : coqtop -> string Ide_intf.value
+val current_goals : coqtop -> Ide_intf.goals Ide_intf.value
+
+(** A specialized version of [raw_interp] dedicated to
+    set/unset options. *)
 
 module PrintOpt :
 sig
@@ -41,21 +67,3 @@ sig
 
   val set : coqtop -> t -> bool -> unit Ide_intf.value
 end
-
-val raw_interp : coqtop -> string -> unit Ide_intf.value
-
-val interp : coqtop -> bool -> string -> unit Ide_intf.value
-
-val rewind : coqtop -> int -> unit Ide_intf.value
-
-val read_stdout : coqtop -> string Ide_intf.value
-
-val is_in_loadpath : coqtop -> string -> bool Ide_intf.value
-
-val make_cases : coqtop -> string -> string list list Ide_intf.value
-
-(* Message to display in lower status bar. *)
-
-val current_status : coqtop -> string Ide_intf.value
-
-val goals : coqtop -> Ide_intf.goals Ide_intf.value
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 2437a61120..f32a3d79dd 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Preferences
-open Coq
-open Coq.PrintOpt
 open Gtk_parsing
 open Ideutils
 
@@ -17,9 +15,17 @@ type ide_info = {
   stop : GText.mark;
 }
 
+(** Have we used admit or declarative mode's daimon ?
+    If yes, we color differently *)
+
+type safety = Safe | Unsafe
+
+let safety_tag = function
+  | Safe -> Tags.Script.processed
+  | Unsafe -> Tags.Script.unjustified
 
 class type analyzed_views=
-object('self)
+object
   val mutable act_id : GtkSignal.id option
   val mutable deact_id : GtkSignal.id option
   val input_buffer : GText.buffer
@@ -31,6 +37,7 @@ object('self)
   val proof_buffer : GText.buffer
   val proof_view : GText.view
   val cmd_stack : ide_info Stack.t
+  val mycoqtop : Coq.coqtop ref
   val mutable is_active : bool
   val mutable read_only : bool
   val mutable filename : string option
@@ -72,17 +79,11 @@ object('self)
   method insert_command : string -> string -> unit
   method tactic_wizard : string list -> unit
   method insert_message : string -> unit
-  method insert_this_phrase_on_success :
-    bool -> bool -> bool -> string -> string -> bool
   method process_next_phrase : bool -> bool -> bool -> bool
   method process_until_iter_or_error : GText.iter -> unit
   method process_until_end_or_error : unit
   method recenter_insert : unit
   method reset_initial : bool -> unit
-  method send_to_coq :
-    bool -> bool -> string ->
-      bool -> bool -> bool ->
-	bool option
   method set_message : string -> unit
   method show_goals : unit
   method show_goals_full : unit
@@ -100,13 +101,13 @@ type viewable_script =
      proof_view : GText.view;
      message_view : GText.view;
      analyzed_view : analyzed_views;
-     toplvl : Coq.coqtop;
+     toplvl : Coq.coqtop ref;
      command : Command_windows.command_window;
     }
 
 let kill_session s =
   s.analyzed_view#kill_detached_views ();
-  Coq.kill_coqtop s.toplvl
+  Coq.kill_coqtop !(s.toplvl)
 
 let build_session s =
   let session_paned = GPack.paned `VERTICAL () in
@@ -177,6 +178,12 @@ let update_notebook_pos () =
 
 let to_do_on_page_switch = ref []
 
+
+(** * Coqide's handling of signals *)
+
+(** We ignore Ctrl-C, and for most of the other catchable signals
+    we launch an emergency save of opened files and then exit *)
+
 let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
 			Sys.sigill; Sys.sigpipe; Sys.sigquit;
 			(* Sys.sigsegv; Sys.sigterm;*) Sys.sigusr2]
@@ -211,6 +218,9 @@ let ignore_break () =
     signals_to_crash;
   Sys.set_signal Sys.sigint Sys.Signal_ignore
 
+
+(** * Locks *)
+
 (* Locking machinery for Coq kernel *)
 let coq_computing = Mutex.create ()
 
@@ -219,7 +229,7 @@ let coq_may_stop = Mutex.create ()
 
 let break () =
   prerr_endline "User break received";
-  Coq.break_coqtop session_notebook#current_term.toplvl
+  Coq.break_coqtop !(session_notebook#current_term.toplvl)
 
 let force_reset_initial () =
   prerr_endline "Reset Initial";
@@ -303,22 +313,24 @@ let remove_current_view_page () =
       | 2 -> do_remove ()
       | _ -> ()
 
+module Opt = Coq.PrintOpt
 
 let print_items = [
-  ([implicit],"Display _implicit arguments",GdkKeysyms._i,false);
-  ([coercions],"Display _coercions",GdkKeysyms._c,false);
-  ([raw_matching],"Display raw _matching expressions",GdkKeysyms._m,true);
-  ([notations],"Display _notations",GdkKeysyms._n,true);
-  ([all_basic],"Display _all basic low-level contents",GdkKeysyms._a,false);
-  ([existential],"Display _existential variable instances",GdkKeysyms._e,false);
-  ([universes],"Display _universe levels",GdkKeysyms._u,false);
-  ([all_basic;existential;universes],"Display all _low-level contents",GdkKeysyms._l,false)
+  ([Opt.implicit],"Display _implicit arguments",GdkKeysyms._i,false);
+  ([Opt.coercions],"Display _coercions",GdkKeysyms._c,false);
+  ([Opt.raw_matching],"Display raw _matching expressions",GdkKeysyms._m,true);
+  ([Opt.notations],"Display _notations",GdkKeysyms._n,true);
+  ([Opt.all_basic],"Display _all basic low-level contents",GdkKeysyms._a,false);
+  ([Opt.existential],"Display _existential variable instances",GdkKeysyms._e,false);
+  ([Opt.universes],"Display _universe levels",GdkKeysyms._u,false);
+  ([Opt.all_basic;Opt.existential;Opt.universes],
+   "Display all _low-level contents",GdkKeysyms._l,false)
 ]
 
 let setopts ct opts v =
   List.fold_left
     (fun acc o ->
-      match set ct o v with
+      match Coq.PrintOpt.set ct o v with
         | Ide_intf.Good () -> acc
         | Ide_intf.Fail lstr -> Ide_intf.Fail lstr
     ) (Ide_intf.Good ()) opts
@@ -405,23 +417,21 @@ exception Found
 (* For find_phrase_starting_at *)
 exception Stop of int
 
+let tag_of_sort = function
+  | Coq_lex.Comment -> Tags.Script.comment
+  | Coq_lex.Keyword -> Tags.Script.kwd
+  | Coq_lex.Declaration -> Tags.Script.decl
+  | Coq_lex.ProofDeclaration -> Tags.Script.proof_decl
+  | Coq_lex.Qed -> Tags.Script.qed
+  | Coq_lex.String -> failwith "No tag"
+
 let apply_tag (buffer:GText.buffer) orig off_conv from upto sort =
-  let conv_and_apply start stop tag =
+  try
+    let tag = tag_of_sort sort in
     let start = orig#forward_chars (off_conv from) in
     let stop = orig#forward_chars (off_conv upto) in
     buffer#apply_tag ~start ~stop tag
-  in match sort with
-    | Coq_lex.Comment ->
-      conv_and_apply from upto Tags.Script.comment
-    | Coq_lex.Keyword ->
-      conv_and_apply from upto Tags.Script.kwd
-    | Coq_lex.Declaration ->
-      conv_and_apply from upto Tags.Script.decl
-    | Coq_lex.ProofDeclaration ->
-      conv_and_apply from upto Tags.Script.proof_decl
-    | Coq_lex.Qed ->
-      conv_and_apply from upto Tags.Script.qed
-    | Coq_lex.String -> ()
+  with _ -> ()
 
 let remove_tags (buffer:GText.buffer) from upto =
   List.iter (buffer#remove_tag ~start:from ~stop:upto)
@@ -789,7 +799,7 @@ object(self)
         else
           (fun _ _ -> ()) in
       try
-        match Coq.goals mycoqtop with
+        match Coq.current_goals !mycoqtop with
           | Ide_intf.Fail (l,str) ->
             self#set_message ("Error in coqtop :\n"^str)
           | Ide_intf.Good goals ->
@@ -802,7 +812,7 @@ object(self)
 
   method show_goals = self#show_goals_full
 
-  method send_to_coq verbosely replace phrase show_output show_error localize =
+  method private send_to_coq ct verbosely phrase show_output show_error localize =
     let display_output msg =
       self#insert_message (if show_output then msg else "") in
     let display_error (loc,s) =
@@ -831,21 +841,18 @@ object(self)
     try
       full_goal_done <- false;
       prerr_endline "Send_to_coq starting now";
-      match Coq.interp mycoqtop verbosely phrase with
+      (* It's important here to work with [ct] and not [!mycoqtop], otherwise
+         we could miss a restart of coqtop and continue sending it orders. *)
+      match Coq.interp ct verbosely phrase with
         | Ide_intf.Fail (l,str) -> sync display_error (l,str); None
         | Ide_intf.Good () ->
-          match Coq.read_stdout mycoqtop with
-            | Ide_intf.Fail (_,str) ->
-              self#set_message
-                ("interp successful but unable to fetch goal, please report bug:\n"^str);
-              None
+	  match Coq.read_stdout ct with
+            | Ide_intf.Fail (l,str) -> sync display_error (l,str); None
             | Ide_intf.Good msg ->
               sync display_output msg;
-	      (* TODO: restore the access to Decl_mode.get_daemon_flag, and
-		 also detect if an admit has been used. Answering "false"
-		 in these cases would trigger a particular coloring
-		 (cf. Tags.Script.unjustified) *)
-              Some true
+	      (** TODO: Restore someday the access to Decl_mode.get_damon_flag,
+		  and also detect the use of admit, and then return Unsafe *)
+              Some Safe
     with
       | e ->
         sync display_error (Coq.process_exn e); None
@@ -884,7 +891,7 @@ object(self)
       end else false
     else false
 
-  method process_next_phrase verbosely display_goals do_highlight =
+  method private process_next_phrase_full ct verbosely display_goals do_highlight =
     let get_next_phrase () =
       self#clear_message;
       prerr_endline "process_next_phrase starting now";
@@ -913,11 +920,10 @@ object(self)
         input_view#set_editable true;
         pop_info ();
       end in
-    let mark_processed is_complete (start,stop) =
+    let mark_processed safe (start,stop) =
       let b = input_buffer in
       b#move_mark ~where:stop (`NAME "start_of_input");
-      b#apply_tag
-        (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop;
+      b#apply_tag (safety_tag safe) ~start ~stop;
       if (self#get_insert#compare) stop <= 0 then
         begin
           b#place_cursor ~where:stop;
@@ -932,23 +938,24 @@ object(self)
       match sync get_next_phrase () with
           None -> false
         | Some (loc,phrase) ->
-          (match self#send_to_coq verbosely false phrase true true true with
-            | Some is_complete ->
-              sync (mark_processed is_complete) loc; true
+          (match self#send_to_coq ct verbosely phrase true true true with
+            | Some safe -> sync mark_processed safe loc; true
             | None -> sync remove_tag loc; false)
     end
 
-  method insert_this_phrase_on_success
+  method process_next_phrase verbosely display_goals do_highlight =
+    self#process_next_phrase_full !mycoqtop verbosely display_goals do_highlight
+
+  method private insert_this_phrase_on_success
     show_output show_msg localize coqphrase insertphrase =
-    let mark_processed is_complete =
+    let mark_processed safe =
       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 start = self#get_start_of_input in
       input_buffer#move_mark ~where:stop (`NAME "start_of_input");
-      input_buffer#apply_tag
-        (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop;
+      input_buffer#apply_tag (safety_tag safe) ~start ~stop;
       if (self#get_insert#compare) stop <= 0 then
         input_buffer#place_cursor ~where:stop;
       let ide_payload = { start = `MARK (input_buffer#create_mark start);
@@ -980,9 +987,8 @@ object(self)
 	 | None -> ())
 	 | _ -> ())
 	 with _ -> ()*) in
-    match self#send_to_coq false false coqphrase show_output show_msg localize with
-      | Some is_complete ->
-        sync mark_processed is_complete; true
+    match self#send_to_coq !mycoqtop false coqphrase show_output show_msg localize with
+      | Some safe -> sync mark_processed safe; true
       | None ->
         sync
           (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
@@ -1006,8 +1012,13 @@ object(self)
         self#get_start_of_input
       end
     in
+    (* All the [process_next_phrase] below should be done with the same [ct]
+       instead of accessing multiple time [mycoqtop]. Otherwise a restart of
+       coqtop could go unnoticed, and the new coqtop could receive strange
+       things. *)
+    let ct = !mycoqtop in
     while ((stop#compare (get_current())>=0)
-           && (self#process_next_phrase false false false))
+           && (self#process_next_phrase_full ct false false false))
     do () done;
     sync (fun _ ->
       self#show_goals;
@@ -1022,7 +1033,7 @@ object(self)
     self#process_until_iter_or_error input_buffer#end_iter
 
   method reset_initial mustlock =
-    Coq.reset_coqtop mycoqtop;
+    mycoqtop := Coq.reset_coqtop !mycoqtop;
     if mustlock then Mutex.lock coq_computing;
     sync (fun _ ->
       Stack.iter
@@ -1055,7 +1066,7 @@ object(self)
     in
     begin
       try
-        match Coq.rewind mycoqtop (n_step 0) with
+        match Coq.rewind !mycoqtop (n_step 0) with
           | Ide_intf.Fail (l,str) ->
             sync self#set_message
               ("Error while backtracking :\n" ^ str ^ "\n" ^
@@ -1126,7 +1137,7 @@ object(self)
             self#show_goals;
             self#clear_message
           in
-          ignore (Coq.rewind mycoqtop 1);
+          ignore (Coq.rewind !mycoqtop 1);
           sync update_input ()
         with
           | Stack.Empty -> (* flash_info "Nothing to Undo"*)()
@@ -1202,18 +1213,18 @@ object(self)
       | None -> ()
       | Some f ->
 	let dir = Filename.dirname f in
-	match Coq.is_in_loadpath mycoqtop dir with
+	let ct = !mycoqtop in
+	match Coq.is_in_loadpath ct dir with
 	  | Ide_intf.Fail (_,str) ->
 	    self#set_message
 	      ("Could not determine lodpath, this might lead to problems:\n"^str)
 	  | Ide_intf.Good true -> ()
 	  | Ide_intf.Good false ->
-	    match Coq.interp mycoqtop false
-              (Printf.sprintf "Add LoadPath \"%s\". "  dir) with
-		| Ide_intf.Fail (l,str) ->
-		  self#set_message
-		    ("Couln't add loadpath:\n"^str)
-		| Ide_intf.Good () -> ()
+	    let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
+	    match Coq.interp ct false cmd with
+	      | Ide_intf.Fail (l,str) ->
+		self#set_message ("Couln't add loadpath:\n"^str)
+	      | Ide_intf.Good () -> ()
   end
 
   method electric_handler =
@@ -1397,16 +1408,11 @@ let create_session () =
     GText.view
       ~buffer:(GText.buffer ~tag_table:Tags.Message.table ())
       ~editable:false ~wrap_mode:`WORD () in
-  let basename =
-    GMisc.label ~text:"*scratch*" () in
-  let stack =
-    Stack.create () in
-  let ct =
-    spawn_coqtop !sup_args in
-  let command =
-    new Command_windows.command_window ct in
-  let legacy_av =
-    new analyzed_view script proof message stack ct in
+  let basename = GMisc.label ~text:"*scratch*" () in
+  let stack = Stack.create () in
+  let ct = ref (Coq.spawn_coqtop !sup_args) in
+  let command = new Command_windows.command_window !ct in
+  let legacy_av = new analyzed_view script proof message stack ct in
   let _ =
     script#buffer#create_mark ~name:"start_of_input" script#buffer#start_iter in
   let _ =
@@ -1414,7 +1420,7 @@ let create_session () =
   let _ =
     GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION] in
   let _ =
-    List.map (fun (opts,_,_,dflt) -> setopts ct opts dflt) print_items in
+    List.map (fun (opts,_,_,dflt) -> setopts !ct opts dflt) print_items in
   let _ = legacy_av#activate () in
   let _ =
     proof#event#connect#motion_notify ~callback:
@@ -2272,7 +2278,7 @@ let main files =
         ignore (f av);
         pop_info ();
         push_info
-          (match Coq.current_status current.toplvl with
+          (match Coq.current_status !(current.toplvl) with
             | Ide_intf.Fail (l,str) ->
 	      "Oops, problem while fetching coq status."
             | Ide_intf.Good str -> str)
@@ -2511,7 +2517,7 @@ let main files =
   (* Template for match *)
   let callback () =
     let w = get_current_word () in
-    let cur_ct = session_notebook#current_term.toplvl in
+    let cur_ct = !(session_notebook#current_term.toplvl) in
     try
       match Coq.make_cases cur_ct w with
         | Ide_intf.Fail _ -> raise Not_found
@@ -2668,7 +2674,7 @@ let main files =
       (fun (opts,text,key,dflt) ->
         view_factory#add_check_item ~key ~active:dflt text
           ~callback:(fun v -> do_or_activate (fun a ->
-            ignore (setopts session_notebook#current_term.toplvl opts v);
+            ignore (setopts !(session_notebook#current_term.toplvl) opts v);
             a#show_goals) ()))
       print_items
   in
@@ -3182,7 +3188,7 @@ let set_coqtop_path argv =
 
 let process_argv argv =
   try
-    let continue,filtered = filter_coq_opts (List.tl argv) in
+    let continue,filtered = Coq.filter_coq_opts (List.tl argv) in
     if not continue then
       (List.iter Pervasives.prerr_endline filtered; exit 0);
     let opts = List.filter (fun arg -> String.get arg 0 == '-') filtered in
diff --git a/ide/coqide.mli b/ide/coqide.mli
index de9eb02385..f6f5b616fd 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -6,10 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* The CoqIde main module. The following function [start] will parse the
-   command line, initialize the load path, load the input
-   state, load the files given on the command line, load the ressource file,
-   produce the output state if any, and finally will launch the interface. *)
+(** * The CoqIde main module *)
 
 (** The arguments that will be passed to coqtop. No quoting here, since
     no /bin/sh when using create_process instead of open_process. *)
@@ -22,9 +19,18 @@ val set_coqtop_path : string list -> string list
 (** Ask coqtop the remaining options it doesn't recognize *)
 val process_argv : string list -> string list
 
+(** Prepare the widgets, load the given files in tabs *)
+val main : string list -> unit
+
+(** The function doing the actual loading of a file. *)
 val do_load : string -> unit
 
-val crash_save : int -> unit
+(** Set coqide to ignore Ctrl-C, while launching [crash_save] and
+    exiting for others received signals *)
 val ignore_break : unit -> unit
+
+(** Emergency saving of opened files as "foo.v.crashcoqide",
+    and exit (if the integer isn't 127). *)
+val crash_save : int -> unit
+
 val check_for_geoproof_input : unit -> unit
-val main : string list -> unit