aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/xmlprotocol.mli
Commit message (Collapse)AuthorAge
* Add XML protocol support for Wait.Gravatar Maxime Dénès2017-09-19
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* [xml] Restore protocol compatibility with 8.6.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | By default, we serialize messages to the "rich printing representation" as it was done in 8.6, this ways clients don't have to adapt unless they specifically request the new format using option `--xml_format=Ppcmds`
* [ide] richpp clenaupGravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | We remove the "abstraction breaking" primitives and reduce the file to the used fragment.
* [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously to this patch, Coq featured to distinct logging paths: the console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format` module, and the `Feedback` one, intended to encapsulate message inside a more general, GUI-based feedback protocol. This patch removes the legacy logging path and makes feedback canonical. Thus, the core of Coq has no dependency on console code anymore. Additionally, this patch resolves the duplication of "document" formats present in the same situation. The original console-based printing code relied on an opaque datatype `std_ppcmds`, (mostly a reification of `Format`'s format strings) that could be then rendered to the console. However, the feedback path couldn't reuse this type due to its opaque nature. The first versions just embedded rending of `std_ppcmds` to a string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was introduced. The idea for this type was to be serializable, however it brought several problems: it didn't have proper document manipulation operations, its format was overly verbose and didn't preserve the full layout, and it still relied on `Format` for generation, making client-side rendering difficult. We thus follow the plan outlined in CEP#9, that is to say, we take a public and refactored version of `std_ppcmds` as the canonical "document type", and move feedback to be over there. The toplevel now is implemented as a feedback listener and has ownership of the console. `richpp` is now IDE-specific, and only used for legacy rendering. It could go away in future versions. `std_ppcmds` carries strictly more information and is friendlier to client-side rendering and display control. Thus, the new panorama is: - `Feedback` has become a very module for event dispatching. - `Pp` contains a target-independent box-based document format. It also contains the `Format`-based renderer. - All console access lives in `toplevel`, with console handlers private to coqtop. _NOTE_: After this patch, many printing parameters such as printing width or depth should be set client-side. This works better IMO, clients don't need to notify Coq about resizing anywmore. Indeed, for box-based capable backends such as HTML or LaTeX, the UI can directly render and let the engine perform the word breaking work. _NOTE_: Many messages could benefit from new features of the output format, however we have chosen not to alter them to preserve output. A Future commits will move console tag handling in `Pp_style` to `toplevel/`, where it logically belongs. The only change with regards to printing is that the "Error:" header was added to console output in several different positions, we have removed some of this duplication, now error messages should be a bit more consistent.
* [ide] Use "log via feedback".Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | We remove the custom logger handler in ide_slave, and handle everything via feedback. This is an experimental patch but it seems to bring quite a bit of cleanup and a more uniform handling to messaging.
* [feedback] Allow messages to carry a location.Gravatar Emilio Jesus Gallego Arias2016-06-25
| | | | | | | The new warnings mechanism may which to forward a location to IDEs. This also makes sense for other message types. Next step is to remove redundant MsgError feedback type.
* Encapsulate xml serialization in xmlprotocol.mliGravatar Emilio Jesus Gallego Arias2016-06-02
| | | | | | | | | | | | | | | This eases the task of replacing/improving the serializer, as well as making it more resistant. See pitfalls below: Main changes are: - fold `message` type into `feedback` type - make messages of type `Richpp.richpp` so we are explicit about the content being a rich document. - moved serialization functions for messages and stateid to `Xmlprotocol` - improved a couple of internal API points (`is_message`). Tested.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Using GADTs in Xmlprotocol.Gravatar Pierre-Marie Pédrot2015-10-22
|/ | | | This removes 109 Obj.magic in one patch!
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* ide/{Xmlprotocol,Interface,Ide_slave}: New command "annotate".Gravatar Regis-Gianas2014-11-04
| | | | | | | | | | | | | | - Extend the protocol with a new command called "annotate". - By the way, relax the dependencies between the "ide" package and the internal packages of Coq by *not* referring to external type definitions inside Interface. Indeed, the purpose of the protocol is to act as a barrier between the source tree of Coq and the source tree of Coqide. We should enforce this property. (Maybe one day coqide will be extracted from the source tree of Coq to live its own life.)
* CoqIDE: new message to print ASTGravatar Enrico Tassi2014-09-29
|
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
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/