* 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.

1 files changed, 18 insertions, 15 deletions

diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 095b108c..4b5f2e4a 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -1,4 +1,4 @@
-;; isar-syntax.el Syntax expressions for Isabelle/Isar
+;; isar-syntax.el Syntax expressions for Isabelle/Isar  -*- lexical-binding:t -*-
 ;; Copyright (C) 1994-2004, 2009, 2010 LFCS Edinburgh.
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
@@ -364,18 +364,18 @@ matches contents of quotes for quoted identifiers.")
 ;; font-lock syntactic fontification
 
 ;; adapted from font-lock.el in GNU Emacs 23.1.1
-(defun isar-font-lock-fontify-syntactically-region 
-  (start end &optional loudly ppss)
-  "Put proper face on each string and comment between START and END.
-START should be at the beginning of a line."
-  (let ((comment-end-regexp
-	 (replace-regexp-in-string "^ *" "" comment-end))
-        state beg)
-    (if loudly (message "Fontifying %s... (syntactically...)" (buffer-name)))
-    (goto-char start)
-    ;;
-    ;; Find the `start' state.
-    (setq state (or ppss (syntax-ppss start)))
+;; FIXME: Why not use the built-in syntactic fontification?
+(defun isar-font-lock-fontify-syntactically-region
+  (end) ;; (start end &optional loudly ppss)
+  "Put proper face on each string and comment between point and END."
+  (let (;; (comment-end-regexp
+	;;  (replace-regexp-in-string "^ *" "" comment-end))
+        (start (point))
+        ;; Find the start state.
+        (state (syntax-ppss))
+        beg)
+    (if font-lock-verbose ;; loudly
+        (message "Fontifying %s... (syntactically...)" (buffer-name)))
     ;;
     ;; Find each interesting place between here and `end'.
     (while
@@ -395,13 +395,16 @@ START should be at the beginning of a line."
 	      (put-text-property beg (point) 'face font-lock-comment-face))))
 	  (< (point) end))
       (setq state (parse-partial-sexp (point) end nil nil state
-				      'syntax-table)))))
+				      'syntax-table))))
+  ;; Job is done, return to font-lock-keywords that there's no match.
+  nil)
 
 ;; font-lock keywords fontification
 
 (defvar isar-font-lock-keywords-1
   (list
-   (cons 'isar-match-nesting                               'font-lock-preprocessor-face)
+   (list #'isar-font-lock-fontify-syntactically-region)
+   (cons #'isar-match-nesting                               'font-lock-preprocessor-face)
    (cons (isar-ids-to-regexp isar-keywords-minor)          'font-lock-type-face)
    (cons (isar-ids-to-regexp isar-keywords-control)        'proof-error-face)
    (cons (isar-ids-to-regexp isar-keywords-diag)           'proof-tacticals-name-face)