> This said, I don't see any hand parsing or pre/post processing tricks > when reading SerAPI's sexps: I only see the prin1-to-sexp hack which > works around the nil-vs-() difference. So maybe the syntax is closer to > that of Elisp than shown in the README.md.
Indeed; in practice it works OK. There's a minimal example of an IDE implementation based on SerAPI at https://github.com/cpitclaudel/elcoq/blob/master/elcoq.el Clément. On 30/11/2018 10.46, Stefan Monnier wrote: > Looking at SerAPI, I'm wondering about the choice of "sexp". I know it > may sound odd to want something else than sexps when working in Elisp, > but in reality sexps only work well if they use *exactly* the same > syntax. E.g. in https://github.com/ejgallego/coq-serapi I see: > > (Query ((sid 3) (pp ((pp_format PpStr)))) Goals) > > (Answer 3 Ack) > > (Answer 3 (ObjList ((CoqString > > "\ > > \n n : nat\ > > \n============================\ > > \nn + 0 = n")))) > > (Answer 3 Completed) > > which seems to show that the strings don't use the same escape syntax as > Elisp. This little detail will likely end up forcing the Elisp side to > either re-implement a sexp-reader by hand (in Elisp, which will be > slowish), or require ugly hacks to try and pre-process the answer before > passing it to the sexp reader (or post-process the sexp), which will > likely always end up flaky. > > Same thing when it comes to turning Elisp sexps into the print > representation of SerAPI sexps, of course. > > This said, I don't see any hand parsing or pre/post processing tricks > when reading SerAPI's sexps: I only see the prin1-to-sexp hack which > works around the nil-vs-() difference. So maybe the syntax is closer to > that of Elisp than shown in the README.md. > > Otherwise I see 2 convenient options: tweak the sexp syntax so it is > a 100% subset of that of Elisp or use some other widespread standard > such as XML or JSON (modern Emacsen can link to efficient parsers of > those two). The first option is of course more convenient for Emacs, > but I understand that the second is more convenient for all the > non-Emacs clients and it's not that bad for Emacs. > > > Stefan >
signature.asc
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
