Note about X-Symbol problems.

2 files changed, 12 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 4e566cbb..76fadd98 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,6 +8,9 @@ Generic Changes
 Minor bug fix for duplicated short output.
  (set proof-shell-eager-annotation-start-length appropriately)
 
+Bug fix with .thy files and X-Symbol mode: subsequently visited
+ theory files would have X-Symbols broken.  (NB: Fix in progress)
+
 
 Coq Changes
 -----------
diff --git a/todo b/todo
index 0439cbd0..2b8e7acb 100644
--- a/todo
+++ b/todo
@@ -49,6 +49,15 @@ B Manual improvements before techreport publishing (see notes at end also):
   - add screenshots?
   - add more index entries
 
+C X-Symbol support for theory files: bugs at the moment, because
+  of duplicate calls to proof-x-symbol-mode and mess with
+  font-lock initialization.  Problem with current version:
+  visit a.thy, b.thy then turn on xsym.  Broken in b.thy.
+  Seems okay visiting new buffers after that.
+  Must also check interaction with xsym-isa-latex stuff,
+  may be broken by removal of mode hook settings.
+  (May need to split extra modes into two parts?)
+
 C Investigate support under Mule.  Suggestion we need to set
   process-coding-system-alist somehow to prevent coding.