aboutsummaryrefslogtreecommitdiff
path: root/lib/interface.mli
AgeCommit message (Collapse)Author
2014-06-25all coqide specific files moved into ide/Enrico Tassi
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/
2014-04-10Have the feedback bus as a backend for dumping globs.Carst Tankink
2014-03-12Stm: smarter delegation policyEnrico Tassi
Stm used to delegate every proof when it was possible, but this may be a bad idea. Small proofs may take less time than the overhead delegation implies (marshalling, etc...). Now it delegates only proofs that take >= 1 second. By default a proof takes 1 second (that may be wrong). If the file was compiled before, it reuses the data stored in the .aux file and assumes the timings are still valid. After a proof is checked, Coq knows how long it takes for real, so it wont predict it wrong again (when the user goes up and down in the file for example). CoqIDE now sends to Coq, as part of the init message, the file name so that Coq can load the .aux file.
2014-01-30STM + CoqIDE: stop_worker message and UIEnrico Tassi
2014-01-30STM: tell the user if the master is recomputing states validated by workersEnrico Tassi
When the worker fails, the master may need to recompute some states the worker has already validates. In this case they are colored accordingly.
2013-12-24CoqIDE: new feedback "incomplete" to signal partial QedEnrico Tassi
2013-11-27Old message Interp returns the state id so that one can BackTo itEnrico Tassi
2013-11-27First stab at retrocompatible INTERP messageEnrico Tassi
2013-11-02Adds a tactic give_up.aspiwack
Gives up on the focused goals. Shows an unsafe status. Unlike the admit tactic, the proof cannot be closed until the users goes back and solves these goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17018 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Adds a shelve tactic.aspiwack
The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17013 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22New feedback message: SlaveStatusgareuselesinge
To tell the gui what a slave is doing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16898 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01typogareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16833 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE protocol/serialization revisedgareuselesinge
- both requests and responses are serialized using the same generic code - no more interp message. Replaced by: - query: performs a query (Search/Check...) at a given state - add: adds to the document a new sentence at the current edit point - edit_at: changes the edit point. the result could be a rewind _or_ a focus to a specific zone that can be edited without rewinding the whole document git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16812 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-12CoqIDE: show number of proofs being checked in backgroundgareuselesinge
good test: Nijmegen/QArithSternBrocot/Zaux.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16773 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-19Modulification and removing of structural equality in Stateid.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Coqide ported to STMgareuselesinge
Main changes for STM: 1) protocol changed to carry edit/state ids 2) colouring reflects the actual status of every span (evaluated or not) 3) button to force the evaluation of the whole buffer 4) cmd_stack and backtracking completely changed to use state numbers instead of counting sentences 5) feedback messages are completely asynchronous, and the whole protocol could be made so with a minor effort, but there is little point in it right now. Left as a future improvement. Missing bit: add sentence-id to responses of interp command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16677 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Coqide: Globalization feedback (proof of concept)gareuselesinge
A new feedback message for globalization infos can be sent by Coq to Coqide. Coqide stores the information in the proof of concept module wg_Tooltip, that also sets things up so that these infos are displayed as a tooltip when the mouse is over the text they are attached to. These infos are available only on locked text, and on the text just processed in the case of an error (on this piece of text, they vanish as the error tag vanishes as soon as the user edits the text). wg_Tooltip stocks these infos as lazy string. This is not needed in the proof of concept, but is necessary to scale up: Coq may not generate the full piece of info when the message is sent (because of high computational cost or big size) and just send an id; later on, when/if the user asks for the piece of info, the gui requests the info explicitly using the id. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16456 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25raise UnsafeSuccess -> feedback AddedAxiomgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Coqide: new feedback mechanism for structured contentgareuselesinge
This amounts to a new type of message called "feedback" and defined in Interface to hold structured data. Coq sends feedback messages asynchronously (they are all fetched, like regular messages, together with the main response to a call) and they are related to a specific sentence by an id. Other changes: - CoqOps pushes the sentence to be processed onto the cmd_stack before processing it and pulls it back if Coq.intep fails, in this way the handler for feedback messages can just look at the cmd_stack to find the offset of the sentence to eventually apply the new Gtk.tag. - The class coqops takes in input a coqtop to set its feedback_handle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16451 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Fix indentationgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16450 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-19interface.mli and serialize.ml reworked to avoid copy/paste of typesgareuselesinge
With this commit the types involved in the protocol between Coq and Coqide are written once and for all in interface.mli serialize.ml is monkey code that contains a reified version of these types and the related machinery needed to marshal values in these types to/from xml in a modular way. This file should be automatically generated from the spec of the protocol in an ideal world. Phantom types are used to statically check that the reified form of the types is in sync with the one declared in interface.mli The benefit of this commit is that changing the protocol is easier: one changes the types in interface.mli and lets ocamlc spot all the places that needs to be modified. This is a necessity if one plays with the protocol very often, like in my Paral-ITP branch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16438 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-09When asked for a SearchAbout request, Coq now returns a more preciseppedrot
name, that is, a pair of a smart qualified name and the missing prefix needed to recover the full path. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15787 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12A new status Unsafe in Interface. Meant for commands such as Admitted.aspiwack
Currently : - only Admitted uses the Unsafe return status - the status is ignored in coqtop - Coqide sees the status but apparently doesn't use it for colouring (I'm not sure why, but then again, it's not as if I understood coqide's code or anything) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15610 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-10Adapting the IDE interface with the focussed display.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15579 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-29Now CoqIDE separates answer and messages. This should hopefullyppedrot
be backward compatible... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15501 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-23Moving logging level to Interface.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15486 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-13Added a SearchAbout-like primitive in coqtop interface.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15313 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-13Added an interface primitive to ask coqtop for its internal versions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15312 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-11Slightly modified the coqtop interface by adding an identifier inppedrot
goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15303 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Added an interface call to exit Coqtop nicely.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15263 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-12lib directory is cut in 2 cma.pboutill
- Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:42:57 +0000