Add interfaces for IDE and remove dead code.

Should fix #6177, which was triggered by lonely .ml files.

12 files changed, 120 insertions, 110 deletions

diff --git a/ide/config_lexer.mli b/ide/config_lexer.mli
new file mode 100644
index 000000000..0c0c5d1e7
--- /dev/null
+++ b/ide/config_lexer.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val print_file : string -> string list Util.String.Map.t -> unit
+val load_file : string -> string list Util.String.Map.t
diff --git a/ide/coq_commands.mli b/ide/coq_commands.mli
new file mode 100644
index 000000000..53026be38
--- /dev/null
+++ b/ide/coq_commands.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val tactics : string list list
+val commands : string list list
+val state_preserving : string list
diff --git a/ide/coq_lex.mli b/ide/coq_lex.mli
new file mode 100644
index 000000000..417e0a76f
--- /dev/null
+++ b/ide/coq_lex.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val delimit_sentences : (int -> GText.tag -> unit) -> string -> unit
+
+exception Unterminated
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 8d99cc3e6..6e330c62b 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -55,6 +55,8 @@ let os_specific_init () = ()
 
 (** Win32 *)
 
+IFDEF WIN32 THEN
+
 (* On win32, we add the directory of coqide to the PATH at launch-time
    (this used to be done in a .bat script). *)
 
@@ -86,7 +88,6 @@ let reroute_stdout_stderr () =
 
 (* We also provide specific kill and interrupt functions. *)
 
-IFDEF WIN32 THEN
 external win32_kill : int -> unit = "win32_kill"
 external win32_interrupt : int -> unit = "win32_interrupt"
 let () =
diff --git a/ide/coqide_main.mli b/ide/coqide_main.mli
new file mode 100644
index 000000000..e1555ba2e
--- /dev/null
+++ b/ide/coqide_main.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+   that does not have a corresponding .mli file *)
diff --git a/ide/coqide_ui.mli b/ide/coqide_ui.mli
new file mode 100644
index 000000000..9f6fa5635
--- /dev/null
+++ b/ide/coqide_ui.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val init : unit -> unit
+val ui_m : GAction.ui_manager
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index f0575e325..7c0a7495a 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -7,11 +7,7 @@
 (************************************************************************)
 
 let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0)
-let arobase = Glib.Utf8.to_unichar "@" ~pos:(ref 0)
 let prime = Glib.Utf8.to_unichar "'" ~pos:(ref 0)
-let bn = Glib.Utf8.to_unichar "\n" ~pos:(ref 0)
-let space = Glib.Utf8.to_unichar " " ~pos:(ref 0)
-let tab = Glib.Utf8.to_unichar "\t" ~pos:(ref 0)
 
 
 (* TODO: avoid num and prime at the head of a word *)
@@ -30,17 +26,6 @@ let ends_word (it:GText.iter) =
        not (is_word_char c)
   )
 
-
-let inside_word (it:GText.iter) =
-  let c = it#char in
-    not (starts_word it) &&
-      not (ends_word it) &&
-      is_word_char c
-
-
-let is_on_word_limit (it:GText.iter) = inside_word it || ends_word it
-
-
 let find_word_start (it:GText.iter) =
   let rec step_to_start it =
     Minilib.log "Find word start";
@@ -72,100 +57,6 @@ let get_word_around (it:GText.iter) =
   let stop =  find_word_end it in
     start,stop
 
-
-let rec complete_backward w (it:GText.iter) =
-  Minilib.log "Complete backward...";
-  match it#backward_search w with
-    | None -> (Minilib.log "backward_search failed";None)
-    | Some (start,stop) ->
-	Minilib.log ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset));
-	if starts_word start then
-	  let ne = find_word_end stop in
-	    if ne#compare stop = 0
-	    then complete_backward w start
-	    else Some (start,stop,ne)
-	else complete_backward w start
-
-
-let rec complete_forward w (it:GText.iter) =
-  Minilib.log "Complete forward...";
-  match it#forward_search w with
-    | None -> None
-    | Some (start,stop) ->
-	if starts_word start then
-	  let ne = find_word_end stop in
-	    if ne#compare stop = 0 then
-	      complete_forward w stop
-	    else Some (stop,stop,ne)
-	else complete_forward w stop
-
-
-let find_comment_end (start:GText.iter) =
-  let rec find_nested_comment (search_start:GText.iter) (search_end:GText.iter) (comment_end:GText.iter) =
-    match (search_start#forward_search ~limit:search_end "(*"),(comment_end#forward_search "*)") with
-      | None,_ -> comment_end
-      | Some _, None -> raise Not_found
-      | Some (_,next_search_start),Some (next_search_end,next_comment_end) ->
-          find_nested_comment next_search_start next_search_end next_comment_end
-  in
-    match start#forward_search "*)" with
-      | None -> raise Not_found
-      | Some (search_end,comment_end) -> find_nested_comment start search_end comment_end
-
-
-let rec find_string_end (start:GText.iter) =
-  let dblquote = int_of_char '"' in
-  let rec escaped_dblquote c =
-    (c#char = dblquote) && not (escaped_dblquote c#backward_char)
-  in
-    match start#forward_search "\"" with
-      | None -> raise Not_found
-      | Some (stop,next_start) ->
-          if escaped_dblquote stop#backward_char
-          then find_string_end next_start
-          else next_start
-
-
-let rec find_next_sentence (from:GText.iter) =
-  match (from#forward_search ".") with
-    | None -> raise Not_found
-    | Some (non_vernac_search_end,next_sentence) ->
-        match from#forward_search ~limit:non_vernac_search_end "(*",from#forward_search ~limit:non_vernac_search_end "\"" with
-          | None,None ->
-              if Glib.Unichar.isspace next_sentence#char || next_sentence#compare next_sentence#forward_char == 0
-              then next_sentence else find_next_sentence next_sentence
-          | None,Some (_,string_search_start) -> find_next_sentence (find_string_end string_search_start)
-          | Some (_,comment_search_start),None -> find_next_sentence (find_comment_end comment_search_start)
-          | Some (_,comment_search_start),Some (_,string_search_start) ->
-              find_next_sentence (
-                if comment_search_start#compare string_search_start < 0
-                then find_comment_end comment_search_start
-                else find_string_end string_search_start)
-
-
-let find_nearest_forward (cursor:GText.iter) targets =
-  let fold_targets acc target =
-    match cursor#forward_search target,acc with
-      | Some (t_start,_),Some nearest when (t_start#compare nearest < 0) -> Some t_start
-      | Some (t_start,_),None -> Some t_start
-      | _ -> acc
-  in
-    match List.fold_left fold_targets None targets with
-      | None -> raise Not_found
-      | Some nearest -> nearest
-
-
-let find_nearest_backward (cursor:GText.iter) targets =
-  let fold_targets acc target =
-    match cursor#backward_search target,acc with
-      | Some (t_start,_),Some nearest when (t_start#compare nearest > 0) -> Some t_start
-      | Some (t_start,_),None -> Some t_start
-      | _ -> acc
-  in
-    match List.fold_left fold_targets None targets with
-      | None -> raise Not_found
-      | Some nearest -> nearest
-
 (** On double-click on a view, select the whole word. This is a workaround for
     a deficient word handling in TextView. *)
 let fix_double_click self =
diff --git a/ide/gtk_parsing.mli b/ide/gtk_parsing.mli
new file mode 100644
index 000000000..b54f731b3
--- /dev/null
+++ b/ide/gtk_parsing.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val fix_double_click :
+  < buffer : < get_iter : [> `INSERT ] -> GText.iter;
+               move_mark : [> `INSERT | `SEL_BOUND ] ->
+                 where:GText.iter -> unit;
+               .. >;
+    event : < connect :
+                < button_press :
+                    callback:([> `TWO_BUTTON_PRESS ] Gdk.event ->
+                              bool) ->
+                    'a;
+                  .. >;
+              .. >;
+    .. > ->
+  unit
+val starts_word : GText.iter -> bool
+val ends_word : GText.iter -> bool
+val find_word_start : GText.iter -> GText.iter
+val find_word_end : GText.iter -> GText.iter
diff --git a/ide/ide_slave.mli b/ide/ide_slave.mli
new file mode 100644
index 000000000..e1555ba2e
--- /dev/null
+++ b/ide/ide_slave.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+   that does not have a corresponding .mli file *)
diff --git a/ide/macos_prehook.mli b/ide/macos_prehook.mli
new file mode 100644
index 000000000..e1555ba2e
--- /dev/null
+++ b/ide/macos_prehook.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+   that does not have a corresponding .mli file *)
diff --git a/ide/nanoPG.mli b/ide/nanoPG.mli
new file mode 100644
index 000000000..3ad8435b5
--- /dev/null
+++ b/ide/nanoPG.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val get_documentation : unit -> string
+val init : GWindow.window -> Session.session Wg_Notebook.typed_notebook ->
+           GAction.action_group list -> unit
diff --git a/ide/utf8_convert.mli b/ide/utf8_convert.mli
new file mode 100644
index 000000000..06a131a68
--- /dev/null
+++ b/ide/utf8_convert.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val f : string -> string