aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.ml
Commit message (Collapse)AuthorAge
...
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Adding an option to deactivate the progress bar.Gravatar Pierre-Marie Pédrot2015-01-05
|
* CoqIDE: better messagesGravatar Enrico Tassi2014-12-17
|
* Ensuring that ide_slave and stm receive only .v files from CoqIDE.Gravatar Hugo Herbelin2014-12-07
| | | | | | In particular, renouncing to original support for existing non .v files in CoqIDE (hoping it is ok for anyone). Please amend if better to propose.
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
| | | | | | | | | | | It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
* Fixing bug #3404.Gravatar Pierre-Marie Pédrot2014-08-24
|
* Enabling drag & drop on the source view widgets.Gravatar Pierre-Marie Pédrot2014-08-24
| | | | | | Sort of fixes bug #2765, but the file loading is broken and puts coqtop in an inconsistent state, so that even the previous half-working patch was actually not functionning at all. This should be fixed eventually.
* Ide: Drop argument added by MacOS during .app launchGravatar Pierre Boutillier2014-07-22
|
* 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/
* Support dropping files over the coqide window. (Partial fix for bug #2765)Gravatar Guillaume Melquiond2014-06-19
| | | | | | | | The fix is only partial, because dropping files only works over the menu bar, the icon bar, the status bar, and so on. Editable boxes, such as the script widget, catch dnd events, hence preventing this code from working for these drop targets. Some (labl)gtk expert should be able to sort it out.
* CoqIDE: options for syntax highlightingGravatar Enrico Tassi2014-04-10
|
* Allowing proof view to be detached in CoqIDE.Gravatar Pierre-Marie Pédrot2014-04-07
|
* Move error and job display to the lower right pane.Gravatar Guillaume Melquiond2014-03-04
|
* STM + CoqIDE: stop_worker message and UIGravatar Enrico Tassi2014-01-30
|
* CoqIDE: command line for extra coqtop "flags"Gravatar Enrico Tassi2014-01-26
| | | | Like the socket for the OCaml debugger
* CoqIDE: ported to spawnGravatar Enrico Tassi2014-01-26
|
* CoqIDE: new feedback "incomplete" to signal partial QedGravatar Enrico Tassi2013-12-24
|
* Fix CoqIDE on windowsGravatar Enrico Tassi2013-12-10
|
* 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: display in the errors window also the slaves statusGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16900 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: when jumping to an error also move the cursorGravatar gareuselesinge2013-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16842 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: use #present to raise error windowGravatar gareuselesinge2013-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16823 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrace.record_backtrace in CoqIDE tooGravatar gareuselesinge2013-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16822 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
* fix error reporting window size calculationGravatar gareuselesinge2013-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16779 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: new async error reporting window and slaves statusGravatar gareuselesinge2013-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16778 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: show number of proofs being checked in backgroundGravatar gareuselesinge2013-09-12
| | | | | | good test: Nijmegen/QArithSternBrocot/Zaux.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16773 85f007b7-540e-0410-9357-904b9bb8a0f7
* More robust argument setter in CoqIDE. It does not crash anymore on badGravatar ppedrot2013-09-04
| | | | | | arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a (very minimal) Proof General mode to CoqIDEGravatar gareuselesinge2013-08-08
| | | | | | documentation available in the help menu git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16685 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
* Protecting every call to current_term in CoqIDE so that callbackGravatar ppedrot2013-07-27
| | | | | | 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
* Added a way to change dynamically coqtop arguments in CoqIDE.Gravatar ppedrot2013-07-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16636 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: view -> zoom in / out / fitGravatar gareuselesinge2013-05-06
| | | | | | | | 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
* raise UnsafeSuccess -> feedback AddedAxiomGravatar gareuselesinge2013-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renaming SearchAbout into Search and Search into SearchHead.Gravatar herbelin2013-04-17
| | | | | | 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
* 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
* CoqIDE: Including autocompletion in word proposalsGravatar ppedrot2013-02-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16227 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monadification of coqtop queries in CoqIDEGravatar ppedrot2013-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16150 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better handling of escape find in CoqIDEGravatar ppedrot2013-01-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16148 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
* Coqide: use labels for all labelled functionsGravatar letouzey2012-12-08
| | | | | | | | This isn't mandatory, but it's a good practice. For instance it allows to easily locate all ~callback arguments. Cf. warning 6 of OCaml 4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: get rid of threads, use gtk asynchronous i/o insteadGravatar letouzey2012-12-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Threads were only there to handle blocking dialogs with the different coqtops. But programming with threads have drawbacks : complex mutex infrastructure, possible deadlocks, etc. In particular gtk functions are not meant to be called from a thread which isn't the gtk main loop, (unless some gtk mutex have been taken). This seem to pose problem specifically in win32 (and macosx ?), hence the use of the GtkThread.(a)sync hack for scheduling code for execution in the gtk main loop. Instead, we now use the Glib.Io module to install a callback that will be runned when some answer of coqtop is available on the channel. This implies using now a continuation-passing style: for instance, instead of two sequential requests to coqtop, we'll now have the 2nd request inside the callback handling the answer to the 1st request. Remarks: - Also use asynchronous i/o for external commands (editor, coqc, make...). Launching an external editor or browser won't freeze coqide anymore. - Reworked handling of coqtop process, especially when closing them. A responsive coqtop should now hara-kiri immediatly when its input channel is closed. Otherwise we try later a soft kill, then some hard kills if necessary. If nothing work we warns the user. When quitting coqide, all this might induce a small delay (2s at worse). - Be careful now to avoid "long" computations (or blocking i/o) in a coqide function. Experimentally, it seems that loading/saving a .v file is quick enough. If necessary, we could use asynchronous i/o also for writing the .v, but for loading I've no clue. - In the Coqide module, we ensure that the current continuation k will indeed be run at the end thanks to an abstract return type (void = opaque copy of unit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: more cleanup (buffers)Gravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: stylistic improvements in analyzed_view initializerGravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16045 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: cleanup concerning insert_text signalGravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16044 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nicer code around Coq_lexGravatar letouzey2012-12-07
| | | | | | | | | | | Instead of many Coq_lex.delimit_sentence followed by String.sub, we let Coq_lex find the different sentences at once. The offset converter (from byte offset to utf8 offset) is optimized to compute these offsets incrementally instead of re-visiting the whole string buffer again and again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16043 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: missing arg when calling process_next_phraseGravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16041 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: minor cleanup around tag_on_insertGravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16039 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: better removal of the error red tagGravatar letouzey2012-12-07
| | | | | | | | Instead of trying to limit the retag to the visible zone (which may be wrong if the user has scrolled), we remove the red error tag from the whole buffer (this isn't costly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16038 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 06:34:51 +0000