aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Collapse)AuthorAge
* CoqIDE: fixing parsing of bullets and brackets even at end of file.Gravatar Hugo Herbelin2014-08-05
|
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
|
* Coqide: check_connection now also checks correct loading of coqide plugin +Gravatar Hugo Herbelin2014-08-05
| | | | reports errors also from stderr.
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
|
* Coqide: annoying popups with GTK errors only in debug modeGravatar Enrico Tassi2014-08-05
|
* Make MacStore like coqide moreGravatar Pierre Boutillier2014-07-24
| | | | including bigger icons
* Ide: Drop argument added by MacOS during .app launchGravatar Pierre Boutillier2014-07-22
|
* the art of forgetting new files during rebase -iGravatar Pierre Boutillier2014-07-22
|
* A makefile rule to build bin/CoqIDE_$VERSION.app macOS bundleGravatar Pierre Boutillier2014-07-22
| | | | The created bundle contains only coqide and gtk (no coqtop, no stdlib)
* Coqide use '(diraname MYSELF)/coqtop' as coqtop only if this file existsGravatar Pierre Boutillier2014-07-22
|
* CoqIDE: on win32 the old interrputer code (SIGINT) is still neededGravatar Enrico Tassi2014-07-10
|
* Little coqide bug, when coqtop outputs empty lines, as e.g. when calling ↵Gravatar Hugo Herbelin2014-06-30
| | | | coqide --help.
* Coq_makefile takes advantages of -I -Q -R cleanupGravatar Pierre Boutillier2014-06-30
|
* Coq_makefile: -extra[-phony] correction + docGravatar Pierre Boutillier2014-06-30
|
* 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.
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 14:08:21 +0000