aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Collapse)AuthorAge
* STM: report the (structured) goals as XMLGravatar Carst Tankink2014-10-01
| | | | | The leafs of the XML trees are still pretty-printed strings, but this could be refined later on.
* Factored out IDE goal structure.Gravatar Carst Tankink2014-10-01
| | | | | | | | | | | | The more structured goal record type of CoqIDE is also useful for other interfaces (in particular, for PIDE). To support this, the datatype was factored out to the Proof module. In addition, the record gains a type parameter, to allow interfaces to adapt the output to their needs. To accommodate this type, the Proof module also gains the map_structured_proof that takes a Proof.proof and a function on the individual goals (in the context of an evar map) and produces a structured goal based on the goal transformer.
* CoqIDE: new message to print ASTGravatar Enrico Tassi2014-09-29
|
* Remove pointless regex for '""' as the empty string already matches it.Gravatar Guillaume Melquiond2014-09-17
|
* Fix highlighting of "Hint Unfold" and "Hint Rewrite".Gravatar Guillaume Melquiond2014-09-17
|
* Properly highlight the Export keyword.Gravatar Guillaume Melquiond2014-09-17
|
* Fix ambiguous regex in syntax highlighting.Gravatar Guillaume Melquiond2014-09-17
| | | | | | | This fix considerably speeds up syntax highlighting. It also avoids burning 100% CPU when typing long identifiers. Finally, identifiers longer than 20 characters are now properly highlighted, since the stack of the automaton no longer overflows because of them.
* Fix broken syntax highlighting for Coq files using "Proof constr".Gravatar Guillaume Melquiond2014-09-17
| | | | | | See Eqdep_dec.v for instance. Module declarations were not highlighted because the IDE wrongly believed they were used inside an unterminated proof.
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
| | | | | instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions.
* IDE: escape popup text (close: 3600)Gravatar Enrico Tassi2014-09-09
|
* IDE: disable editable text area underline when -debugGravatar Enrico Tassi2014-09-09
| | | | This way a user *can* use coqide with -debug
* toploop plugins taken into account when printing --help (close: 3535)Gravatar Enrico Tassi2014-09-09
| | | | | | | | | | | | | E.g. Coq options are: -I dir look for ML files in dir -include dir (idem) [...] -h, --help print this list of options With the flag '-toploop coqidetop' these extra option are also available: --help-XML-protocol print the documentation of the XML protocol used by CoqIDE
* Add a [Variant] declaration which allows to write non-recursive variant types.Gravatar Arnaud Spiwack2014-09-04
| | | | Just like the [Record] keyword allows only non-recursive records.
* Fixup introduction of coqworkmgrGravatar Pierre Boutillier2014-09-02
|
* coqworkmgrGravatar Enrico Tassi2014-09-02
|
* Coqide prints succesive hyps of the same type on 1 lineGravatar Pierre Boutillier2014-09-01
| | | | | This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses don't respect Barendregt convention".
* "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.
* Quick fix for avoiding infinitely many respawning and Warning "CoqGravatar Hugo Herbelin2014-08-12
| | | | died" when coqtop or coqtopide.cmxs are in inconsistent state.
* 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
|