diff options
-rw-r--r-- | .gitignore | 2 | ||||
-rw-r--r-- | Makefile.build | 11 | ||||
-rw-r--r-- | Makefile.ide | 8 | ||||
-rw-r--r-- | dev/ci/user-overlays/06859-ejgallego-stm+top.sh | 5 | ||||
-rw-r--r-- | ide/configwin.ml (renamed from ide/utils/configwin.ml) | 0 | ||||
-rw-r--r-- | ide/configwin.mli (renamed from ide/utils/configwin.mli) | 0 | ||||
-rw-r--r-- | ide/configwin_ihm.ml (renamed from ide/utils/configwin_ihm.ml) | 0 | ||||
-rw-r--r-- | ide/configwin_ihm.mli (renamed from ide/utils/configwin_ihm.mli) | 0 | ||||
-rw-r--r-- | ide/configwin_messages.ml (renamed from ide/utils/configwin_messages.ml) | 0 | ||||
-rw-r--r-- | ide/configwin_types.ml (renamed from ide/utils/configwin_types.mli) | 0 | ||||
-rw-r--r-- | ide/ide.mllib | 8 | ||||
-rw-r--r-- | ide/protocol/ideprotocol.mllib | 7 | ||||
-rw-r--r-- | ide/protocol/interface.ml (renamed from ide/interface.mli) | 0 | ||||
-rw-r--r-- | ide/protocol/richpp.ml (renamed from ide/richpp.ml) | 0 | ||||
-rw-r--r-- | ide/protocol/richpp.mli (renamed from ide/richpp.mli) | 0 | ||||
-rw-r--r-- | ide/protocol/serialize.ml (renamed from ide/serialize.ml) | 0 | ||||
-rw-r--r-- | ide/protocol/serialize.mli (renamed from ide/serialize.mli) | 0 | ||||
-rw-r--r-- | ide/protocol/xml_lexer.mli (renamed from ide/xml_lexer.mli) | 0 | ||||
-rw-r--r-- | ide/protocol/xml_lexer.mll (renamed from ide/xml_lexer.mll) | 0 | ||||
-rw-r--r-- | ide/protocol/xml_parser.ml (renamed from ide/xml_parser.ml) | 0 | ||||
-rw-r--r-- | ide/protocol/xml_parser.mli (renamed from ide/xml_parser.mli) | 0 | ||||
-rw-r--r-- | ide/protocol/xml_printer.ml (renamed from ide/xml_printer.ml) | 0 | ||||
-rw-r--r-- | ide/protocol/xml_printer.mli (renamed from ide/xml_printer.mli) | 0 | ||||
-rw-r--r-- | ide/protocol/xmlprotocol.ml (renamed from ide/xmlprotocol.ml) | 0 | ||||
-rw-r--r-- | ide/protocol/xmlprotocol.mli (renamed from ide/xmlprotocol.mli) | 0 |
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 a8f3ea501..b85418243 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) | $(IDETOPBYTE) $(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 |