diff options
| -rw-r--r-- | BUGS | 4 | ||||
| -rw-r--r-- | Makefile.devel | 3 | ||||
| -rw-r--r-- | coq/coqtags | 3 | ||||
| -rw-r--r-- | coq/example.v | 1 | ||||
| -rw-r--r-- | doc/proof.texinfo | 3 | ||||
| -rw-r--r-- | generic/pbp.el | 1 | ||||
| -rw-r--r-- | generic/proof.el | 1 | ||||
| -rw-r--r-- | generic/span-extent.el | 20 | ||||
| -rw-r--r-- | generic/span-overlay.el | 58 | ||||
| -rw-r--r-- | isa/example.ML | 9 | ||||
| -rw-r--r-- | isa/isa-syntax.el | 4 | ||||
| -rw-r--r-- | isa/isa.el | 2 | ||||
| -rw-r--r-- | lego/lego-syntax.el | 3 | ||||
| -rw-r--r-- | lego/lego.el | 3 | ||||
| -rw-r--r-- | lego/legotags | 4 |
15 files changed, 40 insertions, 79 deletions
@@ -1,6 +1,8 @@ -Known bugs and workarounds. +Known Bugs and Workarounds. =========================== +$Id$ + * Outline-mode does not work in proof script files due to read-only restrictions of protected region diff --git a/Makefile.devel b/Makefile.devel index f66d13e7..b508346e 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -1,8 +1,11 @@ +# # TODO (da): # - tag the release in the sources # - build docs # - distrib is built by running 'make dist' in # exported source dir +# +# $Id$ CVSROOT = /home/lego/src EXPORTDIR = /home/lego/pub/emacs diff --git a/coq/coqtags b/coq/coqtags index b6c72c78..b51066ed 100644 --- a/coq/coqtags +++ b/coq/coqtags @@ -1,4 +1,7 @@ #!/usr/local/bin/perl4 +# +# $Id$ +# $/=0777; if($#ARGV<$[) {die "No Files\n";} diff --git a/coq/example.v b/coq/example.v index c9c88d9e..045e2f94 100644 --- a/coq/example.v +++ b/coq/example.v @@ -1,2 +1,3 @@ +(* Id *) INSERT HANDY COQ EXAMPLE HERE!
\ No newline at end of file diff --git a/doc/proof.texinfo b/doc/proof.texinfo index a825feae..fd3a3b29 100644 --- a/doc/proof.texinfo +++ b/doc/proof.texinfo @@ -1,4 +1,7 @@ \input texinfo @c -*-texinfo-*- +@c +@c $Id$ +@c @c %**start of header @setfilename proof.info @settitle Generic Proof Assistant Mode diff --git a/generic/pbp.el b/generic/pbp.el index 23ffdd68..921765fb 100644 --- a/generic/pbp.el +++ b/generic/pbp.el @@ -1,2 +1,3 @@ +;; $Id$ (provide 'pbp) diff --git a/generic/proof.el b/generic/proof.el index c343c83f..f2c5e2e4 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -6,6 +6,7 @@ ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> ;; Thanks to Robert Boyer, Rod Burstall, ;; James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens +;; ;; $Id$ (require 'proof-site) diff --git a/generic/span-extent.el b/generic/span-extent.el index cc74eee6..0a9777c8 100644 --- a/generic/span-extent.el +++ b/generic/span-extent.el @@ -4,25 +4,7 @@ ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> -;; $Log$ -;; Revision 2.0 1998/09/09 13:57:45 da -;; Fixup branch number -;; -;; Revision 1.1 1998/09/03 13:51:33 da -;; Renamed for new subdirectory structure -;; -;; Revision 2.0 1998/08/11 15:00:13 da -;; New branch -;; -;; Revision 1.4 1998/06/10 14:01:48 hhg -;; Wrote generic span functions for making spans read-only or read-write. -;; -;; Revision 1.3 1998/06/02 15:36:44 hhg -;; Corrected comment about this being for xemacs. -;; -;; Revision 1.2 1998/05/19 15:30:27 hhg -;; Added header and log message. -;; +;; $Id$ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Bridging the emacs19/xemacs gulf ;; diff --git a/generic/span-overlay.el b/generic/span-overlay.el index 228a3967..3d816272 100644 --- a/generic/span-overlay.el +++ b/generic/span-overlay.el @@ -4,63 +4,7 @@ ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> -;; $Log$ -;; Revision 2.0 1998/09/09 13:57:46 da -;; Fixup branch number -;; -;; Revision 1.1 1998/09/03 13:51:34 da -;; Renamed for new subdirectory structure -;; -;; Revision 2.0 1998/08/11 15:00:13 da -;; New branch -;; -;; Revision 1.9 1998/06/10 14:02:39 hhg -;; Wrote generic span functions for making spans read-only or read-write. -;; Fixed bug in add-span and remove-span concerning return value of -;; span-traverse. -;; -;; Revision 1.8 1998/06/10 12:41:47 hhg -;; Compare span-end first rather than span-start in span-lt, because -;; proof-lock-span is often changed and has starting point 1. -;; Factored out common code of add-span and remove-span into -;; span-traverse. -;; -;; Revision 1.7 1998/06/03 17:40:07 hhg -;; Changed last-span to before-list. -;; Added definitions of foldr and foldl if they aren't already loaded. -;; Changed definitions of add-span, remove-span and find-span-aux to be -;; non-recursive. -;; Removed detach-extent since this file isn't used by xemacs. -;; Added function append-unique to avoid repetitions in list generated by -;; spans-at-region. -;; Changed next-span so it uses member-if. -;; -;; Revision 1.6 1998/06/02 15:36:51 hhg -;; Corrected comment about this being for emacs19. -;; -;; Revision 1.5 1998/05/29 09:50:10 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/21 17:27:41 hhg -;; Removed uninitialized os variable in spans-at-region. -;; -;; Revision 1.3 1998/05/21 08:28:52 hhg -;; Initialize 'before pointer in add-span-aux when last-span is nil. -;; Removed span-at-type. -;; Fixed bug in span-at-before, where (span-start span) may be nil. -;; Added spans-at-(point|region)[-prop], which fixes bug of C-c u at end -;; of buffer. -;; -;; Revision 1.2 1998/05/19 15:31:37 hhg -;; Added header and log message. -;; Fixed set-span-endpoints so it preserves invariant. -;; Changed add-span and remove-span so that they update last-span -;; correctly themselves, and don't take last-span as an argument. -;; +;; $Id$ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Bridging the emacs19/xemacs gulf ;; diff --git a/isa/example.ML b/isa/example.ML index d5ba5153..5a6f7dfb 100644 --- a/isa/example.ML +++ b/isa/example.ML @@ -1,3 +1,12 @@ +(* + Example proof script for Isabelle + + David Aspinall <da@dcs.ed.ac.uk> + + $Id$ + +*) + goal HOL.thy "(A & B)-->(B & A)"; br impI 1; diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el index 6baa5e9d..52e2ee90 100644 --- a/isa/isa-syntax.el +++ b/isa/isa-syntax.el @@ -1,5 +1,9 @@ ;; isa-syntax.el Syntax expressions for Isabelle ;; +;; David Aspinall <da@dcs.ed.ac.uk> +;; +;; $Id$ +;; (require 'proof-syntax) @@ -1,7 +1,7 @@ ;; isa.el Major mode for Isabelle proof assistant ;; Copyright (C) 1994-1998 LFCS Edinburgh. ;; Author: David Aspinall - +;; ;; $Id$ ;; diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el index 60ede04f..f9fb52d2 100644 --- a/lego/lego-syntax.el +++ b/lego/lego-syntax.el @@ -2,6 +2,9 @@ ;; Copyright (C) 1994, 1995, 1996, 1997 LFCS Edinburgh. ;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequeira ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> +;; +;; $Id$ +;; (require 'proof-syntax) diff --git a/lego/lego.el b/lego/lego.el index 3dd06ca5..2b83e51a 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -2,6 +2,9 @@ ;; Copyright (C) 1994 - 1998 LFCS Edinburgh. ;; Author: Thomas Kleymann and Dilip Sequeira ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> +;; +;; $Id$ +;; (require 'lego-syntax) (require 'outline) diff --git a/lego/legotags b/lego/legotags index a3c13eab..a5c0f825 100644 --- a/lego/legotags +++ b/lego/legotags @@ -1,5 +1,7 @@ #!/usr/local/bin/perl - +# +# $Id$ +# undef $/; if($#ARGV<$[) {die "No Files\n";} |