aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-17 23:45:26 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-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 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