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
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
