| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16323 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
|
| |
|
|
|
|
|
|
|
|
|
| |
PrintOpt.set now only updates the state Hashtbl of options,
a PrintOpt.enforce is mandatory to transmit them to coqtop.
This enforce is done for instance by Coq.goals.
The various signal handlers about coqide's buffer are now installed
in session creation, and not anymore via the coqops initializer.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16105 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
Main victim is analyzed_view :
- some unnecessary methods have been killed (hep_for_keyword for instance)
- some other migrated elsewhere (recenter_input, find_next_occurrence, ...)
- analyzed_view is now split in two : fileops (filename, save, revert, ...)
and coqops (process_next_phrase, ...)
Four new files created:
- Sentence (for tag_on_insert and alii)
- FileOps (ex-first-half of analyzed_view)
- CoqOps (ex-second-half of analyzed_view)
- Session (ex-record viewable_script and functions about it)
Also lots of renaming, trying to be shorter (but still meaningful) and
more uniform
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16057 85f007b7-540e-0410-9357-904b9bb8a0f7
|
gareuselesinge
ppedrot
letouzey