aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/isar-autotest.el
Commit message (Collapse)AuthorAge
* Use `cl-lib` instead of `cl` everywhereGravatar Stefan Monnier2018-12-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Use lexical-binding in a few files where it was easy. Don't require `proof-compat` when it's not used. * coq/coq-db.el: Use lexical-binding. * coq/coq-system.el: Use lexical-binding. (coq--extract-prog-args): Use concatenated-args rather than recomputing it. * coq/coq.el: Require `span` to silence some warnings. * generic/pg-user.el: Use lexical-binding. (complete, add-completion, completion-min-length): Silence warnings. * generic/pg-xml.el: Use lexical-binding. (pg-xml-string-of): Prefer mapconcat to reduce+concat. * generic/proof-depends.el: Use lexical-binding. (proof-dep-split-deps): Use `push`. * generic/proof-shell.el: Require `span` to silence some warnings. (proof-shell-invisible-command): Don't use lexical-let just to build a wasteful η-redex! * lib/holes.el: Use lexical-binding. Remove redundant :group args. * lib/span.el: Use lexical-binding. (span-read-only-hook): Use user-error. (span-raise): Remove, unused.
* Change (eval-when (compile) ...) to (eval-when-compile ...)Gravatar Clément Pit--Claudel2017-05-05
| | | | This fixes a bunch of compilation warnings
* Remove compile-time calls to proof-ready-for-assistantGravatar Clément Pit--Claudel2017-03-08
| | | | | Compilation used to run in a separate Emacs process for each file, but that's not what happens when installing PG with package.el.
* Fix incorrect assumption that noninteractive == byte-compilingGravatar Clément Pit--Claudel2017-03-08
| | | | | The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't.
* Repair operation with compiled code. Fails with interpreter, see Trac #445Gravatar David Aspinall2012-09-02
|
* Add fix and regression test for Trac #138Gravatar David Aspinall2011-10-17
|
* auto-solve -> auto-solve-direct for Isabelle2011.Gravatar David Aspinall2011-01-31
|
* Add autotest startGravatar David Aspinall2011-01-26
|
* Remove debug messagesGravatar David Aspinall2011-01-25
|
* Fix bug with nested spans, solving #344/#335Gravatar David Aspinall2010-08-27
|
* Clean flag settings for profiling. Add AHundredProofs.Gravatar David Aspinall2010-08-18
|
* Extend testingGravatar David Aspinall2010-08-11
|
* Support custom syntactic fontification.Gravatar David Aspinall2010-08-11
|
* Note completeGravatar David Aspinall2010-08-08
|
* Separate profiling from testingGravatar David Aspinall2010-08-03
|
* Fix compileGravatar David Aspinall2010-08-03
|
* Fix compilationGravatar David Aspinall2010-08-03
|
* Resurrect autotest frameworkGravatar David Aspinall2010-08-03
|
* Fix compile errorsGravatar David Aspinall2009-09-15
|
* Experimental changes to queue several commands at once and to allow ↵Gravatar David Aspinall2009-09-10
| | | | pre-processing of commands when they're queued from script
* Clean whitespaceGravatar David Aspinall2009-09-05
|
* Updated.Gravatar David Aspinall2008-01-16
|
* Remove eval-when, seems unreliableGravatar David Aspinall2007-12-14
|
* Improve loading; these tests are not functioning yetGravatar David Aspinall2007-12-14
|
* Fix commentGravatar David Aspinall2007-02-28
|
* Added simple testing framework (in progress)Gravatar David Aspinall2005-02-13