| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
| |
Coq is not going to send any feedback message for the
brute-force canceled jobs, given that the process was killed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16780 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16779 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16778 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16775 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
good test: Nijmegen/QArithSternBrocot/Zaux.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16773 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
arguments.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16761 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Trying to understand if the edit concernes the processed zone
from the begin_user_action callback was a bad idea, the callback
cannot reliably know where the edit takes place (E.g. insert mark
means nothing: one can copy from the insert point but paste elsewhere).
The callbacks delete_range and insert_text do know where the edit is and
can ask coq to backtrack if needed. If coq is busy, the user action is
cancelled (the locked zone cannot be unlocked).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16701 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16700 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
That is pretty tricky, and is not as nice I would like
for to_process text (that is still considered as locked).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16698 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16693 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16687 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
documentation available in the help menu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16685 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Stm contains many TODO items to improve the thing, but it should
be already possible to play with it (but not use it in production).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16684 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16668 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Parenthesis matching on click in all term displays.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16643 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
will not raise an exception if there is no opened tab.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16637 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16636 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Code for printing XML moved from xml_utils.ml to xml_printer.ml
and improved to generate less garbage using Buffer.t systematically.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16480 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
This commit adds zoom facilities that are useful for demos (quickly
increate font size) and daily use (set size so that 80 colums fit
the window width).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16479 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16476 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16457 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16455 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16453 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
| |
I hope I did not forget any place to change.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16322 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16321 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16243 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
cutting XML phrases carelessly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16238 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16237 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
to be untagged whenever trying to modify the first offset.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16230 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16229 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16228 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16227 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16224 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
through a popup.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16223 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16202 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16200 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16151 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16150 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16149 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16148 85f007b7-540e-0410-9357-904b9bb8a0f7
|