Updated.

5 files changed, 25 insertions, 76 deletions

diff --git a/TODO b/TODO
index 1de24ff9..355620f5 100644
--- a/TODO
+++ b/TODO
@@ -34,3 +34,6 @@ Plans for upcoming versions
 
 * Make an XEmacs package
 
+* Repair byte-compilation
+
+
diff --git a/etc/announce b/etc/announce
index c0d972d6..39a31654 100644
--- a/etc/announce
+++ b/etc/announce
@@ -1,42 +1,8 @@
-To: coq-club@pauillac.inria.fr,
-    isabelle-users@cl.cam.ac.uk,
-    lego-club@dcs.ed.ac.uk,
-    uitp@dcs.gla.ac.uk,
-    bra-types@cs.chalmers.se,
-    info-hol@leopard.cs.byu.edu,
-    pvs@csl.sri.com, 
-    qed@mcs.anl.gov,				
-    theorem-provers@ai.mit.edu,
-    types@cis.upenn.edu,
-    formal-methods@cs.uidaho.edu,
-    reliable_computing@interval.usl.edu,
-    prog-lang@diku.dk
-
-    Also newsgroups:
-     comp.lang.ml
-     comp.lang.functional
-     gnu.emacs.sources
-     comp.emacs.xemacs
-     comp.os.linux.announce
-     freshmeat.net
-
-tag for comp.lang.ml, comp.lang.functional: 
-     
-[Posted here because ML and functional languages generally are
- traditional for implementing interactive theorem provers.
- Implementors of such systems may be interested in Proof General.
- Apologies for multiple copies]
-
-
- 
-        
-Subject: Proof General --- Version 3.4 release
-
             Announcing  Proof General  Version 3.4
     A Generic Emacs interface for Interactive Proof Assistants
                  http://www.proofgeneral.org
 
-         contact: David Aspinall <da@proofgeneral.org>
+           Contact: David Aspinall <da@proofgeneral.org>
 
 Proof General is a generic (X)Emacs interface for proof assistants.
 It can be instantiated for the proof assistant of your choice, and is
@@ -60,7 +26,7 @@ Summary of changes since 3.3:
 . GPL license
 . Improvements to menus, colour schemes
 . Visibility control over portions of proof script
-. In Isabelle: tracing buffers, dependency highlighting
+. In Isabelle: tracing buffers, dependency highlighting support
 . In Coq: much improved synchronization (inc sections, nested proofs)
 . Bug fixes, efficiency improvements, better generic code.
 . Compatibility improvements: XEmacs 21.4, Emacs 21.2
diff --git a/etc/release-log.txt b/etc/release-log.txt
index 045601ee..4a14cbed 100644
--- a/etc/release-log.txt
+++ b/etc/release-log.txt
@@ -1,5 +1,4 @@
-XX.08.02  3.4 Release 3-4-1
-
+29.08.02  3.4 Release 3-4 based on branch 7.0
 
 --------------------
 
diff --git a/isa/README b/isa/README
index 61527cf2..b99be777 100644
--- a/isa/README
+++ b/isa/README
@@ -15,7 +15,7 @@ with dependencies between theories communicated between Isabelle and
 Proof General.  It has a mode for editing theory files taken from
 Isamode.
 
-There is proper support for X Symbol, using the Isabelle print mode
+There is excellent support for X Symbol, using the Isabelle print mode
 for X Symbol tokens.  Many Isabelle theories have X Symbol syntax
 already defined and it's easy to add to your own theories.
 
diff --git a/todo b/todo
index 4f2b7d71..984cab31 100644
--- a/todo
+++ b/todo
@@ -708,52 +708,33 @@ Output written on ProofGeneral.pdf (2 pages, 54702 bytes).
 
 =================================================================
 
-LIST OF THINGS FOR PG 3.4
-=========================
+List of things postponed from PG 3.4: need to be merged above
 
-** LATEST
+*** Stefan Monnier's big patch (Coq stuff, imenu, other)
 
--- Coq pbp focussing --- does this part work at least?  Test case.
--- Pierre's changes
--- Christophe's changes
+*** Isar tracing error: (error/warning) Error in process filter: (error Nesting too deep for parser)
 
-** X-SYMBOL PROBLEMS 
-    -- GNU emacs probs with Coq and friends.
-    -- Isabelle probs (electric token, latin1, sub/sup).
+*** Coq pbp focussing --- does this part work at least?  Test case.
 
-** Check all instantiations.
+*** Christophe's changes suggested for handling x-sym / highlighting.
 
-** Nested idiom spans:
-    - check nested 'idiom spans are removed in all cases.
-       (Maybe they should have type annotation after all?)
+*** Comment at the end for Isabelle theory files!!!!
 
-** GNU Emacs probs:
- Another miscellaneous hang: on "Exit Isabelle" after doing
- retraction because of part-way through processing a file.
+*** X-Symbol 4.4 backwards compatibility for Coq and friends.
 
-** Announce mailing list move, new test version.
+*** Check: does proof-follow-mode have any effect???  
+    Consider removal to simplify it?
 
-** Does proof-follow-mode have any effect???
+*** Fix-up show/hide for nested proofs.  (Wierdness with
+   cursor jumping as well)
 
-** Fix-up show/hide for nested proofs.  (Wierdness with cursor jumping as well)
+*** Cleanup undo behaviour to cope with new Coq mechanism.
 
-** Show/hide in FSF Emacs.
+ Is the simplified mechanism better for other provers too, or does the
+ split still apply?  Probably best to leave Isar as-is and have
+ proof-nesting-depth left as experimental.
 
-** Context menu for FSF Emacs.
+*** proof-nesting-depth:
+    This needs to be fixed up in count undos, find-and-forget.
 
-** Cleanup undo behaviour to cope with new Coq mechanism.
-   Is the simplified mechanism better for other provers too, or does the
-   split still apply?  Probably best to leave Isar as-is and have
-   proof-nesting-depth left as experimental.  (Branch?)
-
-** Cleanup Coq undo: discussion with Pierre clarified. 
-   Docs, variable names need improvement.
-
-** proof-shell-proof-completed
-  Doesn't behave right for Isabelle/Isar??
-
-** proof-nesting-depth:
-  This needs to be fixed up in count undos, find-and-forget.
-
-** Would be good to make count undos and find-and-forget generic.
-    [ Perhaps too tricky/temperamental to get this right ]
+*** Generic versions of count undos and find-and-forget generic.