ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mli

The .mli only acknowledges the current API. I'm not guilty your honor!

8 files changed, 86 insertions, 15 deletions

diff --git a/.gitignore b/.gitignore
index 8bbfce5d8..6e6f01a43 100644
--- a/.gitignore
+++ b/.gitignore
@@ -128,7 +128,7 @@ ide/xml_lexer.ml
 
 g_*.ml
 
-ide/project_file.ml
+lib/coqProject_file.ml
 parsing/cLexer.ml
 plugins/ltac/coretactics.ml
 plugins/ltac/extratactics.ml
diff --git a/Makefile.build b/Makefile.build
index 56f1fb8b4..8aedd9cec 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -377,7 +377,7 @@ $(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,)
 
-COQMAKEFILECMO:=lib/clib.cma ide/project_file.cmo tools/coq_makefile.cmo
+COQMAKEFILECMO:=lib/clib.cma tools/coq_makefile.cmo
 
 $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO))
 	$(SHOW)'OCAMLBEST -o $@'
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 0b7567a5a..e47db8d19 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -84,7 +84,7 @@ let pr_exit_status = function
 let make_coqtop_args = function
   |None -> "", !sup_args
   |Some the_file ->
-    let get_args f = Project_file.args_from_project f
+    let get_args f = CoqProject_file.args_from_project f
       !custom_project_files project_file_name#get
     in
     match read_project#get with
@@ -1346,7 +1346,7 @@ let read_coqide_args argv =
       else (output_string stderr "Error: multiple -coqtop options"; exit 1)
     |"-f" :: file :: args ->
       let d = CUnix.canonical_path_name (Filename.dirname file) in
-      let p = Project_file.read_project_file file in
+      let p = CoqProject_file.read_project_file file in
       filter_coqtop coqtop ((d,p) :: project_files) out args
     |"-f" :: [] ->
       output_string stderr "Error: missing project file name"; exit 1
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 78b4c01e8..57e9fe5ad 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,6 +9,8 @@ Config_lexer
 Utf8_convert
 Preferences
 Project_file
+Serialize
+Richprinter
 Xml_lexer
 Xml_parser
 Xml_printer
diff --git a/lib/clib.mllib b/lib/clib.mllib
index c73ae9b90..71f728291 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -32,3 +32,4 @@ CUnix
 Envars
 Aux_file
 Monad
+CoqProject_file
diff --git a/ide/project_file.ml4 b/lib/coqProject_file.ml4
index d32273bc2..d32273bc2 100644
--- a/ide/project_file.ml4
+++ b/lib/coqProject_file.ml4
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
new file mode 100644
index 000000000..36513dbde
--- /dev/null
+++ b/lib/coqProject_file.mli
@@ -0,0 +1,68 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type target =
+  | ML of string (* ML file : foo.ml -> (ML "foo.ml") *)
+  | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *)
+  | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *)
+  | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *)
+  | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *)
+  | V of string  (* V file : foo.v -> (V "foo") *)
+  | Arg of string
+  | Special of string * string * bool * string
+    (* file, dependencies, is_phony, command *)
+  | Subdir of string
+  | Def of string * string (* X=foo -> Def ("X","foo") *)
+  | MLInclude of string (* -I physicalpath *)
+  | Include of string * string (* -Q physicalpath logicalpath *)
+  | RInclude of string * string (* -R physicalpath logicalpath *)
+
+type install =
+  | NoInstall
+  | TraditionalInstall
+  | UserInstall
+  | UnspecInstall
+
+exception Parsing_error
+
+val args_from_project : 
+           string ->
+           (string *
+            ('a *
+             (('b * string) list * ('c * string * string) list *
+              ('d * string * string) list) *
+             (string list * 'e)))
+           list -> string -> string * string list
+
+val read_project_file :
+           string ->
+           (string list *
+            (string list * string list * string list * string list *
+             string list) *
+            (string * string * bool * string) list * string list) *
+           ((string * string) list * (string * string * string) list *
+            (string * string * string) list) *
+           (string list * (string * string) list)
+
+val process_cmd_line :
+           string ->
+           string option * string option * install * bool ->
+           target list ->
+           string list ->
+           (string option * string option * install * bool) * target list
+
+val split_arguments :
+           target list ->
+           (string list *
+            (string list * string list * string list * string list *
+             string list) *
+            (string * string * bool * string) list * string list) *
+           ((string * string) list * (string * string * string) list *
+            (string * string * string) list) *
+           (string list * (string * string) list)
+
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 4875cb62b..d72916232 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -282,7 +282,7 @@ let where_put_doc = function
 	"$(INSTALLDEFAULTROOT)"
 
 let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function
-  |Project_file.NoInstall -> ()
+  |CoqProject_file.NoInstall -> ()
   |is_install ->
     let not_empty = function |[] -> false |_::_ -> true in
     let cmos = List.rev_append mlpacks (List.rev_append mls ml4s) in
@@ -295,7 +295,7 @@ let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function
        ("CMOFILES",cmos);("CMIFILES",cmis);("CMAFILES",mllibs)]
       inc in
     let doc_dir = where_put_doc inc in
-    if is_install = Project_file.UnspecInstall then begin
+    if is_install = CoqProject_file.UnspecInstall then begin
 	print "userinstall:\n\t+$(MAKE) USERINSTALL=true install\n\n"
     end;
     if not_empty cmxss then begin
@@ -533,8 +533,8 @@ let variables is_install opt (args,defs) =
 \n  $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
     end;
     match is_install with
-      | Project_file.NoInstall -> ()
-      | Project_file.UnspecInstall ->
+      | CoqProject_file.NoInstall -> ()
+      | CoqProject_file.UnspecInstall ->
         section "Install Paths.";
 	print "ifdef USERINSTALL\n";
         print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n";
@@ -545,13 +545,13 @@ let variables is_install opt (args,defs) =
         print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n";
         print "COQTOPINSTALL=\"${COQLIB}toploop\"\n";
 	print "endif\n\n"
-      | Project_file.TraditionalInstall ->
+      | CoqProject_file.TraditionalInstall ->
           section "Install Paths.";
           print "COQLIBINSTALL=\"${COQLIB}user-contrib\"\n";
           print "COQDOCINSTALL=\"${DOCDIR}user-contrib\"\n";
           print "COQTOPINSTALL=\"${COQLIB}toploop\"\n";
           print "\n"
-      | Project_file.UserInstall ->
+      | CoqProject_file.UserInstall ->
           section "Install Paths.";
           print "XDG_DATA_HOME?=\"$(HOME)/.local/share\"\n";
           print "COQLIBINSTALL=$(XDG_DATA_HOME)/coq\n";
@@ -895,11 +895,11 @@ let do_makefile args =
     |_::_ -> var := true in
   let (project_file,makefile,is_install,opt),l =
     try
-      Project_file.process_cmd_line Filename.current_dir_name
-       (None,None,Project_file.UnspecInstall,true) [] args
-    with Project_file.Parsing_error -> usage () in
+      CoqProject_file.process_cmd_line Filename.current_dir_name
+       (None,None,CoqProject_file.UnspecInstall,true) [] args
+    with CoqProject_file.Parsing_error -> usage () in
   let (v_f,(mli_f,ml4_f,ml_f,mllib_f,mlpack_f),sps,sds as targets), inc, defs =
-    Project_file.split_arguments l in
+    CoqProject_file.split_arguments l in
 
   let () = match project_file with |None -> () |Some f -> make_name := f in
   let () = match makefile with
@@ -920,7 +920,7 @@ let do_makefile args =
     List.iter check_dep (Str.split (Str.regexp "[ \t]+") dependencies)) sps;
 
   let inc = ensure_root_dir targets inc in
-  if is_install <> Project_file.NoInstall then begin
+  if is_install <> CoqProject_file.NoInstall then begin
     warn_install_at_root_directory targets inc;
   end;
   check_overlapping_include inc;