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

1 files changed, 12 insertions, 6 deletions

diff --git a/ide/coqide.mli b/ide/coqide.mli
index de9eb0238..f6f5b616f 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