diff options
| author | Pierre-Marie Pédrot | 2018-06-22 12:24:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-07 16:34:44 +0200 |
| commit | ef29c0a927728d9cf4a45bc3c26d2393d753184e (patch) | |
| tree | d43b108a24ac69f7fbcdd184781141fea36a1dd5 /ide | |
| parent | 4b3187a635864f8faa2d512775231a4e6d204c51 (diff) | |
Introduce a Pcoq.Entry module for functions that ought to be exported.
We deprecate the corresponding functions in Pcoq.Gram. The motivation is
that the Gram module is used as an argument to Camlp5 functors, so that
it is not stable by extension. Enforcing that its type is literally the
one Camlp5 expects ensures robustness to extension statically.
Some really internal functions have been bluntly removed. It is unlikely
that they are used by external plugins.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/idetop.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml index 6fb0040611..0c3328ee08 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -80,7 +80,7 @@ let set_doc doc = ide_doc := Some doc let add ((s,eid),(sid,verbose)) = let doc = get_doc () in - let pa = Pcoq.Gram.parsable (Stream.of_string s) in + let pa = Pcoq.Parsable.make (Stream.of_string s) in let loc_ast = Stm.parse_sentence ~doc sid pa in let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in set_doc doc; @@ -113,14 +113,14 @@ let edit_at id = * be removed in the next version of the protocol. *) let query (route, (s,id)) = - let pa = Pcoq.Gram.parsable (Stream.of_string s) in + let pa = Pcoq.Parsable.make (Stream.of_string s) in let doc = get_doc () in Stm.query ~at:id ~doc ~route pa let annotate phrase = let doc = get_doc () in let {CAst.loc;v=ast} = - let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in + let pa = Pcoq.Parsable.make (Stream.of_string phrase) in Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa in (* XXX: Width should be a parameter of annotate... *) |