aboutsummaryrefslogtreecommitdiff
path: root/coq
AgeCommit message (Collapse)Author
2012-06-28Fixed some small bugs in coq indentation.Pierre Courtieu
2012-06-28Complete rework of the indentation mechanism using smie. The firstPierre Courtieu
version of smie indentation code was a good first try but this one is much faster and cleaner. All desambiguations are done in the lexers, it is still a bit slow on large proofs. Some bugs remain to be fixed.
2012-06-19Simplified file variables code.Pierre Courtieu
2012-06-14Fix a bug in coq indet code when at the beginning of a buffer.Pierre Courtieu
2012-06-11Trying to minimize the slowness of indentation when no "Proof." isPierre Courtieu
given. Seems to work.
2012-06-10Fixing indentation details for coq. All known bugs seems fixed.Pierre Courtieu
2012-06-10Fixing indentation details for coq.Pierre Courtieu
2012-06-10Still fixing indentation details for coq.Pierre Courtieu
2012-06-10Still fixing indentation (operator precedences) details for coq.Pierre Courtieu
2012-06-10Still fixing indentation details for coq.Pierre Courtieu
2012-06-09Made a small change in generic code about the setting ofPierre Courtieu
comment-start-skip: if it is already set then proof-script should not change it. Ultimately if David approves we should moreover fix the setting itself which is bugged. coq-mode now sets this variable by itself.
2012-06-08Indentation is a bit more accurate.Pierre Courtieu
2012-06-07Fix a bug of indentation in presence of comment. Probably due to a badPierre Courtieu
set of rules. Fixed by cleaning rules.
2012-06-07Fix indentation of dependent match clauses (as ... in ... return ...).Pierre Courtieu
+ bug fixes.
2012-06-06Fixing a bug with the indentation of qualified names.Pierre Courtieu
2012-06-06Trying to fix some minor indentation bugs with infox operators.Pierre Courtieu
2012-06-04One more fix for indentation.Pierre Courtieu
2012-06-04Fixing indentation (same bug than 2 previous commits). this time it seems ok.Pierre Courtieu
2012-06-04Fixing the last fix on indentation. Still not perfect.Pierre Courtieu
2012-06-03Fix a bug of indentation.Pierre Courtieu
2012-05-31Fix of a bug. coq id can start with underscore.Pierre Courtieu
2012-05-29- erase invalid coq-load-path entry format '("dir")Hendrik Tews
- check if coq-load-path is well-formed - update documentation
2012-05-26another hide additional subgoals fixHendrik Tews
2012-05-24fix "Hide Additional Subgoals" for coq 8.4betaHendrik Tews
2012-05-09fix typo + add one missing cvsignoreHendrik Tews
2012-02-13fix coqdep error recognitionHendrik Tews
2012-02-10Fixed an ineficiency in comment detection.Pierre Courtieu
2012-02-01Cleaning some code.Pierre Courtieu
2012-02-01Quick fix of a regression introduced by my last commit. Looking for aPierre Courtieu
better fix.
2012-02-01Fixed command end recognition in presence of operators of the form .+Pierre Courtieu
+. is not accepted yet.
2012-01-18Fixed a small bug in indentation (ter repetita). Bullets are indentedPierre Courtieu
correctly provided that the precedence - > + > * is respected.
2012-01-18Fixed a small bug in indentation (bis repetita).Pierre Courtieu
2012-01-18Fixed a small bug in indentation.Pierre Courtieu
2012-01-10Support proof-shell-interactive-prompt-regexp, ref Trac #430David Aspinall
2012-01-09proof-shell-start-goals-regexp: shy match to avoid introducing match groupDavid Aspinall
2012-01-04* fix case where some existential is instantiated with the last proof commandHendrik Tews
* protocol change - rename proof-complete into proof-finished and add existential info - add proof-complete message
2012-01-03hide the dependent evars lineHendrik Tews
2012-01-03merge ProofTreeBranch into main trunk:Hendrik Tews
- add support for proof-tree displays (currently Coq only) - new file generic/proof-tree.el contains generic code - Coq specific code has been added to coq/coq.el Changes to existing Proof General functions: - proof-shell-exec-loop and proof-shell-filter-manage-output call proof-tree display functions, when the proof-tree display is on - proof-shell-exec-loop returns t if proof-action-list is empty _or_ contains only items for updating the proof-tree - proof-shell-should-be-silent returns nil when the proof-tree display is on - coq-last-prompt-info, coq-last-prompt-info-safe return as additional 4th element the name of the current proof
2011-12-27Extra testDavid Aspinall
2011-12-27TypoDavid Aspinall
2011-12-16Fixed some regexp. One for goal closing detection and one forPierre Courtieu
understanding the new message about dependent evars (the two window mode was bugged).
2011-12-16Adapting coq syntax recognition to the future v8.4 behavior of bulletsPierre Courtieu
(stand-alone commands), which is different of the experiments made until now in coq/trunk.
2011-12-07- protect proof-shell-handle-delayed-output against the case whereHendrik Tews
proof-shell-end-goals-regexp is defined but does not match - add coq setting for hiding additional subgoals
2011-12-06ensure optim-resp-window does not change the current bufferHendrik Tews
2011-12-05Applied a patch from Tom Prince which makesPierre Courtieu
coq-update-minor-mode-alist behavior more acceptable.
2011-11-15Quick stab at support for switching to proof shell when interactive support ↵David Aspinall
expected, see Trac #430
2011-11-14Small fixes to coq smie indentation.Pierre Courtieu
2011-11-11Fixed coq smie indentation.Pierre Courtieu
2011-11-10Fixed coq smie indentation.Pierre Courtieu
2011-11-10fixed some small bugs in coq indentation smie code.Pierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 02:20:44 +0000