[ide] Move common protocol library to its own folder/object.

The `ide` folder contains two different binaries, the language server
`coqidetop` and `coqide` itself.

Even if these binaries are in the same folder, the only thing they
have in common is that they link to the protocol files. In the OCaml
world, having "doubly" linked files in the same project is considered
a bit of an ugly practice, and some build tools such as Dune disallow it.q

Thus, to clean up the build, we move the common protocol files to its
own library `ideprotocol`.

This helps towards Dune integration and towards having an IDE
standalone target, such as the one that was implemented here:
https://github.com/ejgallego/coqide-exp

25 files changed, 20 insertions, 21 deletions

diff --git a/.gitignore b/.gitignore
index f1960ba68..6adbc9fb2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -124,7 +124,7 @@ tools/coqwc.ml
 tools/coqdep_lexer.ml
 tools/ocamllibdep.ml
 tools/coqdoc/cpretty.ml
-ide/xml_lexer.ml
+ide/protocol/xml_lexer.ml
 
 # .ml4 / .mlp files
 
diff --git a/Makefile.build b/Makefile.build
index 7454e1b0c..036a3126b 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -206,7 +206,7 @@ OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
 
 BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
 OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(FLAMBDA_FLAGS)
-DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$@),, -I ide -I ide/utils)
+DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$@),, -I ide -I ide/protocol)
 
 # On MacOS, the binaries are signed, except our private ones
 ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin)
@@ -551,14 +551,11 @@ $(COQWORKMGRBYTE): $(COQWORKMGRCMO)
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqidetop
 
-FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/document.cmo	\
- ide/serialize.cmo ide/xml_lexer.cmo ide/xml_parser.cmo	\
- ide/xml_printer.cmo ide/richpp.cmo ide/xmlprotocol.cmo	\
- tools/fake_ide.cmo
+FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo tools/fake_ide.cmo
 
 $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP)
 	$(SHOW)'OCAMLBEST -o $@'
-	$(HIDE)$(call bestocaml, -I ide -package str -package dynlink)
+	$(HIDE)$(call bestocaml, -I ide -I ide/protocol -package str -package dynlink)
 
 $(FAKEIDEBYTE): $(FAKEIDECMO) | $(IDETOPLOOPCMA)
 	$(SHOW)'OCAMLC -o $@'
@@ -659,7 +656,7 @@ kernel/kernel.cmxa: kernel/kernel.mllib
 	$(SHOW)'OCAMLOPT -pack -o $@'
 	$(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^)
 
-COND_IDEFLAGS=$(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,)
+COND_IDEFLAGS=$(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide -I ide/protocol,)
 COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,)
 
 COND_BYTEFLAGS= \
diff --git a/Makefile.ide b/Makefile.ide
index 48b554912..6bb0f62f3 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -39,11 +39,11 @@ COQIDEINAPP:=$(COQIDEAPP)/Contents/MacOS/coqide
 # one that will be loaded by coqidetop) refers to some
 # core modules of coq, for instance printing/*.
 
-IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils
+IDESRCDIRS:= $(CORESRCDIRS) ide ide/protocol
 
 COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES)
 
-IDEDEPS:=clib/clib.cma lib/lib.cma
+IDEDEPS:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma
 IDECMA:=ide/ide.cma
 IDETOPEXE=bin/coqidetop$(EXE)
 IDETOP=bin/coqidetop.opt$(EXE)
@@ -146,7 +146,7 @@ $(IDETOPEXE): $(IDETOP:.opt=.$(BEST))
 
 $(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide \
+	$(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \
 			   $(SYSMOD) -package camlp5.gramlib \
 			   $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@
 	$(STRIP) $@
@@ -154,7 +154,7 @@ $(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX)
 
 $(IDETOPBYTE): ide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) -I ide \
+	$(HIDE)$(OCAMLC) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \
 	                 -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
 			 $(SYSMOD) -package camlp5.gramlib \
 			 $(LINKCMO) $(IDETOPCMA) $(BYTEFLAGS) $< -o $@
diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
index ca0076b46..b22ab3630 100644
--- a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
+++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh
@@ -1,6 +1,9 @@
 #!/bin/sh
 
-if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || [ "$CI_BRANCH" = "pr-6859" ]; then
+if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top"   ] ||     \
+   [ "$CI_PULL_REQUEST" = "7543" ] || [ "$CI_BRANCH" = "ide+split" ] ; then
+
     pidetop_CI_BRANCH=stm+top
     pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git
+
 fi
diff --git a/ide/utils/configwin.ml b/ide/configwin.ml
index 69e8b647a..69e8b647a 100644
--- a/ide/utils/configwin.ml
+++ b/ide/configwin.ml
diff --git a/ide/utils/configwin.mli b/ide/configwin.mli
index 7616e471d..7616e471d 100644
--- a/ide/utils/configwin.mli
+++ b/ide/configwin.mli
diff --git a/ide/utils/configwin_ihm.ml b/ide/configwin_ihm.ml
index d16efa603..d16efa603 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/configwin_ihm.ml
diff --git a/ide/utils/configwin_ihm.mli b/ide/configwin_ihm.mli
index c867ad912..c867ad912 100644
--- a/ide/utils/configwin_ihm.mli
+++ b/ide/configwin_ihm.mli
diff --git a/ide/utils/configwin_messages.ml b/ide/configwin_messages.ml
index de1b4721d..de1b4721d 100644
--- a/ide/utils/configwin_messages.ml
+++ b/ide/configwin_messages.ml
diff --git a/ide/utils/configwin_types.mli b/ide/configwin_types.ml
index 9e339d135..9e339d135 100644
--- a/ide/utils/configwin_types.mli
+++ b/ide/configwin_types.ml
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 96ea8c410..a7ade7130 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,15 +9,7 @@ Config_lexer
 Utf8_convert
 Preferences
 Project_file
-Serialize
-Richprinter
-Xml_lexer
-Xml_parser
-Xml_printer
-Serialize
-Richpp
 Topfmt
-Xmlprotocol
 Ideutils
 Coq
 Coq_lex
diff --git a/ide/protocol/ideprotocol.mllib b/ide/protocol/ideprotocol.mllib
new file mode 100644
index 000000000..8317a0868
--- /dev/null
+++ b/ide/protocol/ideprotocol.mllib
@@ -0,0 +1,7 @@
+Xml_lexer
+Xml_parser
+Xml_printer
+Serialize
+Richpp
+Interface
+Xmlprotocol
diff --git a/ide/interface.mli b/ide/protocol/interface.ml
index debbc8301..debbc8301 100644
--- a/ide/interface.mli
+++ b/ide/protocol/interface.ml
diff --git a/ide/richpp.ml b/ide/protocol/richpp.ml
index 19e9799c1..19e9799c1 100644
--- a/ide/richpp.ml
+++ b/ide/protocol/richpp.ml
diff --git a/ide/richpp.mli b/ide/protocol/richpp.mli
index 31fc7b56f..31fc7b56f 100644
--- a/ide/richpp.mli
+++ b/ide/protocol/richpp.mli
diff --git a/ide/serialize.ml b/ide/protocol/serialize.ml
index 86074d44d..86074d44d 100644
--- a/ide/serialize.ml
+++ b/ide/protocol/serialize.ml
diff --git a/ide/serialize.mli b/ide/protocol/serialize.mli
index af082f25b..af082f25b 100644
--- a/ide/serialize.mli
+++ b/ide/protocol/serialize.mli
diff --git a/ide/xml_lexer.mli b/ide/protocol/xml_lexer.mli
index e61cb055f..e61cb055f 100644
--- a/ide/xml_lexer.mli
+++ b/ide/protocol/xml_lexer.mli
diff --git a/ide/xml_lexer.mll b/ide/protocol/xml_lexer.mll
index 4a52147e1..4a52147e1 100644
--- a/ide/xml_lexer.mll
+++ b/ide/protocol/xml_lexer.mll
diff --git a/ide/xml_parser.ml b/ide/protocol/xml_parser.ml
index 8db3f9e8b..8db3f9e8b 100644
--- a/ide/xml_parser.ml
+++ b/ide/protocol/xml_parser.ml
diff --git a/ide/xml_parser.mli b/ide/protocol/xml_parser.mli
index ac2eab352..ac2eab352 100644
--- a/ide/xml_parser.mli
+++ b/ide/protocol/xml_parser.mli
diff --git a/ide/xml_printer.ml b/ide/protocol/xml_printer.ml
index 488ef7bf5..488ef7bf5 100644
--- a/ide/xml_printer.ml
+++ b/ide/protocol/xml_printer.ml
diff --git a/ide/xml_printer.mli b/ide/protocol/xml_printer.mli
index 178f7c808..178f7c808 100644
--- a/ide/xml_printer.mli
+++ b/ide/protocol/xml_printer.mli
diff --git a/ide/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml
index e18219210..e18219210 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/protocol/xmlprotocol.ml
diff --git a/ide/xmlprotocol.mli b/ide/protocol/xmlprotocol.mli
index ba6000f0a..ba6000f0a 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/protocol/xmlprotocol.mli