diff options
author | Stefan Monnier <monnier@iro.umontreal.ca> | 2018-12-18 09:40:59 -0500 |
---|---|---|
committer | Stefan Monnier <monnier@iro.umontreal.ca> | 2018-12-22 08:44:55 -0500 |
commit | f7cc8f1f76baf5e517e51f1db47510ed605064e8 (patch) | |
tree | 188186c199a2176c7708422c60a545d2d1ae914d /generic/proof-syntax.el | |
parent | ebb55c998867fd13f8767a52a9542447347f7dc1 (diff) |
* coq-mode.el: New file to make coq-mode independent from PG
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.
Diffstat (limited to 'generic/proof-syntax.el')
-rw-r--r-- | generic/proof-syntax.el | 27 |
1 files changed, 9 insertions, 18 deletions
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index d494279a..2ba6b7b6 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -197,13 +197,6 @@ it calls `proof-looking-at-syntactic-context'." ;; For font-lock, we treat ,-separated identifiers as one identifier ;; and refontify commata using \{proof-zap-commas}. -(defsubst proof-ids (proof-id &optional sepregexp) - "Generate a regular expression for separated lists of identifiers. -Default is comma separated, or SEPREGEXP if set." - (concat proof-id "\\(\\s-*" (or sepregexp ",") "\\s-*" - proof-id "\\)*")) - - (defun proof-zap-commas (limit) "Remove the face of all `,' from point to LIMIT. Meant to be used from `font-lock-keywords' as a way @@ -228,17 +221,15 @@ this were even more bogus...." ;; fontification function. ;; -(eval-after-load "font-lock" -'(progn -(defadvice font-lock-fontify-keywords-region - (before font-lock-fontify-keywords-advice (beg end &optional loudly)) - "Call proof assistant specific syntactic region fontify. -If it's bound, we call <PA>-font-lock-fontify-syntactically-region." - (when (and proof-buffer-type - (fboundp (proof-ass-sym font-lock-fontify-syntactically-region))) - (funcall (proof-ass-sym font-lock-fontify-syntactically-region) - beg end loudly))) -(ad-activate 'font-lock-fontify-keywords-region))) +;; (defadvice font-lock-fontify-keywords-region +;; (before font-lock-fontify-keywords-advice (beg end &optional loudly)) +;; "Call proof assistant specific syntactic region fontify. +;; If it's bound, we call <PA>-font-lock-fontify-syntactically-region." +;; (when (and proof-buffer-type +;; (fboundp (proof-ass-sym font-lock-fontify-syntactically-region))) +;; (funcall (proof-ass-sym font-lock-fontify-syntactically-region) +;; beg end loudly))) +;; (ad-activate 'font-lock-fontify-keywords-region) ;; ;; Functions for doing something like "format" but with customizable |