diff options
| author | Regis-Gianas | 2014-11-04 12:09:42 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 22:51:36 +0100 |
| commit | 6905915f7ce8989dc64473118ada94adf9a20cd9 (patch) | |
| tree | c9076534e14552d20d2b35690df839100b16c7bd | |
| parent | d3b4b78faced5dae3c4b8f2b05dc40375a7a6d91 (diff) | |
ide/Ide_slave.annotate: Implement annotate.
| -rw-r--r-- | ide/ide_slave.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 4186f6cf03..a4e84903e2 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -119,7 +119,14 @@ let edit_at id = let query (s,id) = Stm.query ~at:id s; read_stdout () let annotate phrase = - Xml_datatype.PCData "FIXME" + let (loc, ast) = + let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in + Vernac.parse_sentence (pa,None) + in + let (_, _, xml) = + RichPrinter.richpp_vernac ast + in + xml (** Goal display *) |