aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-05-12 17:28:52 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-05-12 17:28:52 +0000
commitce7ed629d5d43cce6b3118cdbc6244c70b8e4113 (patch)
tree4260559a469590558be97b21d6aed2d05d7ec2bd
parentada49d04eccf9f94831ad7498cac436ecfbffd40 (diff)
Notes about fixing docstring-magic.
-rw-r--r--doc/docstring-magic.el6
-rw-r--r--todo7
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.