aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-05-17 23:45:26 +0200
committerEmilio Jesus Gallego Arias2018-05-24 13:21:59 +0200
commit5a564f986b5dcb74e347fbdc571d9e1a9980c2a4 (patch)
tree0b056da1338cb98e07bfc2271e58054c7ec298d2 /ide
parent9392d7ed7c1dfe3ad2b3d6b0f5e039353fbd6517 (diff)
[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
Diffstat (limited to 'ide')
-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.mllib8
-rw-r--r--ide/protocol/ideprotocol.mllib7
-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
21 files changed, 7 insertions, 8 deletions
diff --git a/ide/utils/configwin.ml b/ide/configwin.ml
index 69e8b647ae..69e8b647ae 100644
--- a/ide/utils/configwin.ml
+++ b/ide/configwin.ml
diff --git a/ide/utils/configwin.mli b/ide/configwin.mli
index 7616e471db..7616e471db 100644
--- a/ide/utils/configwin.mli
+++ b/ide/configwin.mli
diff --git a/ide/utils/configwin_ihm.ml b/ide/configwin_ihm.ml
index d16efa603d..d16efa603d 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 c867ad9127..c867ad9127 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 de1b4721d0..de1b4721d0 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 9e339d135d..9e339d135d 100644
--- a/ide/utils/configwin_types.mli
+++ b/ide/configwin_types.ml
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 96ea8c410e..a7ade71307 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 0000000000..8317a08681
--- /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 debbc8301e..debbc8301e 100644
--- a/ide/interface.mli
+++ b/ide/protocol/interface.ml
diff --git a/ide/richpp.ml b/ide/protocol/richpp.ml
index 19e9799c19..19e9799c19 100644
--- a/ide/richpp.ml
+++ b/ide/protocol/richpp.ml
diff --git a/ide/richpp.mli b/ide/protocol/richpp.mli
index 31fc7b56f1..31fc7b56f1 100644
--- a/ide/richpp.mli
+++ b/ide/protocol/richpp.mli
diff --git a/ide/serialize.ml b/ide/protocol/serialize.ml
index 86074d44d5..86074d44d5 100644
--- a/ide/serialize.ml
+++ b/ide/protocol/serialize.ml
diff --git a/ide/serialize.mli b/ide/protocol/serialize.mli
index af082f25b1..af082f25b1 100644
--- a/ide/serialize.mli
+++ b/ide/protocol/serialize.mli
diff --git a/ide/xml_lexer.mli b/ide/protocol/xml_lexer.mli
index e61cb055f7..e61cb055f7 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 4a52147e17..4a52147e17 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 8db3f9e8ba..8db3f9e8ba 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 ac2eab352f..ac2eab352f 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 488ef7bf57..488ef7bf57 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 178f7c808f..178f7c808f 100644
--- a/ide/xml_printer.mli
+++ b/ide/protocol/xml_printer.mli
diff --git a/ide/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml
index e18219210f..e18219210f 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/protocol/xmlprotocol.ml
diff --git a/ide/xmlprotocol.mli b/ide/protocol/xmlprotocol.mli
index ba6000f0a0..ba6000f0a0 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/protocol/xmlprotocol.mli