| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2011-01-14 | - simple backward compatible change to invoke a function to | Hendrik Tews | |
| compute the command line arguments for a proof assistant | |||
| 2011-01-12 | Add preliminary support for multiple files for coq. | Hendrik Tews | |
| The following points are implemented already: - recompile either via an external command (make) or let ProofGeneral handle everything internally - complete dependency tracking and recompilation for coq files in internal mode - support for extending the LoadPath: does almost work, even if specified file-locally - move back to clean state if recompilation fails There are the following known problems: - coq-load-path extensions are not retracted - fails on partially qualified library names | |||
| 2011-01-12 | Set version tag for new release. | David Aspinall | |
| 2011-01-12 | Remove comment | David Aspinall | |
| 2011-01-12 | Type-check on integer settings | David Aspinall | |
| 2011-01-12 | Fix quoting in 'float patch. | David Aspinall | |
| 2011-01-11 | Add additional support for pgipfloat type | David Aspinall | |
| 2011-01-11 | 'float -> 'number | David Aspinall | |
| 2011-01-11 | defpacustom: support for 'float type | David Aspinall | |
| 2010-12-16 | Set version tag for new release. | David Aspinall | |
| 2010-12-16 | Patch to add pgipfloat type. | David Aspinall | |
| 2010-12-10 | Set version tag for new release. | David Aspinall | |
| 2010-11-25 | Set version tag for new release. | David Aspinall | |
| 2010-11-03 | Set version tag for new release. | David Aspinall | |
| 2010-10-11 | proof-debug: fiddle with warning levels to make *PG Debug* buffer appear, ↵ | David Aspinall | |
| set it in help mode. | |||
| 2010-10-11 | proof-segment-up-to-using-cache: improve attempt | David Aspinall | |
| 2010-10-11 | Set version tag for new release. | David Aspinall | |
| 2010-10-11 | Use parser cache by default. | David Aspinall | |
| 2010-10-11 | Set version tag for new release. | David Aspinall | |
| 2010-10-11 | unicode-tokens-enable: turn on by default in Isabelle | David Aspinall | |
| 2010-10-10 | Set version tag for new release. | David Aspinall | |
| 2010-10-10 | Set version tag for new release. | David Aspinall | |
| 2010-10-10 | Add a master debug flag, and disable debug output ordinarily. | David Aspinall | |
| 2010-10-10 | Fix debug message format | David Aspinall | |
| 2010-10-10 | Updated | David Aspinall | |
| 2010-10-10 | Reenable LEGO since it's included in docs (needed for make magic) | David Aspinall | |
| 2010-10-10 | Disable lego and hol-light by default | David Aspinall | |
| 2010-10-10 | Set version tag for new release. | David Aspinall | |
| 2010-10-10 | pg-span-name: improve docstring. | David Aspinall | |
| proof-complete-buffer-atomic: simplify. Add debug message for parser cache. | |||
| 2010-10-10 | pg-span-context-menu: add doc | David Aspinall | |
| 2010-10-10 | Activate debug message printing into log file | David Aspinall | |
| 2010-10-10 | Fix to last patch. | David Aspinall | |
| 2010-10-10 | proof-assert-electric-terminator: prevent adding terminator if point is ↵ | David Aspinall | |
| after it as well as before, as in PG 3.7. Fixes #371. | |||
| 2010-10-10 | Adjust a comment on proof-shell-mode | David Aspinall | |
| 2010-10-08 | Remove developers note from docstring of togglers | David Aspinall | |
| 2010-10-06 | No compile warning if image-size not available | David Aspinall | |
| 2010-10-04 | Clean up obsolete comments | David Aspinall | |
| 2010-10-04 | Fixes in strings/comments from Erik Martin-Dorel | David Aspinall | |
| 2010-10-04 | Set version tag for new release. | David Aspinall | |
| 2010-10-04 | Move mouse button bindings to avoid clashes (patch from Trac #365, Erik ↵ | David Aspinall | |
| Martin-Dorel) | |||
| 2010-10-01 | Set version tag for new release. | David Aspinall | |
| 2010-10-01 | proof-universal-keys: Add binding for pg-identifier-under-mouse-query. | David Aspinall | |
| 2010-10-01 | Add doc | David Aspinall | |
| 2010-10-01 | proof-script-new-command-advance: add back some indentation attempt | David Aspinall | |
| auto sending: improve messages, bind autosend-running flag lexically in case of errors query identifier: use history variable, remove key bindings | |||
| 2010-10-01 | Move utility span-make-modifying-removing-span to span.el | David Aspinall | |
| 2010-10-01 | Add explicit 'invisible flag on the action list for invisible commands. | David Aspinall | |
| This means that certain display actions will always be avoided for non-scripting commands (i.e., hints, anything in `proof-shell-error-or-interrupt-hook'). | |||
| 2010-10-01 | proof-shell-handle-error-or-interrupt-hook: only run if ordinary scripting ↵ | David Aspinall | |
| input (no non-nil flags in queue) | |||
| 2010-10-01 | Adjust handling of insertion of newlines before next command. | David Aspinall | |
| 2010-10-01 | proof-next-command-on-new-line: add this new internal flag | David Aspinall | |
| 2010-10-01 | proof-script-command-separator: remove; proof-one-command-per-line becomes ↵ | David Aspinall | |
| prover specific. | |||
