aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorEnrico Tassi2014-06-25 17:04:35 +0200
committerEnrico Tassi2014-06-25 17:04:35 +0200
commit753b8f4aaa78fe1cf8ea033d8cf45e88b5da9d13 (patch)
tree66ef0fdf8f9152d0740b1f875d80343bac1ae4af /dev
parent0a829ad04841d0973b22b4407b95f518276b66e7 (diff)
all coqide specific files moved into ide/
lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/
Diffstat (limited to 'dev')
-rw-r--r--dev/printers.mllib2
1 files changed, 2 insertions, 0 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 81fcc8493f..dcd3f0efbf 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -18,6 +18,8 @@ Loc
Compat
Flags
Control
+Loc
+Serialize
Pp
Segmenttree
Unicodetable