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, 33 insertions, 25 deletions

diff --git a/ide/coq.mli b/ide/coq.mli
index c34c8f525..58bedca1b 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