From 7298e49425de3576c740fc7eab655835f7d28315 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 12 Jan 2000 14:05:56 +0000
Subject: Note about X-Symbol problems.

---
 CHANGES | 3 +++
 todo    | 9 +++++++++
 2 files changed, 12 insertions(+)

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.
 
-- 
cgit v1.2.3