From 77687d352a1b1bcb5d359b6ee1dd8a29ec3c31ae Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 11 Aug 1998 11:43:14 +0000 Subject: Renamed -fontlock to -syntax --- coq-fontlock.el | 269 ----------------------------------------------------- coq-syntax.el | 272 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ coq.el | 5 +- lego-fontlock.el | 126 ------------------------- lego-syntax.el | 127 +++++++++++++++++++++++++ proof-fontlock.el | 139 ---------------------------- proof-indent.el | 3 +- proof-syntax.el | 143 ++++++++++++++++++++++++++++ proof.el | 6 +- 9 files changed, 550 insertions(+), 540 deletions(-) delete mode 100644 coq-fontlock.el create mode 100644 coq-syntax.el delete mode 100644 lego-fontlock.el create mode 100644 lego-syntax.el delete mode 100644 proof-fontlock.el create mode 100644 proof-syntax.el diff --git a/coq-fontlock.el b/coq-fontlock.el deleted file mode 100644 index 9d106d7c..00000000 --- a/coq-fontlock.el +++ /dev/null @@ -1,269 +0,0 @@ -;; coq-fontlock.el Font lock expressions for Coq -;; Copyright (C) 1997, 1998 LFCS Edinburgh. -;; Author: Thomas Kleymann and Healfdene Goguen -;; Maintainer: LEGO Team - -;; $Log$ -;; Revision 1.14 1998/06/11 12:20:14 hhg -;; Added "Scheme" as definition keyword. -;; -;; Revision 1.13 1998/06/10 11:38:04 hhg -;; Added "Mutual Inductive" as definition keyword. -;; Changed "\\s " into "\\s-" as whitespace pattern. -;; -;; Revision 1.12 1998/06/03 18:01:54 hhg -;; Changed Compute from command to tactic. -;; Added Fix, Destruct and Cofix as tactics. -;; Added Local as goal. -;; -;; Revision 1.11 1998/06/02 15:33:16 hhg -;; Minor modifications to comments -;; -;; Revision 1.10 1998/05/15 16:13:23 hhg -;; Added CoFixpoint and tactics. -;; Changed indentation. -;; -;; Revision 1.9 1998/05/05 14:19:39 hhg -;; Added CoInductive. -;; Made updates to reflect problem with "Definition", which couldn't be -;; used with proof scripts. -;; -;; Revision 1.8 1998/01/15 13:30:17 hhg -;; Added coq-shell-cd -;; Some new fontlocks -;; -;; Revision 1.7 1997/11/26 17:12:55 hhg -;; Incorporated tms's suggestion for simplifying coq-font-lock-keywords-1 -;; -;; Revision 1.6 1997/11/06 16:46:20 hhg -;; Updates to Coq fontlock tables -;; -;; Revision 1.5 1997/10/30 15:58:29 hhg -;; Updates for coq, including: -;; * pbp-goal-command and pbp-hyp-command use proof-terminal-string -;; * updates to keywords -;; * fix for goal regexp -;; -;; Revision 1.4 1997/10/24 14:51:07 hhg -;; Changed order of "Inversion_clear" and "Inversion" so that former is -;; fontified first. -;; Added "Print" to list of commands. -;; -;; Revision 1.3 1997/10/17 14:45:53 hhg -;; Added "Induction" as tactic -;; -;; Revision 1.2 1997/10/13 17:10:29 tms -;; *** empty log message *** -;; -;; Revision 1.1.2.2 1997/10/08 08:22:28 hhg -;; Updated undo, fixed bugs, more modularization -;; -;; Revision 1.1.2.1 1997/10/07 13:34:10 hhg -;; New structure to share as much as possible between LEGO and Coq. -;; -;; - -(require 'proof-fontlock) - -;; ----- keywords for font-lock. - -(defvar coq-keywords-decl - '( -"Axiom" -"Hypothesis" -"Parameter" -"Variable" -)) - -(defvar coq-keywords-defn - '( -"CoFixpoint" -"CoInductive" -"Fixpoint" -"Inductive" -"Mutual\\s-+Inductive" -"Scheme" -)) - -(defvar coq-keywords-goal - '( -"Definition" -"Fact" -"Goal" -"Lemma" -"Local" -"Remark" -"Theorem" -)) - -(defvar coq-keywords-save - '( -"Defined" -"Save" -"Qed" -)) - -(defvar coq-keywords-kill-goal '( -"Abort" -)) - -(defvar coq-keywords-commands - '( -"AddPath" -"Cd" -"Check" -"Class" -"Coercion" -"DelPath" -"Eval" -"Extraction" -"Focus" -"Immediate" -"Hint" -"Infix" -"Opaque" -"Print" -"Proof" -"Pwd" -"Reset" -"Search" -"Show" -"Transparent" -)) - -(defvar coq-tactics - '( -"Absurd" -"Apply" -"Assumption" -"Auto" -"Case" -"Change" -"Clear" -"Cofix" -"Compute" -"Constructor" -"Contradiction" -"Cut" -"DHyp" -"DInd" -"Dependent" -"Destruct" -"Discriminate" -"Double" -"EApply" -"EAuto" -"Elim" -"End" -"Exact" -"Exists" -"Fix" -"Generalize" -"Grammar" -"Hnf" -"Induction" -"Injection" -"Intro" -"Intros" -"Intuition" -"Inversion_clear" -"Inversion" -"LApply" -"Left" -"Linear" -"Load" -"Pattern" -"Program_all" -"Program" -"Prolog" -"Realizer" -"Red" -"Reflexivity" -"Replace" -"Rewrite" -"Right" -"Section" -"Simplify_eq" -"Simpl" -"Specialize" -"Split" -"Symmetry" -"Syntax" -"Tauto" -"Transitivity" -"Trivial" -"Unfold" -)) - -(defvar coq-keywords - (append coq-keywords-goal coq-keywords-save coq-keywords-decl - coq-keywords-defn coq-keywords-commands coq-tactics) - "All keywords in a Coq script") - -(defvar coq-tacticals '( -"Do" -"Idtac" -"OrElse" -"Repeat" -"Try" -)) - -;; ----- regular expressions -(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\)" - "A regular expression indicating that the Coq process has identified - an error.") - -(defvar coq-id proof-id) - -(defvar coq-ids (proof-ids coq-id)) - -(defun coq-abstr-regexp (paren char) - (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" char)) - -(defvar coq-font-lock-terms - (list - - ;; lambda binders - (list (coq-abstr-regexp "\\[" ":") 1 'font-lock-declaration-name-face) - - ;; Pi binders - (list (coq-abstr-regexp "(" ":") 1 'font-lock-declaration-name-face) - - ;; Kinds - (cons (concat "\\\\|\\\\|\\ + +;; $Log$ +;; Revision 1.2 1998/08/11 11:43:13 da +;; Renamed -fontlock to -syntax +;; +;; Revision 1.14 1998/06/11 12:20:14 hhg +;; Added "Scheme" as definition keyword. +;; +;; Revision 1.13 1998/06/10 11:38:04 hhg +;; Added "Mutual Inductive" as definition keyword. +;; Changed "\\s " into "\\s-" as whitespace pattern. +;; +;; Revision 1.12 1998/06/03 18:01:54 hhg +;; Changed Compute from command to tactic. +;; Added Fix, Destruct and Cofix as tactics. +;; Added Local as goal. +;; +;; Revision 1.11 1998/06/02 15:33:16 hhg +;; Minor modifications to comments +;; +;; Revision 1.10 1998/05/15 16:13:23 hhg +;; Added CoFixpoint and tactics. +;; Changed indentation. +;; +;; Revision 1.9 1998/05/05 14:19:39 hhg +;; Added CoInductive. +;; Made updates to reflect problem with "Definition", which couldn't be +;; used with proof scripts. +;; +;; Revision 1.8 1998/01/15 13:30:17 hhg +;; Added coq-shell-cd +;; Some new fontlocks +;; +;; Revision 1.7 1997/11/26 17:12:55 hhg +;; Incorporated tms's suggestion for simplifying coq-font-lock-keywords-1 +;; +;; Revision 1.6 1997/11/06 16:46:20 hhg +;; Updates to Coq fontlock tables +;; +;; Revision 1.5 1997/10/30 15:58:29 hhg +;; Updates for coq, including: +;; * pbp-goal-command and pbp-hyp-command use proof-terminal-string +;; * updates to keywords +;; * fix for goal regexp +;; +;; Revision 1.4 1997/10/24 14:51:07 hhg +;; Changed order of "Inversion_clear" and "Inversion" so that former is +;; fontified first. +;; Added "Print" to list of commands. +;; +;; Revision 1.3 1997/10/17 14:45:53 hhg +;; Added "Induction" as tactic +;; +;; Revision 1.2 1997/10/13 17:10:29 tms +;; *** empty log message *** +;; +;; Revision 1.1.2.2 1997/10/08 08:22:28 hhg +;; Updated undo, fixed bugs, more modularization +;; +;; Revision 1.1.2.1 1997/10/07 13:34:10 hhg +;; New structure to share as much as possible between LEGO and Coq. +;; +;; + +(require 'proof-syntax) + +;; ----- keywords for font-lock. + +(defvar coq-keywords-decl + '( +"Axiom" +"Hypothesis" +"Parameter" +"Variable" +)) + +(defvar coq-keywords-defn + '( +"CoFixpoint" +"CoInductive" +"Fixpoint" +"Inductive" +"Mutual\\s-+Inductive" +"Scheme" +)) + +(defvar coq-keywords-goal + '( +"Definition" +"Fact" +"Goal" +"Lemma" +"Local" +"Remark" +"Theorem" +)) + +(defvar coq-keywords-save + '( +"Defined" +"Save" +"Qed" +)) + +(defvar coq-keywords-kill-goal '( +"Abort" +)) + +(defvar coq-keywords-commands + '( +"AddPath" +"Cd" +"Check" +"Class" +"Coercion" +"DelPath" +"Eval" +"Extraction" +"Focus" +"Immediate" +"Hint" +"Infix" +"Opaque" +"Print" +"Proof" +"Pwd" +"Reset" +"Search" +"Show" +"Transparent" +)) + +(defvar coq-tactics + '( +"Absurd" +"Apply" +"Assumption" +"Auto" +"Case" +"Change" +"Clear" +"Cofix" +"Compute" +"Constructor" +"Contradiction" +"Cut" +"DHyp" +"DInd" +"Dependent" +"Destruct" +"Discriminate" +"Double" +"EApply" +"EAuto" +"Elim" +"End" +"Exact" +"Exists" +"Fix" +"Generalize" +"Grammar" +"Hnf" +"Induction" +"Injection" +"Intro" +"Intros" +"Intuition" +"Inversion_clear" +"Inversion" +"LApply" +"Left" +"Linear" +"Load" +"Pattern" +"Program_all" +"Program" +"Prolog" +"Realizer" +"Red" +"Reflexivity" +"Replace" +"Rewrite" +"Right" +"Section" +"Simplify_eq" +"Simpl" +"Specialize" +"Split" +"Symmetry" +"Syntax" +"Tauto" +"Transitivity" +"Trivial" +"Unfold" +)) + +(defvar coq-keywords + (append coq-keywords-goal coq-keywords-save coq-keywords-decl + coq-keywords-defn coq-keywords-commands coq-tactics) + "All keywords in a Coq script") + +(defvar coq-tacticals '( +"Do" +"Idtac" +"OrElse" +"Repeat" +"Try" +)) + +;; ----- regular expressions +(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\)" + "A regular expression indicating that the Coq process has identified + an error.") + +(defvar coq-id proof-id) + +(defvar coq-ids (proof-ids coq-id)) + +(defun coq-abstr-regexp (paren char) + (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" char)) + +(defvar coq-font-lock-terms + (list + + ;; lambda binders + (list (coq-abstr-regexp "\\[" ":") 1 'font-lock-declaration-name-face) + + ;; Pi binders + (list (coq-abstr-regexp "(" ":") 1 'font-lock-declaration-name-face) + + ;; Kinds + (cons (concat "\\\\|\\\\|\\-fontlock to -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-fontlock.el deleted file mode 100644 index 437c4906..00000000 --- a/lego-fontlock.el +++ /dev/null @@ -1,126 +0,0 @@ -;; lego-fontlock.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 - -;; should perhaps be called lego-syntax instead of lego-fontlock - -;; $Log$ -;; Revision 1.6 1998/07/27 15:39:53 tms -;; Supports official LEGO release 1.3 -;; -;; Revision 1.5 1998/05/29 09:49:40 tms -;; o outsourced indentation to proof-indent -;; o support indentation of commands -;; o replaced test of Emacs version with availability test of specific -;; features -;; o C-c C-c, C-c C-v and M-tab is now available in all buffers -;; -;; Revision 1.4 1998/05/22 09:37:12 tms -;; included "Invert" in `lego-keywords' -;; -;; Revision 1.3 1997/11/26 14:11:29 tms -;; simplified code: -;; lego-goal-with-hole-regexp and lego-save-with-hole-regexp is now -;; used for lego-font-lock-keywords-1 as well -;; -;; Revision 1.2 1997/10/13 17:13:14 tms -;; *** empty log message *** -;; -;; Revision 1.1.2.2 1997/10/08 08:22:31 hhg -;; Updated undo, fixed bugs, more modularization -;; -;; Revision 1.1.2.1 1997/10/07 13:34:23 hhg -;; New structure to share as much as possible between LEGO and Coq. -;; -;; - - -(require 'proof-fontlock) - -;; ----- keywords for font-lock. - -(defconst lego-keywords-goal '("$?Goal")) - -(defconst lego-keywords-save '("$?Save" "SaveFrozen" "SaveUnfrozen")) - -(defconst lego-commands - (append lego-keywords-goal lego-keywords-save - '("allE" "allI" "andE" "andI" "Assumption" "Claim" - "Cut" "Discharge" "DischargeKeep" - "echo" "exE" "exI" "Expand" "ExpAll" - "ExportState" "Equiv" "For" "Freeze" "Hnf" "Immed" - "impE" "impI" "Induction" "Inductive" - "Invert" "Init" "intros" "Intros" "Module" "Next" - "Normal" "notE" "notI" "orE" "orIL" "orIR" "qnify" "Qnify" - "Qrepl" "Record" "Refine" "Repeat" "Try" "Unfreeze")) - "Subset of LEGO keywords and tacticals which are terminated by a \?;") - -(defconst lego-keywords - (append lego-commands - '("Constructors" "Double" "ElimOver" "Fields" "Import" "Inversion" - "NoReductions" "Parameters" "Relation" "Theorems"))) - -(defconst lego-tacticals '("Then" "Else" "Try" "Repeat" "For")) - -;; ----- regular expressions for font-lock -(defvar lego-error-regexp "^\\(Error\\|Lego parser\\)" - "A regular expression indicating that the LEGO process has - identified an error.") - -(defvar lego-id proof-id) - -(defvar lego-ids (concat lego-id "\\(\\s *,\\s *" lego-id "\\)*") - "*For font-lock, we treat \",\" separated identifiers as one identifier - and refontify commata using \\{lego-fixup-change}.") - -(defun lego-decl-defn-regexp (char) - (concat "\\[\\s *\\(" lego-ids - "\\)\\s *\\(\\[[^]]+\\]\\s *\\)*" char)) -; Examples -; ^ ^^^^ ^^^^^^^^^^^^^^^^^^^^^^^ ^^^^ -; [ sort = -; [ sort [n:nat] = -; [ sort [abbrev=...][n:nat] = - -(defvar lego-font-lock-terms - (list - - ; lambda binders - (list (lego-decl-defn-regexp "[:|]") 1 - 'font-lock-declaration-name-face) - - ; let binders - (list (lego-decl-defn-regexp "=") 1 'font-lock-function-name-face) - - ; Pi and Sigma binders - (list (concat "[{<]\\s *\\(" lego-ids "\\)") 1 - 'font-lock-declaration-name-face) - - ;; Kinds - (cons (concat "\\\\|\\ + +;; $Log$ +;; Revision 1.2 1998/08/11 11:43:14 da +;; Renamed -fontlock to -syntax +;; +;; Revision 1.6 1998/07/27 15:39:53 tms +;; Supports official LEGO release 1.3 +;; +;; Revision 1.5 1998/05/29 09:49:40 tms +;; o outsourced indentation to proof-indent +;; o support indentation of commands +;; o replaced test of Emacs version with availability test of specific +;; features +;; o C-c C-c, C-c C-v and M-tab is now available in all buffers +;; +;; Revision 1.4 1998/05/22 09:37:12 tms +;; included "Invert" in `lego-keywords' +;; +;; Revision 1.3 1997/11/26 14:11:29 tms +;; simplified code: +;; lego-goal-with-hole-regexp and lego-save-with-hole-regexp is now +;; used for lego-font-lock-keywords-1 as well +;; +;; Revision 1.2 1997/10/13 17:13:14 tms +;; *** empty log message *** +;; +;; Revision 1.1.2.2 1997/10/08 08:22:31 hhg +;; Updated undo, fixed bugs, more modularization +;; +;; Revision 1.1.2.1 1997/10/07 13:34:23 hhg +;; New structure to share as much as possible between LEGO and Coq. +;; +;; + + +(require 'proof-syntax) + +;; ----- keywords for font-lock. + +(defconst lego-keywords-goal '("$?Goal")) + +(defconst lego-keywords-save '("$?Save" "SaveFrozen" "SaveUnfrozen")) + +(defconst lego-commands + (append lego-keywords-goal lego-keywords-save + '("allE" "allI" "andE" "andI" "Assumption" "Claim" + "Cut" "Discharge" "DischargeKeep" + "echo" "exE" "exI" "Expand" "ExpAll" + "ExportState" "Equiv" "For" "Freeze" "Hnf" "Immed" + "impE" "impI" "Induction" "Inductive" + "Invert" "Init" "intros" "Intros" "Module" "Next" + "Normal" "notE" "notI" "orE" "orIL" "orIR" "qnify" "Qnify" + "Qrepl" "Record" "Refine" "Repeat" "Try" "Unfreeze")) + "Subset of LEGO keywords and tacticals which are terminated by a \?;") + +(defconst lego-keywords + (append lego-commands + '("Constructors" "Double" "ElimOver" "Fields" "Import" "Inversion" + "NoReductions" "Parameters" "Relation" "Theorems"))) + +(defconst lego-tacticals '("Then" "Else" "Try" "Repeat" "For")) + +;; ----- regular expressions for font-lock +(defvar lego-error-regexp "^\\(Error\\|Lego parser\\)" + "A regular expression indicating that the LEGO process has + identified an error.") + +(defvar lego-id proof-id) + +(defvar lego-ids (concat lego-id "\\(\\s *,\\s *" lego-id "\\)*") + "*For font-lock, we treat \",\" separated identifiers as one identifier + and refontify commata using \\{lego-fixup-change}.") + +(defun lego-decl-defn-regexp (char) + (concat "\\[\\s *\\(" lego-ids + "\\)\\s *\\(\\[[^]]+\\]\\s *\\)*" char)) +; Examples +; ^ ^^^^ ^^^^^^^^^^^^^^^^^^^^^^^ ^^^^ +; [ sort = +; [ sort [n:nat] = +; [ sort [abbrev=...][n:nat] = + +(defvar lego-font-lock-terms + (list + + ; lambda binders + (list (lego-decl-defn-regexp "[:|]") 1 + 'font-lock-declaration-name-face) + + ; let binders + (list (lego-decl-defn-regexp "=") 1 'font-lock-function-name-face) + + ; Pi and Sigma binders + (list (concat "[{<]\\s *\\(" lego-ids "\\)") 1 + 'font-lock-declaration-name-face) + + ;; Kinds + (cons (concat "\\\\|\\ - -;; $Log$ -;; Revision 1.8 1998/06/10 11:45:12 hhg -;; Changed "\\s " to "\\s-" in proof-id as whitespace pattern. -;; -;; Revision 1.7 1998/05/29 09:49:53 tms -;; o outsourced indentation to proof-indent -;; o support indentation of commands -;; o replaced test of Emacs version with availability test of specific -;; features -;; o C-c C-c, C-c C-v and M-tab is now available in all buffers -;; -;; Revision 1.6 1998/05/06 15:56:14 hhg -;; Fixed problem introduced by working on emacs19 in -;; proof-zap-commas-region. -;; -;; Revision 1.5 1998/05/05 14:25:45 hhg -;; Simple white-space changes. -;; -;; Revision 1.4 1998/01/16 15:40:28 djs -;; Commented the code of proof.el and lego.el a bit. Made a minor change -;; to the way errors are handled, so that any delayed output is inserted -;; in the buffer before the error message is printed. -;; -;; Revision 1.3 1997/11/17 17:11:19 djs -;; Added some magic commands: proof-frob-locked-end, proof-try-command, -;; proof-interrupt-process. Added moving nested lemmas above goal for coq. -;; Changed the key mapping for assert-until-point to C-c RET. -;; -;; Revision 1.2 1997/10/13 17:13:50 tms -;; *** empty log message *** -;; -;; Revision 1.1.2.1 1997/10/07 13:34:27 hhg -;; New structure to share as much as possible between LEGO and Coq. -;; -;; - -(require 'font-lock) - -(defun ids-to-regexp (l) - "transforms a non-empty list of identifiers `l' into a regular - expression matching any of its elements" - (mapconcat (lambda (s) (concat "\\<" s "\\>")) l "\\|")) - -;; Generic font-lock - -;; proof-commands-regexp is used for indentation -(defvar proof-commands-regexp "" - "Subset of keywords and tacticals which are terminated by the - `proof-terminal-char'") - - -(defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)" - "A regular expression for parsing identifiers.") - -;; For font-lock, we treat ,-separated identifiers as one identifier -;; and refontify commata using \{proof-unfontify-separator}. - -(defun proof-ids (proof-id) - "Function to generate a regular expression for separated lists of - identifiers." - (concat proof-id "\\(\\s-*,\\s-*" proof-id "\\)*")) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; font lock faces: declarations, errors, tacticals ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun proof-have-color () - ()) - -(defvar font-lock-declaration-name-face -(progn - (cond - ((proof-have-color) - (copy-face 'bold 'font-lock-declaration-name-face) - - ;; Emacs 19.28 compiles this down to - ;; internal-set-face-1. This is not compatible with XEmacs - (set-face-foreground - 'font-lock-declaration-name-face "chocolate")) - (t (copy-face 'bold-italic 'font-lock-declaration-name-face))))) - -;; (if running-emacs19 -;; (setq font-lock-declaration-name-face -;; (face-name 'font-lock-declaration-name-face)) - -(defvar font-lock-tacticals-name-face -(if (proof-have-color) - (let ((face (make-face 'font-lock-tacticals-name-face))) - (dont-compile - (set-face-foreground face "MediumOrchid3")) - face) - (copy-face 'bold 'font-lock-tacticals-name-face))) - -(defvar font-lock-error-face -(if (proof-have-color) - (let ((face (make-face 'font-lock-error-face))) - (dont-compile - (set-face-foreground face "red")) - face) - (copy-face 'bold 'font-lock-error-face))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; A big hack to unfontify commas in declarations and definitions. ;; -;; All that can be said for it is that the previous way of doing ;; -;; this was even more bogus. ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; Refontify the whole line, 'cos that's what font-lock-after-change -;; does. - -(defun proof-zap-commas-region (start end length) - (save-excursion - (let - ((start (progn (goto-char start) (beginning-of-line) (point))) - (end (progn (goto-char end) (end-of-line) (point)))) - (goto-char start) - (while (search-forward "," end t) - (if (memq (get-char-property (- (point) 1) 'face) - '(font-lock-declaration-name-face - font-lock-function-name-face)) - (font-lock-remove-face (- (point) 1) (point)) - ))))) - -(defun proof-zap-commas-buffer () - (proof-zap-commas-region (point-min) (point-max) 0)) - -(defun proof-unfontify-separator () - (make-local-variable 'after-change-functions) - (setq after-change-functions - (append (delq 'proof-zap-commas-region after-change-functions) - '(proof-zap-commas-region)))) - - -(provide 'proof-fontlock) 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 (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-syntax.el b/proof-syntax.el new file mode 100644 index 00000000..56eae4b4 --- /dev/null +++ b/proof-syntax.el @@ -0,0 +1,143 @@ +;; proof-syntax.el Generic font lock expressions +;; Copyright (C) 1997 LFCS Edinburgh. +;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequiera +;; Maintainer: LEGO Team + +;; $Log$ +;; Revision 1.2 1998/08/11 11:43:14 da +;; Renamed -fontlock to -syntax +;; +;; Revision 1.8 1998/06/10 11:45:12 hhg +;; Changed "\\s " to "\\s-" in proof-id as whitespace pattern. +;; +;; Revision 1.7 1998/05/29 09:49:53 tms +;; o outsourced indentation to proof-indent +;; o support indentation of commands +;; o replaced test of Emacs version with availability test of specific +;; features +;; o C-c C-c, C-c C-v and M-tab is now available in all buffers +;; +;; Revision 1.6 1998/05/06 15:56:14 hhg +;; Fixed problem introduced by working on emacs19 in +;; proof-zap-commas-region. +;; +;; Revision 1.5 1998/05/05 14:25:45 hhg +;; Simple white-space changes. +;; +;; Revision 1.4 1998/01/16 15:40:28 djs +;; Commented the code of proof.el and lego.el a bit. Made a minor change +;; to the way errors are handled, so that any delayed output is inserted +;; in the buffer before the error message is printed. +;; +;; Revision 1.3 1997/11/17 17:11:19 djs +;; Added some magic commands: proof-frob-locked-end, proof-try-command, +;; proof-interrupt-process. Added moving nested lemmas above goal for coq. +;; Changed the key mapping for assert-until-point to C-c RET. +;; +;; Revision 1.2 1997/10/13 17:13:50 tms +;; *** empty log message *** +;; +;; Revision 1.1.2.1 1997/10/07 13:34:27 hhg +;; New structure to share as much as possible between LEGO and Coq. +;; +;; + +(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" + (mapconcat (lambda (s) (concat "\\<" s "\\>")) l "\\|")) + +;; Generic font-lock + +;; proof-commands-regexp is used for indentation +(defvar proof-commands-regexp "" + "Subset of keywords and tacticals which are terminated by the + `proof-terminal-char'") + + +(defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)" + "A regular expression for parsing identifiers.") + +;; For font-lock, we treat ,-separated identifiers as one identifier +;; and refontify commata using \{proof-unfontify-separator}. + +(defun proof-ids (proof-id) + "Function to generate a regular expression for separated lists of + identifiers." + (concat proof-id "\\(\\s-*,\\s-*" proof-id "\\)*")) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; font lock faces: declarations, errors, tacticals ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-have-color () + ()) + +(defvar font-lock-declaration-name-face +(progn + (cond + ((proof-have-color) + (copy-face 'bold 'font-lock-declaration-name-face) + + ;; Emacs 19.28 compiles this down to + ;; internal-set-face-1. This is not compatible with XEmacs + (set-face-foreground + 'font-lock-declaration-name-face "chocolate")) + (t (copy-face 'bold-italic 'font-lock-declaration-name-face))))) + +;; (if running-emacs19 +;; (setq font-lock-declaration-name-face +;; (face-name 'font-lock-declaration-name-face)) + +(defvar font-lock-tacticals-name-face +(if (proof-have-color) + (let ((face (make-face 'font-lock-tacticals-name-face))) + (dont-compile + (set-face-foreground face "MediumOrchid3")) + face) + (copy-face 'bold 'font-lock-tacticals-name-face))) + +(defvar font-lock-error-face +(if (proof-have-color) + (let ((face (make-face 'font-lock-error-face))) + (dont-compile + (set-face-foreground face "red")) + face) + (copy-face 'bold 'font-lock-error-face))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; A big hack to unfontify commas in declarations and definitions. ;; +;; All that can be said for it is that the previous way of doing ;; +;; this was even more bogus. ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Refontify the whole line, 'cos that's what font-lock-after-change +;; does. + +(defun proof-zap-commas-region (start end length) + (save-excursion + (let + ((start (progn (goto-char start) (beginning-of-line) (point))) + (end (progn (goto-char end) (end-of-line) (point)))) + (goto-char start) + (while (search-forward "," end t) + (if (memq (get-char-property (- (point) 1) 'face) + '(font-lock-declaration-name-face + font-lock-function-name-face)) + (font-lock-remove-face (- (point) 1) (point)) + ))))) + +(defun proof-zap-commas-buffer () + (proof-zap-commas-region (point-min) (point-max) 0)) + +(defun proof-unfontify-separator () + (make-local-variable 'after-change-functions) + (setq after-change-functions + (append (delq 'proof-zap-commas-region after-change-functions) + '(proof-zap-commas-region)))) + + +(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))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -- cgit v1.2.3