From ce7ed629d5d43cce6b3118cdbc6244c70b8e4113 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 12 May 2000 17:28:52 +0000
Subject: Notes about fixing docstring-magic.

---
 doc/docstring-magic.el | 6 ++++--
 todo                   | 7 +++++++
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/doc/docstring-magic.el b/doc/docstring-magic.el
index 2f7bd6c8..f136c8cd 100644
--- a/doc/docstring-magic.el
+++ b/doc/docstring-magic.el
@@ -15,14 +15,16 @@
 (load "proof-config.el")
 (load "proof.el")
 (load "proof-toolbar.el")
-;; New ones first incase they duplicate variable names
-;; accidently. 
+
+;; FIXME: Loading several prover files at once is a bit of a problem
+;; with new config mechanism.
 (load "isar.el")
 (load "plastic.el")
 (load "isa.el")
 (load "thy-mode.el")
 (load "coq.el")
 (load "lego.el")
+(load "hol98.el")
 ;; A couple of comint symbols are mentioned in the docs
 (require 'comint)
 
diff --git a/todo b/todo
index 80bfdf75..3ccb19c2 100644
--- a/todo
+++ b/todo
@@ -27,6 +27,13 @@ D		e.g. desirable to fix at some point
 X (Low)		e.g. probably not worth spending time on
 
 
+*** Extremely urgent bits
+
+A Fix docstring-magic somehow so that multiple instances of PG can
+  be loaded at the same time.  Looks like will have to redefine
+  the proof-assistant specific settings one by one, before calling
+  the specific code.
+
 *** Outstanding bugs to investigate
 
 A find C-c C-l binding and remove it.  Overriden with goto-end-of-locked.
-- 
cgit v1.2.3