diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-17 23:45:26 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-24 13:21:59 +0200 |
commit | 5a564f986b5dcb74e347fbdc571d9e1a9980c2a4 (patch) | |
tree | 0b056da1338cb98e07bfc2271e58054c7ec298d2 /ide | |
parent | 9392d7ed7c1dfe3ad2b3d6b0f5e039353fbd6517 (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.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 |
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 |