aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Collapse)AuthorAge
* Fixing ml-doc.Gravatar Pierre-Marie Pédrot2014-05-01
|
* Fix broken commit 2bcb2cb.Gravatar Guillaume Melquiond2014-04-28
|
* Fix incorrect syntax highlighting after the Goal command.Gravatar Guillaume Melquiond2014-04-28
|
* CoqIDE: options for syntax highlightingGravatar Enrico Tassi2014-04-10
|
* CoqIDE: removing a timer may raise an exceptionGravatar Enrico Tassi2014-04-10
|
* nanoPG: when the cursor moves, scroll to make it appear on screenGravatar Enrico Tassi2014-04-09
|
* nanoPG: takeover keypress only when text view has focusGravatar Enrico Tassi2014-04-09
|
* Allowing proof view to be detached in CoqIDE.Gravatar Pierre-Marie Pédrot2014-04-07
|
* Clean up the .merlinGravatar Thomas Refis2014-04-03
| | | | | | | | | | | | | | | | | | | | | | | | | I added a .merlin in ide/ who inherits everything from the root .merlin and also adds the dependency to lablgtk, which I removed from the root file. These way people not working on that part of the code won't get bothered if they don't have that package. I removed the S/B entry for plugins which was useless, indeed there is no ML file in that directory and merlin doesn't scan the subdirectories recursively (as you know). I also removed the S/B entry for checker since most of the files of this directory are also present in kernel and that was the cause of a lot errors on merlin's side (think "inconsistent assumptions"). On top of that, no part of the tree depends on checker (I back that assertion by a grep of the *.d files of the tree) so these lines in the .merlin were actually useless. The only part of the tree where you need to know what's in checker/ is when you are working in checker/ itself, but since merlin automatically adds the directory of the file under edition in its source and load paths nothing else is needed. There might still be problems after this patch, but they should be less of them. Considering my poor knowledge of the codebase there might be other conflicts I have missed.
* CoqIDE: better error reporting for Qed on incomplete proofGravatar Enrico Tassi2014-03-26
|
* nanoPG: better copy/pasteGravatar Enrico Tassi2014-03-13
|
* Stm: smarter delegation policyGravatar Enrico Tassi2014-03-12
| | | | | | | | | | | | | | | | | | | | 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.
* CoqIDE: Errors page gets red if not emptyGravatar Enrico Tassi2014-03-12
|
* CoqIDE: detachable message/error/jobs panesGravatar Enrico Tassi2014-03-12
|
* remove trailing '\r' from file names returned by coqtopGravatar Virgile Prevosto2014-03-06
|
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
| | | | | | | | With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
* Move error and job display to the lower right pane.Gravatar Guillaume Melquiond2014-03-04
|
* Fix syntax highlighting of "Implicit Arguments" for gtksourceview.Gravatar Guillaume Melquiond2014-03-02
|
* CoqIDE: when coqtop misbehaves kill it properly (no zombie)Gravatar Enrico Tassi2014-02-17
|
* [nanoPG]: emacs like copy/pasteGravatar Enrico Tassi2014-02-17
|
* STM + CoqIDE: stop_worker message and UIGravatar Enrico Tassi2014-01-30
|
* STM: tell the user if the master is recomputing states validated by workersGravatar Enrico Tassi2014-01-30
| | | | | | When the worker fails, the master may need to recompute some states the worker has already validates. In this case they are colored accordingly.
* 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: do not unfocus if not needed on errors (closes: 3197)Gravatar Enrico Tassi2014-01-06
|
* nanoPG: compete rewriting with more Emacs/PG like featuresGravatar Enrico Tassi2014-01-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It is not possible to add shortcuts with arbitrary modifiers and to save into a state some data, like the line offset for C-n and the killed text for C-k and C-y. If you see that your favorite Emacs/PG shortcut is missing, please tell me! Currently supported shortcuts: C-_ Undo C-g Esc C-s Search C-e Move to end of line M-e Move to end of sentence M-a Move to beginning of sentence C-n Move to next line C-p Move to previous line C-f Forward char C-b Backward char M-f Forward word M-b Backward word C-k Kill untill the end of line M-d Kill next word M-k Kill until sentence end M-DELBACK Kill word before cursor C-d Delete next character C-y Yank killed text back C-c C-RET Go to C-c C-n Advance 1 sentence C-c C-u Retract 1 sentence C-c C-b Advance C-c C-r Restart C-c C-c Stop C-c C-a C-p Print C-c C-a C-c Check C-c C-a C-b About C-c C-a C-a Search About C-c C-a C-o Search Pattern C-c C-a C-l Locate C-c C-a C-RET match template C-x C-s Save C-x C-c Quit C-x C-f Open
* Paral-ITP: cleanup of command line flags and more conservative defaultGravatar Enrico Tassi2014-01-05
| | | | | | | | | | | | | | | | | | | | | | | | | -async-proofs off the system behaves as in 8.4 -async-proofs lazy proofs are delayed (when possible) but never processed in parallel -async-proofs on proofs are processed in parallel (when possible). The number of workers is 1, can be changed with -async-proofs-j. Extra options to the worker process can be given with -async-proofs-worker-flags. The default for batch compilation used to be "lazy", now it is "off". The "lazy" default was there to test the machinery, but it makes very little sense in a batch scenario. If you process things sequentially, you'd better do them immediately instead of accumulating everything in memory until the end of the file and only then force all lazy computations. The default for -ideslave was and still is "on". It becomes dynamically "lazy" on a per task (proof) basis if the worker dies badly. Note that by passing "-async-proofs on" to coqc one can produce a .vo exploiting multiple workers. But this is rarely profitable given that master-to-worker communication is inefficient (i.e. it really depends on the size of proofs v.s. size of system state).
* CoqIDE: new feedback "incomplete" to signal partial QedGravatar Enrico Tassi2013-12-24
|
* Fix CoqIDE compilation under standard version of lablgtk2Gravatar Enrico Tassi2013-12-11
| | | | We use the win32 specific function only if WIN32 is defined
* Fix CoqIDE on windowsGravatar Enrico Tassi2013-12-10
|
* Ensure locality modifiers are properly highlighted in CoqIDE.Gravatar Guillaume Melquiond2013-12-03
|
* Silence compilation warning by avoiding some deprecated constructs.Gravatar Guillaume Melquiond2013-12-03
|
* CoqIDE: show error message for parsing errorsGravatar Enrico Tassi2013-11-27
|
* Adds a tactic give_up.Gravatar aspiwack2013-11-02
| | | | | | 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
* Adds a shelve tactic.Gravatar aspiwack2013-11-02
| | | | | | 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
* CoqIDE: scroll to the right position if there is an interp errorGravatar gareuselesinge2013-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16962 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: fix coloring bug when jumping back to the first phraseGravatar gareuselesinge2013-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16928 85f007b7-540e-0410-9357-904b9bb8a0f7
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16921 85f007b7-540e-0410-9357-904b9bb8a0f7
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* CoqIDE: do not try to backtrack to a dummy idGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16906 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
* wg_Detachable: move out of wg_CommandGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16903 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wg_Commands: fix warning "widget not within a GtkWindow"Gravatar gareuselesinge2013-10-22
| | | | | | | The constructor was calling indirectly grab_default that requires the widget to be anchored. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16902 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wg_Commands: when detached display the buffer nameGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16901 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
* wg_Commands: smaller icons in tabsGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16897 85f007b7-540e-0410-9357-904b9bb8a0f7
* ideutils: support custom size for stock iconsGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16896 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: make error background configurableGravatar gareuselesinge2013-10-11
| | | | | | #FFCCCC is quite dark on some beamers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16881 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: single underline for errorsGravatar gareuselesinge2013-10-11
| | | | | | | The double underline has some bugs, sometimes the lower line is not correctly cleared. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16875 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 00:45:09 +0000