aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/session.ml
Commit message (Collapse)AuthorAge
* Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
|
* [ide] Set Stateid in query pane.Gravatar Emilio Jesus Gallego Arias2017-04-20
| | | | | | We again remove another user of Stateid.dummy. However, we need to adapt the protocol so `Coq.query` takes the `route_id` and we can redirect the output properly to the subwindow.
* Do not stop propagation of signals when Coq is busy (bug #3941).Gravatar Guillaume Melquiond2016-09-28
| | | | | | | | When inserting a character in an already processed buffer, a message is sent to Coq so that the proof is backtracked and the character is inserted. If a second character is inserted while Coq is still busy with the first message, the action is canceled, but the signal is no longer dropped so that the second character is properly inserted.
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-21
|\
| * CoqIDE: STOP button also stops workers (fix #4542)Gravatar Enrico Tassi2016-02-19
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Replacing old-style preferences in CoqIDE.Gravatar Pierre-Marie Pédrot2015-08-26
| | | | | | | | | | There is no remaining global preference record anymore, every preference is now defined in the new event-based style.
* | Using the new preference mechanism for colors in CoqIDE.Gravatar Pierre-Marie Pédrot2015-08-16
| | | | | | | | | | A lot of legacy code has been removed in the process in favour of signal-based interactions.
* | Turning CoqIDE preferences into new style.Gravatar Pierre-Marie Pédrot2015-08-16
|/ | | | | Some old style references remain because all type converters are not implemented yet.
* coqide: don't require ocaml >= 4Gravatar Enrico Tassi2015-05-29
|
* Jump to error line in CoqIDE grabs focus of the textview.Gravatar Pierre-Marie Pédrot2015-05-26
|
* CoqIDE columns in error and job panels can be sorted.Gravatar Pierre-Marie Pédrot2015-05-25
| | | | This grants wish #4194.
* CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)Gravatar Enrico Tassi2015-04-02
| | | | | | | | | | | No "read-only" terminator. If no terminator is present the UI complains. If the terminator is different, STM warns but continues. The STM warns that the "check the document" button will not honor the terminator change, and what to do to avoid that. Technically, one cannot turn (a posteriori) an axiom into a theorem and vice versa. Could be done, but not with a small patch.
* Fixing bug #4073.Gravatar Pierre-Marie Pédrot2015-02-20
|
* Trying to fix bug #3930.Gravatar Pierre-Marie Pédrot2015-02-13
| | | | | | Instead of setting the last modified part of the text to be the insert point, we register all modifications to the buffer between to user actions and take the last modified point to be the least offset of all those modifications.
* Tentative fix for CoqIDE randomly dropping deletions.Gravatar Pierre-Marie Pédrot2015-02-12
| | | | | | We make the deletion callback not to regenerate a task id, as the insertion callback does. I can't find a particular reason for this dissymetry, and it was indeed causing trouble.
* Focussing on message view in CoqIDE when a message is pushed.Gravatar Pierre-Marie Pédrot2015-02-12
| | | | Also fixes bug #4030.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Implementing a segment-viewer in CoqIDE.Gravatar Pierre-Marie Pédrot2015-01-05
| | | | | | | This allows a nifty display of the current state of the document through a dedicated progress bar. Also closes bug #3764.
* CoqIDE: cleanup jobs window on worker deathGravatar Enrico Tassi2014-12-17
|
* IDE: disable editable text area underline when -debugGravatar Enrico Tassi2014-09-09
| | | | This way a user *can* use coqide with -debug
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
|
* Allowing proof view to be detached in CoqIDE.Gravatar Pierre-Marie Pédrot2014-04-07
|
* CoqIDE: Errors page gets red if not emptyGravatar Enrico Tassi2014-03-12
|
* CoqIDE: detachable message/error/jobs panesGravatar Enrico Tassi2014-03-12
|
* Move error and job display to the lower right pane.Gravatar Guillaume Melquiond2014-03-04
|
* CoqIDE: new feedback "incomplete" to signal partial QedGravatar Enrico Tassi2013-12-24
|
* CoqIDE: always retag on insertGravatar gareuselesinge2013-10-22
| | | | | | | This should fix Arnaud's bug (reported by private email) that makes coq eat two sentences at once (and process only the first one). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16907 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wg_Find: regex + case insensitive find/replace supportGravatar gareuselesinge2013-10-22
| | | | | | It uses Str, hence it also supports captures \(..\) and \1 .. \n git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16904 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: error reporting fixedGravatar gareuselesinge2013-10-10
| | | | | | | | | Many things were wrong. Error tags were deleted by mistake, the screen was recentered on `INSERT using the wrong function (that cause some horizontal scrolling even if it was not needed), the cursor not advanced to the end of the wrong sentence. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16874 85f007b7-540e-0410-9357-904b9bb8a0f7
* wg_Command: detachable, less "from the 80s", query paneGravatar gareuselesinge2013-09-30
| | | | | | | | | | | | | | | | | - Tabs have labels derived from the query (e.g. "About eq_ind" will have "eq_ind" as its label, that is better than "Page 1" ;-) - Tabs have a [x] close icon - Icon to create a new tab in in the notebook - Dispotically grab the F1 key to open/close the query pane (alt-esc is grabbed by windows managers these days) - Esc hides the query pane (like the search pane) - F1 puts a detached query pane in front - Tab switches from the combo-box to the entry on its right - Detaching is taken-over, and the query pane is reparented in a regular window that can be resized - A detached query pane can be put back by closing the window git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16817 85f007b7-540e-0410-9357-904b9bb8a0f7
* wg_Session: fix copy/paste of tagged textGravatar gareuselesinge2013-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16816 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE ported to the revides protocolGravatar gareuselesinge2013-09-30
| | | | | | | | | | | - the zone to be edited is now between the marks start_of_input and stop_of_input - when -debug is given, the edit zone is underlined - the cmd_stack is focused/unfocused according to the new protocol - read only tag resurrected and used to block the "Qed" ending a focused zone git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16814 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: fixed detection of edits in the locked zoneGravatar gareuselesinge2013-08-20
| | | | | | | | | | | | | 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
* Automatic backtracking if locked zone is editedGravatar gareuselesinge2013-08-11
| | | | | | | 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
* Coqide ported to STMGravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | | | 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
* Coqide: Globalization feedback (proof of concept)Gravatar gareuselesinge2013-04-25
| | | | | | | | | | | | | | | | | | | | 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
* Coqide: new feedback mechanism for structured contentGravatar gareuselesinge2013-04-25
| | | | | | | | | | | | | | | | | 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
* Better encapsulation of MessageViewGravatar ppedrot2013-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing an annoying bug in CoqIDE which causes the very first lineGravatar ppedrot2013-02-20
| | | | | | 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
* Coqide: cleaner Coq.PrintOpt and session creationGravatar letouzey2012-12-19
| | | | | | | | | | | 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
* Coqide: some more refactoring to lighten coqide.mlGravatar letouzey2012-12-10
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