Renamed <file>-fontlock to <file>-syntax

6 files changed, 26 insertions, 16 deletions

diff --git a/coq-fontlock.el b/coq-syntax.el
index 9d106d7c..1563bf13 100644
--- a/coq-fontlock.el
+++ b/coq-syntax.el
@@ -1,9 +1,12 @@
-;; coq-fontlock.el Font lock expressions for Coq
+;; coq-syntax.el Font lock expressions for Coq
 ;; Copyright (C) 1997, 1998 LFCS Edinburgh. 
 ;; Author: Thomas Kleymann and Healfdene Goguen
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
 
 ;; $Log$
+;; Revision 1.2  1998/08/11 11:43:13  da
+;; Renamed <file>-fontlock to <file>-syntax
+;;
 ;; Revision 1.14  1998/06/11 12:20:14  hhg
 ;; Added "Scheme" as definition keyword.
 ;;
@@ -63,7 +66,7 @@
 ;;
 ;;
 
-(require 'proof-fontlock)
+(require 'proof-syntax)
 
 ;; ----- keywords for font-lock.
 
@@ -266,4 +269,4 @@
      (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face)
      (list coq-save-with-hole-regexp 2 'font-lock-function-name-face))))
 
-(provide 'coq-fontlock)
+(provide 'coq-syntax)
diff --git a/coq.el b/coq.el
index 90cef476..b24d4d21 100644
--- a/coq.el
+++ b/coq.el
@@ -3,6 +3,9 @@
 ;; Author: Healfdene Goguen and Thomas Kleymann
 
 ;; $Log$
+;; Revision 2.0  1998/08/11 11:39:20  da
+;; Renamed <file>-fontlock to <file>-syntax
+;;
 ;; Revision 1.29  1998/06/10 11:42:06  hhg
 ;; Added coq-init-syntax-table as function to initialize syntax entries
 ;; particular to coq.
@@ -138,7 +141,7 @@
 ;; New structure to share as much as possible between LEGO and Coq.
 ;;
 
-(require 'coq-fontlock)
+(require 'coq-syntax)
 (require 'outline)
 (require 'proof)
 (require 'info)
diff --git a/lego-fontlock.el b/lego-syntax.el
index 437c4906..8b3ac7f7 100644
--- a/lego-fontlock.el
+++ b/lego-syntax.el
@@ -1,11 +1,12 @@
-;; lego-fontlock.el Font lock expressions for LEGO
+;; lego-syntax.el Font lock expressions for LEGO
 ;; Copyright (C) 1994, 1995, 1996, 1997 LFCS Edinburgh. 
 ;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequeira
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
 
-;; should perhaps be called lego-syntax instead of lego-fontlock
-
 ;; $Log$
+;; Revision 1.2  1998/08/11 11:43:14  da
+;; Renamed <file>-fontlock to <file>-syntax
+;;
 ;; Revision 1.6  1998/07/27 15:39:53  tms
 ;; Supports official LEGO release 1.3
 ;;
@@ -36,7 +37,7 @@
 ;;
 
 
-(require 'proof-fontlock)
+(require 'proof-syntax)
 
 ;; ----- keywords for font-lock.
 
@@ -123,4 +124,4 @@
      (list lego-goal-with-hole-regexp 2 'font-lock-function-name-face)
      (list lego-save-with-hole-regexp 2 'font-lock-function-name-face))))
      
-(provide 'lego-fontlock)
+(provide 'lego-syntax)
diff --git a/proof-indent.el b/proof-indent.el
index c380a9c3..bb42f462 100644
--- a/proof-indent.el
+++ b/proof-indent.el
@@ -4,8 +4,7 @@
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
 
 (require 'cl)
-(require 'proof-fontlock)
-;; proof-fontlock ought to be renamed to proof-syntax
+(require 'proof-syntax)
 
 (defvar proof-stack-to-indent nil
   "Prover-specific code for indentation.")
diff --git a/proof-fontlock.el b/proof-syntax.el
index 6d2bd51f..56eae4b4 100644
--- a/proof-fontlock.el
+++ b/proof-syntax.el
@@ -1,9 +1,12 @@
-;; proof-fontlock.el Generic font lock expressions
+;; proof-syntax.el Generic font lock expressions
 ;; Copyright (C) 1997 LFCS Edinburgh. 
 ;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequiera
 ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
 
 ;; $Log$
+;; Revision 1.2  1998/08/11 11:43:14  da
+;; Renamed <file>-fontlock to <file>-syntax
+;;
 ;; Revision 1.8  1998/06/10 11:45:12  hhg
 ;; Changed "\\s " to "\\s-" in proof-id as whitespace pattern.
 ;;
@@ -41,6 +44,7 @@
 
 (require 'font-lock)
 
+;;; FIXME: change this to proof-
 (defun ids-to-regexp (l)
   "transforms a non-empty list of identifiers `l' into a regular
   expression matching any of its elements"
@@ -136,4 +140,4 @@
 		   '(proof-zap-commas-region))))
 
 
-(provide 'proof-fontlock)
+(provide 'proof-syntax)
diff --git a/proof.el b/proof.el
index 7522d8fc..802078ae 100644
--- a/proof.el
+++ b/proof.el
@@ -16,7 +16,7 @@
 (cond ((fboundp 'make-extent) (require 'span-extent))
       ((fboundp 'make-overlay) (require 'span-overlay))
       (t nil))
-(require 'proof-fontlock)
+(require 'proof-syntax)
 (require 'proof-indent)
 (require 'easymenu)
 
@@ -803,7 +803,8 @@
    ((string-match proof-shell-interrupt-regexp string)
     'interrupt)
 
-   ((string-match proof-shell-abort-goal-regexp string)
+   ((and proof-shell-abort-goal-regexp
+	 (string-match proof-shell-abort-goal-regexp string))
     (setq proof-shell-delayed-output (cons 'insert "\n\nAborted"))
     ())
 	 
@@ -835,7 +836,6 @@
     (funcall (cdr proof-shell-process-output-system-specific)
 	     cmd string))
 
-
    (t (setq proof-shell-delayed-output (cons 'insert string)))))
          
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;