Ide: stronger separation from coqtop

 Former module Ide_blob is now divided in Ide_intf (linked both
 by coqtop and coqide) and Ide_slave (now only in coqtop).
 Ide_intf has almost no dependencies, we can now compile coqide
 with only coq_config.cm* and lib.cm(x)a

 TODO:
  - Devise a better way to display whether coqide is byte or opt
    in the about message (instead of Mltop.is_native, I display
    now the executable name, which hopefully contains opt or byte)
  - Check the late error handling in ide/coq.ml

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

1 files changed, 84 insertions, 0 deletions

diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
new file mode 100644
index 000000000..fb8c9e94d
--- /dev/null
+++ b/toplevel/ide_intf.ml
@@ -0,0 +1,84 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Interface of calls to Coq by CoqIde *)
+
+type 'a menu = 'a * (string * string) list
+
+type goals =
+  | Message of string
+  | Goals of ((string menu) list * string menu) list
+
+(** We use phantom types and GADT to protect ourselves against wild casts *)
+
+type 'a call =
+  | In_loadpath of string
+  | Raw_interp of string
+  | Interp of bool * string
+  | Rewind of int
+  | Read_stdout
+  | Cur_goals
+  | Cur_status
+  | Cases of string
+
+let is_in_loadpath s : bool call =
+  In_loadpath s
+
+let raw_interp s : unit call =
+  Raw_interp s
+
+let interp b s : int call =
+  Interp (b,s)
+
+let rewind i : int call =
+  Rewind i
+
+let read_stdout : string call =
+  Read_stdout
+
+let current_goals : goals call =
+  Cur_goals
+
+let current_status : string call =
+  Cur_status
+
+let make_cases s : string list list call =
+  Cases s
+
+(** * Coq answers to CoqIde *)
+
+type 'a value =
+  | Good of 'a
+  | Fail of (Util.loc option * string)
+
+type handler = {
+  is_in_loadpath : string -> bool;
+  raw_interp : string -> unit;
+  interp : bool -> string -> int;
+  rewind : int -> int;
+  read_stdout : unit -> string;
+  current_goals : unit -> goals;
+  current_status : unit -> string;
+  make_cases : string -> string list list;
+}
+
+let abstract_eval_call handler explain_exn c =
+  try
+    let res = match c with
+      | In_loadpath s -> Obj.magic (handler.is_in_loadpath s)
+      | Raw_interp s -> Obj.magic (handler.raw_interp s)
+      | Interp (b,s) -> Obj.magic (handler.interp b s)
+      | Rewind i -> Obj.magic (handler.rewind i)
+      | Read_stdout -> Obj.magic (handler.read_stdout ())
+      | Cur_goals -> Obj.magic (handler.current_goals ())
+      | Cur_status -> Obj.magic (handler.current_status ())
+      | Cases s -> Obj.magic (handler.make_cases s)
+    in Good res
+  with e ->
+    let (l,str) = explain_exn e in
+    Fail (l,str)