aboutsummaryrefslogtreecommitdiffhomepage
path: root/isar/isar-syntax.el
Commit message (Collapse)AuthorAge
* * coq-mode.el: New file to make coq-mode independent from PGGravatar Stefan Monnier2018-12-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Move the part of coq.el that is not specific to ProofGeneral into coq-mode.el to make `coq-mode` into a major mode that can work without PG. * coq/coq-mode.el: New file, with code extracted from coq.el. (coq-use-pg): New var. (coq-near-comment-region): Complete rewrite. * Makefile.devel (autoloads): Add `coq` to the scanned subdirectories. * generic/proof-autoloads.el: Regenerate. * generic/proof-site.el: Don't override pre-existing major-mode definitions. * coq/coq-syntax.el (coq-init-syntax-table): Delete function. Setup the syntax-table while loading coq-mode.el instead. * coq/coq-system.el (coq-prog-name, get-coq-library-directory) (coq-library-directory, coq-tags): Move to coq-mode.el. * coq/coq.el: Set proof-assistant when loaded. (coq-may-use-prettify, coq-outline-regexp) (coq-outline-heading-end-regexp, coq-mode) (coq-prettify-symbols-alist, coq-fill-paragraph-function) (coq-adaptive-fill-function): Move to coq-mode.el. (coq-shell-mode-syntax-table, coq-response-mode-syntax-table) (coq-goals-mode-syntax-table): Just reuse the already setup coq-mode-syntax-table... (coq-shell-mode-config, coq-goals-mode-config, coq-response-config): ... instead of calling coq-init-syntax-table. (coq-get-comment-region): Delete, not used any more. (coq-pg-mode-map): New var. Move top-level keymap setup here. (coq-pg-setup): Rename from coq-mode-config. Move all the non-PG specific settings to coq-mode. * generic/proof-script.el (proof-mode): Simplify call to proof-splash-message since it does the same extra tests internally. (proof-config-done-related): Don't touch font-lock-defaults if the mode doesn't provide any font-lock-defaults. * isar/isar-syntax.el: Use lexical-binding. (isar-font-lock-fontify-syntactically-region): Make it callable from font0lock-keywords. (isar-font-lock-keywords-1): Call isar-font-lock-fontify-syntactically-region. * generic/proof-syntax.el (font-lock-fontify-keywords-region): Remove advice. (proof-ids): Remove, unused. * lib/bufhist.el (bufhist-erase-buffer): Don't let-bind after-change-functions. * generic/pg-pbrpm.el (pg-pbrpm-auto-select-around-point): Fix one more left-over cl.el use. * generic/proof-utils.el (proof-with-script-buffer): Add edebug spec.
* 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.
* Fix colours for dark backgroundsGravatar David Aspinall2015-03-05
|
* clarified isar-improper-regexp -- "prems" is already reported as legacy by ↵Gravatar Makarius Wenzel2011-08-31
| | | | the prover (after Isabelle2011);
* generalized font-lock regexps: isar-text allows any non-control characters ↵Gravatar Makarius Wenzel2011-07-06
| | | | to be marked up (e.g. notation for "free" and "skolem" variables after Isabelle2011);
* Replace proof-boring-face -> isabelle-quote-face, reported onGravatar David Aspinall2011-05-05
| | | | Isabelle-users list by Peter Lammich.
* some attempts to indent 'notepad' 'begin' ... 'end' like a proof body;Gravatar Makarius Wenzel2010-12-08
|
* iasbelle-string-face: Remove italic from defaults becauseGravatar David Aspinall2010-08-19
| | | | | STIXRegular doesn't include italic variants of symbols, resulting in empty glyphs appearing on Mac OS X
* isabelle-quote-face: add this face to customize vanishing quotesGravatar David Aspinall2010-08-11
|
* Experiment with default string font being italic, to match STIX italic.Gravatar David Aspinall2010-08-11
|
* Support custom syntactic fontification.Gravatar David Aspinall2010-08-11
|
* isabelle-string-face: switch to a more traditional greenGravatar David Aspinall2010-08-11
| | | | (strings are brown, but logic is green)
* Fix compile and spellingGravatar David Aspinall2010-08-09
|
* isabelle-string-face: introduce custom string colour as font lock default is ↵Gravatar David Aspinall2010-08-04
| | | | terrible
* Fix for matching names in regexps, restores behaviour of name-aware code ↵Gravatar David Aspinall2010-08-02
| | | | such as imenu.
* isar-ids-to-regexp: regexp-opt with 'words arg (non-shy matching insideGravatar David Aspinall2009-12-01
| | | | | | \< \>) appears to work on Emacs 22, hopefully repairing http://proofgeneral.inf.ed.ac.uk/trac/ticket/300. Also replace proof-splice-separator -> mapconcat builtin.
* define isar-pr as load-time constant;Gravatar Makarius Wenzel2009-11-24
|
* Use ProofGeneral.pr if available. See Trac #292.Gravatar David Aspinall2009-11-23
|
* tvar font-lock: allow more than one ? (as in inference parameter ??'a);Gravatar Makarius Wenzel2009-11-21
|
* named entity needed for goal-with-holeGravatar David Aspinall2009-10-14
|
* Remove fume settingsGravatar David Aspinall2009-10-14
|
* Start using new parser, adjusting isar-any-command-regexp.Gravatar David Aspinall2009-10-03
|
* Documentation.Gravatar David Aspinall2009-09-29
|
* Add pr to print state in case of linear_undo. See Trac #292.Gravatar David Aspinall2009-09-26
| | | | | Still not ideal: when there is no proof state, we'd prefer that an empty goal screen is displayed.
* isar-outline-heading-alist: fix list formatGravatar David Aspinall2009-09-14
|
* isar-outline-heading-alist: fix list formatGravatar David Aspinall2009-09-14
|
* isar-outline-heading-alist: fix structureGravatar David Aspinall2009-09-14
|
* Improve support for outline mode: additional headings and sublevel supportGravatar David Aspinall2009-09-14
|
* Support linear_undo. Add minimal font-lock for readability in *isabelle*.Gravatar David Aspinall2009-09-09
|
* Clean whitespaceGravatar David Aspinall2009-09-05
|
* Remove proof-no-commandGravatar David Aspinall2009-09-04
|
* output-font-lock-keywords: remove unnecessary bracketsGravatar David Aspinall2009-09-03
|
* Fix font-lock output keywords for tvars starting ?'Gravatar David Aspinall2009-09-03
|
* First attempt at command wrapping (see ↵Gravatar David Aspinall2009-08-18
| | | | http://proofgeneral.inf.ed.ac.uk/trac/ticket/199)
* isar-syntactic-context: tweak (still not perfect, loses between "--" and ↵Gravatar David Aspinall2009-08-17
| | | | string start)
* isar-syntactic-context: fix calls to re-search-backwardGravatar David Aspinall2009-08-17
|
* isar-syntactic-context: modify proof-looking-at-syntactic-context to allowGravatar David Aspinall2009-08-17
| | | | recognition of terminating comment strings.
* isar-output-font-lock-keywords-1: enable display of ? and ' againGravatar David Aspinall2009-08-14
|
* Do not hide the spurious ASCII characters as it confuses old hands.Gravatar David Aspinall2009-08-14
|
* Remove yank-handler experiment, in favour of buffer-substring-filtersGravatar David Aspinall2009-05-26
|
* isar-strip-output-markup: simple output markup strippingGravatar David Aspinall2009-05-26
| | | | Experiment with font-lock to set yank-handler.
* Hide goals marker start again (Isabelle2009 doesn't markup subgoals)Gravatar David Aspinall2009-05-26
|
* Add highlighting for sendbackGravatar David Aspinall2009-05-26
|
* isar-output-font-lock-keywords-1: simplified regexp for invisible stuff, and ↵Gravatar Makarius Wenzel2009-03-31
| | | | added special "L", special "V";
* Linear undo commandGravatar David Aspinall2008-12-05
|
* Fix by Stephan HoheGravatar David Aspinall2008-09-18
| | | | http://proofgeneral.inf.ed.ac.uk/trac/ticket/236
* Merge changes from Version4Branch.Gravatar David Aspinall2008-07-24
|
* removed obsolete comment;Gravatar Makarius Wenzel2008-07-10
|
* defface: using proof-face-specs makes faces appear on non-X11 window systems ↵Gravatar Makarius Wenzel2008-07-07
| | | | as well;
* isar-undos: fix bug trac #189 introduced by attempt to remove proof-no-command.Gravatar David Aspinall2008-01-29
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 12:40:46 +0000