Renamed file

1 files changed, 196 insertions, 0 deletions

diff --git a/etc/doc-notes.txt b/etc/doc-notes.txt
new file mode 100644
index 00000000..0cf83b88
--- /dev/null
+++ b/etc/doc-notes.txt
@@ -0,0 +1,196 @@
+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.
+
+