Deleted file

6 files changed, 0 insertions, 481 deletions

diff --git a/etc/announce b/etc/announce
deleted file mode 100644
index 45537576..00000000
--- a/etc/announce
+++ /dev/null
@@ -1,56 +0,0 @@
-            Announcing  Proof General  Version 3.6
-    A Generic Emacs interface for Interactive Proof Assistants
-              http://proofgeneral.inf.ed.ac.uk
-
-      Contact: David Aspinall <da+pg-feedback@inf.ed.ac.uk>
-
-Proof General is a generic (X)Emacs interface for proof assistants.
-It can be instantiated for the proof assistant of your choice, and is
-supplied ready-customised for Isabelle, Coq, LEGO, and PhoX, and, 
-experimentally, several other systems.
-
-Proof General includes these features, amongst others:
-
-. Script management: proof assistant state reflected in editor
-. Toolbar and menus: commands for building and replaying proofs
-. Syntax highlighting of proof scripts and prover output; hiding proofs
-. Display of real logical symbols, greek letters, etc with X-Symbol
-. Activation of prover output for subterm navigation, proof-by-pointing
-. Simplified communication: proof assistant verbosity hidden
-. Menus for jumping to theorems/definitions, etc in a proof script
-. Provision to easily run proof assistant on a remote host
-. Works on any platform Emacs does, in window system or plain console 
-
-Summary of interesting changes since 3.5 (April 2004):
-
-. Updates and bug fixes for Coq 8.0
-. Extensions for development version of Isabelle, esp. PGIP support
-
-Summary of interesting changes since 3.4 (August 2002):
-
-. Speedbar and Index Menu.  Speedbar provides a handy file/tag tree.
-. Improved display management.  
-. RPM packages with freedesktop.org integration and compiled files
-. Keyboard hints and other messages displayed in minibuffer
-. Improved menus, user options, script colouring and active highlighting
-. For Coq (8.0): "holes" for editing expressions, extra menus, auto compilation
-. For Isabelle (2004): browsing/highlighting theorem dependencies
-. For Isabelle: using LaTeX mode for LaTeX parts of proof documents (via MMM)
-. New instances of PG: Casl Consistency Checker, Shell Script
-. Additional sample proofs (some from http://www.cs.kun.nl/~freek/comparison/)
-. Many other minor improvements and editing features
-. Many changes for compatibility with latest Emacsen (esp. GNU) and provers
-. Auxiliary modes bundled: X-Symbol and MMM (Multiple Major Mode)
-
-For details of changes since 3.4, see
-http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=ProofGeneral-3.6%2FCHANGES
-
-For the latest user manual, see http://proofgeneral.inf.ed.ac.uk/doc
-
-Proof General needs a recent version of Emacs to run with.  
-Proof General 3.6 has been tested with XEmacs 21.4.15, and 
-GNU Emacs 21.3.1.  Other recent versions of either Emacs may work but 
-are not guaranteed.
-
- - David Aspinall.
-   September 2004.
diff --git a/etc/bug-notes.txt b/etc/bug-notes.txt
deleted file mode 100644
index e00a23e7..00000000
--- a/etc/bug-notes.txt
+++ /dev/null
@@ -1,32 +0,0 @@
--*- outline -*-
-
-$Id$
-
-Test cases for PG and/or Emacs bugs.
-
-----------------
-
-* XEmacs bug: buffer-syntactic-context-depth returns weird values
-
-Seems to depend on previous history.  Test in Coq buffer:
-  
-   X
-  (* comment one *)
-   Y
-  (* comment two *)
-   Z
-
-Evaluate (buffer-syntactic-context-depth) at X, Y, then Z.
-Values 0, 1, 2.  Evaluate at point Y.  Now get 0.
-Perhaps caches previous value, and bases parse on moving point
-forwards from previous value?  Anyway, doesn't do well with
-block comments.  Also bad with line comments, use same test
-case with buffer in lisp mode, except with lisp comments.
-
-Shame, would be nice to use this to help parse lisp-like
-syntax for PAs, fitting in with present scheme.
-
-
-
-
-
diff --git a/etc/doc-notes.txt b/etc/doc-notes.txt
deleted file mode 100644
index 0cf83b88..00000000
--- a/etc/doc-notes.txt
+++ /dev/null
@@ -1,196 +0,0 @@
-Developers' Notes about Documentation
--------------------------------------
-
-
-
-
-* Plan for outline of improved documentation.   (Completed)
-
- Terminology:  I suggest "proof mode" should become "proof script
- mode", aka "the proof script mode of Proof General".  We should
- be careful here, e.g. present docs speak of buffers in proof
- mode, etc, but no buffer is directly in that mode, which is
- confusing to the users, at least!
- 
- 1. Introduction						[da]
-	1.1  Quick start guide
-	1.2  Feature list, xref'd to later chaps.
-	1.2  Supported Proof Assistants, xref'd too.
-	      Support for new instances, xref'd to later chaps.
-	
- 2. Basics of script management					[da]
-        
-	2.1  What a proof script is
-	2.2  Locked region and queue region
-	2.3  Script processing commands
-	2.4  Toolbar commands
-        2.5  Other commands
-	2.4  Walkthrough example [maybe in appendix?]
-
- 3. Advanced script management					[done]
-        3.1  Proof General's view of processed files
-	3.2  Switching between proof scripts
-	3.3  Retracting across files
-	3.4  Handy hints and tips  (e.g. C-c C-b stuff?)
-	3.5  Using the proof shell
-	[ 3.6  Re-synchronizing with the proof assistant - if added ]
-
- 4. Customizing Proof General					[da]
-	4.1  Setting user options, what they are:
-	       proof-splash-inhibit
-	       etc.
-        4.2  Using proof assistant on another machine
-	4.3  Examining configuration settings (xref'd later)
-	
- 5. LEGO Proof General						[done]
-	5.1  LEGO commands
-	5.2  LEGO customizations
-	
- 6. Coq Proof General						[anon]
-        6.1  Coq commands
-	6.2  Coq customizations
-
- 7. Isabelle Proof General					[da]
-	7.1  Isabelle commands
-	7.2  Isabelle customizations
-	7.3  Notes about multiple files
-
- 8. Adapting Proof General to New Provers			[da]
-	8.1  Files and directories.  Skeleton code.
-	8.2  Settings for proof scripts
-	8.3  Settings for proof shell
-	     -- Special annotations
-	
- 9. Internals of Proof General.					[tms]
-	9.1  Proof script mode:
-		- fontification hacks
-		- spans in locked region
-	9.2  Proof shell mode
-		- proof-action-list
-		- proof-shell-exec-loop
-		- proof-shell-output-filter
-		- eager annotations
-
- 10. Credits and history					[done]
- 
- APPENDIX
-
- A. Obtaining and installing the software			[da]
- B. Known bugs  						[done]
- C. Future ideas and plans					[da]
- 
- 
-*********
-
-Support for Function Menus
-
-fume-func is a handy package which makes a menu from the function
-declarations in a buffer.  Proof General configures fume-func so
-that you can quickly jump to particular proofs in a script buffer.
-
-If you want to use fume-func, you may need to enable it for
-yourself.  It is distributed with XEmacs (and FSF GNU Emacs)
-but by not enabled by default.  To enable it you should find
-the file func-menu.el and follow the instructions there.  
-At the time of writing, the current version of XEmacs is 20.4 and
-it has these instructions:
-
-(require 'func-menu)
-(define-key global-map 'f8 'function-menu)
-(add-hook 'find-file-hooks 'fume-add-menubar-entry)
-(define-key global-map "\C-cl" 'fume-list-functions)
-(define-key global-map "\C-cg" 'fume-prompt-function-goto)
-(define-key global-map '(shift button3) 'mouse-function-menu)
-(define-key global-map '(meta  button1) 'fume-mouse-function-goto)
-
-If you have any other version of Emacs, you should check the
-fume-func.el file
-
-
-
-*********
-
-
-Isabelle with multiple files.
-
-Proper multiple file support only works for .ML files which are read
-via the theory loader, with use_thy.  If you want to load .ML files
-which aren't associated with theories, it's best to use a dummy
-theory, see [Reference to Isabelle manual]
-
-
-*****************************************************************
-
-Notes for writing a paper describing Proof General
--------------------------------------------------
-
-
-Thesis/introduction
-===================
-
-As programming languages have evolved, environments for developing and
-debugging programs have also improved.  However, discounting various
-"visual" programming languages, a program is usually still a piece of
-text which can be directly edited by a programmer, a situation which
-hasn't changed since the early days when VDUs replaced punched cards.
-
-Similarly, whilst the history of languages for proof assistants is
-much shorter, we believe that a proof script, describing the
-operations needed to construct a proof, will remain the fundamental
-form of input for proof systems.
-
-...
-- interactive proof assistants geared to developing proof scripts
-  interactively, but may not come with integrated editing support.
-  Problem of shell-like interaction is that input has to be
-  tediously reassembled after or during proof to get a successful
-  proof script.
-
-- script management [refs] aims to make this process easier.
-
-
-
-Aspects of design
-=================
-
-- Generic.  Fits inside Emacs architecture.  (Compare with comint).
-
-- Extensive use of Emacs Customization mechanism to make it easy
-  to set/inspect configuration as well as user-options.
-
-- Script management with multiple files
-
-
-Seen one proof assistant, use them all
-======================================
-
-- Same interface for different underlying systems
-
-- Compare: web technology, where "browsing" works for 
-  different protocols: http, ftp, etc
-
-- Anyone can use Proof General to browse and replay proofs from
-  other systems, without needing to know how to invoke
-  the system, etc. 
-
-- However, proof script language and output remains particular to
-  each prover.   It would be another (interesting) project to attempt to
-  map input and output into an interchange format for proof systems.
-
-
-
-A Specification for a proof assistant interface
-===============================================
-
-The settings to instantiate Proof General can be seen as a set of 
-requirements for a proof assistant interface.
-
-
-
-Example of API design guidlines
-===============================
-
-1. Use a different prompt for continued lines during input
-communication.  Helps parsing output.
-
-
diff --git a/etc/screenshot-notes.txt b/etc/screenshot-notes.txt
deleted file mode 100644
index 3a0daff6..00000000
--- a/etc/screenshot-notes.txt
+++ /dev/null
@@ -1,36 +0,0 @@
-Screenshot notes.
-=================
-
-All in 80x40 sized XEmacs.  
-
-* Isabelle: Dagstuhl HOLCF example.  Show theory file on screen too.
-
-* Isar: Example Group.thy is modified version with extra X-Symbol line:
-
-syntax (xsymbols)
-  "op *"      :: "['a::times, 'a] => 'a"          (infixl "\\<bullet>" 70);
-
-And uses of * replaced with \\<bullet>.
-
-* Coq: Example from Sorting library.  Multiple frame mode, X-Symbols,
-also with Netscape.  
-
-Most shots scaled to 0.2 or thereabouts to give nice sized thumbnail.
-
-
-
-
-
-
------------------------------------------------------------------
-
-Regenerating screen shot in html/IsaPGscreen.jpg:
-
- 30x80 sized XEmacs.  Visit isa/example.ML.
- Click on "next" button four times. 
- Drag middle modeline to display whole proof script.
- Move point to end of locked region.
- Grab with gimp, Xtns -> Screen Shot.
- Save with default quality settings.
-
------------------------------------------------------------------
\ No newline at end of file
diff --git a/etc/test-schedule.txt b/etc/test-schedule.txt
deleted file mode 100644
index 700cf5ca..00000000
--- a/etc/test-schedule.txt
+++ /dev/null
@@ -1,19 +0,0 @@
-Some test schedules for Proof General
-=====================================
-
-$Id$
-
-(in progress)
-
---------------------
-
-Desirable tests:
-
-* Settings mechanism; PROOFGENERAL_ASSISTANTS vs .emacs and
-  customize-set-variable, interaction with Isabelle startup
-  scripts.
-
-
-
-
-
diff --git a/etc/testing-log.txt b/etc/testing-log.txt
deleted file mode 100644
index 324284d4..00000000
--- a/etc/testing-log.txt
+++ /dev/null
@@ -1,142 +0,0 @@
-Fri Mar 24 15:40:10 GMT 2000 da
-
- Tested Proof General on win32 (NT4sp6) with Isabelle, Coq and
- XEmacs 21.1.9.
-
- Problems:  Isabelle bombs on paths containing chars like \ : $
-            XEmacs barfs on reading some files in PG, why??
-	    e.g. coq/coq.el 
-
-	 Can fix this by reloading coq stuff again.
-
-	 A few probs remain, e.g. toolbar enablers for undo are
-	 flaky.
-	
-
-Wed Mar 22 13:45:34 GMT 2000 da 
-
- Tested file name quoting problem with Coq, Isabelle, LEGO.
-  
-   \ quoting triggers bug in Isabelle (complaint about pathname)
-   " quoting not allowed in LEGO, \ quoting not needed.
-   Coq works well with either.
-   
-	
-
---------
-	
-Wed Nov 17 13:43:11 GMT 1999
-
- Tested compiled version.  Seems to work well for XEmacs!
- Also for FSF Emacs!  So long as using their own elc's.
-
-Tue Nov 16 15:28:51 GMT 1999
-
- Tested automatic multiple file handling: see etc/demoisa
-
- Tested FSF Emacs, after fixing several things.
-
- Tested proof by pointing in LEGO.  Fixes for bugs,
- empty pbp response, and added a useful click
- (C-button 3) for undoing and deleting the last 
- pbp command.  Can now prove example.l by PBP.
- Proof-by-pointing lives!
-
-Thu Nov 11 19:05:39 GMT 1999
-
- Tested response buffer display: see isa/message-test.ML
- Made output more regular by removing spurious space/newline 
- after every prompt, and padding response buffer with 
- newlines when messages aren't newline terminated.
-
- Testing window management for multiple frames.  Could find no
- evidence of old bug message in code about with
- special-display-regexps, script buffer gets made into
- dedicated buffer.  Removed the comment.
-
-Mon Aug 23 19:00:26 BST 1999 da
-
-  Summary of tests today:
-
-  Proof General 2.0:  sanity check.
-    Okay with XEmacs 20.4, lego 1.3.1 and Isabelle 98p1.
-    Strange overlay disappearing problem with FSF Emacs 20.2,
-    so must be X Server or architecture anomaly that causes
-    different display order.
-
-  Today's Proof General.
-
-    1. With Isabelle 98p1, no go.
-    2. Same show-stopper as above with Emacs 20.2 and 20.3.  
-       Argh!  I'm really fed up of FSF Emacs, it goes wrong
-       even when "nothing" has changed.
-    3. With current Isabelle (or, at least, 99pre180899).
-    4. Using x-symbol.  No success, and a big mess (rebinds M-x !!?)
-
-Thu Jan 21 14:27:36 GMT 1999 da
-
-  Quick test for pipe communication with emacs 20.3.
-  Used C-c C-n and C-c C-u on example.ML file in 
-  Isabelle successfully.
-
-  (Tested 990115 prerelease with piped communication
-   patch in XEmacs already, for LEGO and Isabelle).
-
-Wed Dec 16 15:45:53 GMT 1998  da
-
-  Quick test of Coq mode.
-
-  xemacs -q -l ProofGeneral/generic/proof-site.el
-
-  (setq proof-rsh-command "ssh hope")
-
-  Assertion and retraction commands work as far as I can
-  tell.  Using toolbar on file coq/example.v
-
-
-Wed Dec 16 12:25:00 GMT 1998  tms
-
-  Clarification of entry "Mon Dec 14 15:02:52 GMT 1998  da"
-
-  The problem with LEGOVERSION "alpha" can also be reproduced with
-  lego 1.3.1 (and XEmacs 20.4 or FSF Emacs 20.2) and the file
-  lego/example2.l which accesses a module in a non-writable directory.
-  You need to set chmod u-w readonly yourself; CVS doesn't like
-  non-writable directories)
-  It is a LEGO specific problem. LEGO forgets about annotations
-  sometimes. This has been reported to lego@dcs.ed.ac.uk .
-
-
-Wed Dec 16 12:25:00 GMT 1998  tms
-
-  On scar, tested Emacs 20.2.1 with lego 1.3.1 via "ssh craro",
-  LEGOVERSION "std"
-
-  emacs-20.2 -eval '(progn (load
-  "/home/tms/emacs/ProofGeneral/generic/proof-site.el")(setq
-  proof-rsh-command "ssh craro"))' lego/example.l 
-
-  Pressing C-c C-n crashes Emacs: Fatal error (11).Segmentation fault
-
-  This must be a problem with my .emacs file. Including -q in the
-  options, everyting seems to work just fine. Still, this is somewhat
-  concerning. 
-
-
-Mon Dec 14 15:02:52 GMT 1998  da
-
-  Tested Emacs 20.2.1 with lego 1.3 via "ssh hope", 
-		      with lego 1.3.1 via "ssh craro", LEGOVERSION "std"
-
-  Both successfully process example.l
-
-  With lego 1.3.1 via "ssh craro", LEGOVERSION "alpha", 
-  processing gets stuck, never reports "imports done".  
-  Is this a bug or problem with LEGO installation?
-
-  Bugs: 
-    Killing off process shell via proof-shell-exit.
-    Killing proof script buffer gives error.
-
-
-