From abbe57d8b69d79e9eb6899f182379d9c6c4fdc7f Mon Sep 17 00:00:00 2001 From: Thomas Kleymann Date: Thu, 3 Sep 1998 13:40:31 +0000 Subject: minor modifications --- proof-syntax.el | 44 +------------------------------------------- 1 file changed, 1 insertion(+), 43 deletions(-) (limited to 'proof-syntax.el') diff --git a/proof-syntax.el b/proof-syntax.el index 45c9015d..5caa8fe3 100644 --- a/proof-syntax.el +++ b/proof-syntax.el @@ -1,50 +1,8 @@ ;; proof-syntax.el Generic font lock expressions -;; Copyright (C) 1997 LFCS Edinburgh. +;; Copyright (C) 1997-1998 LFCS Edinburgh. ;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequiera ;; Maintainer: LEGO Team -;; $Log$ -;; Revision 2.0 1998/08/11 15:00:04 da -;; New branch -;; -;; 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- -- cgit v1.2.3