From 3b33deaeb9c34d37917ec06427e063c4a4235518 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 10 Nov 1999 18:12:23 +0000 Subject: Latest todos --- todo | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/todo b/todo index 69673a8d..4d7a0ab9 100644 --- a/todo +++ b/todo @@ -47,19 +47,39 @@ A Pending work, in progress [da]: re-enabled), proof-toggle-scripting, new configuration options. proof-cd - more 3.0 issues: extending the queue region, being more lax - about proof-shell-busy. + about proof-shell-busy. - Fix sentinel infinite loop bug - noticeable delay when loading ML files for Isabelle (fontification?) +A Markus's bug reminder list: + - cut&paste from hilited Isabelle output includes invisible specials; + - c-c c-c does not work reliably; + - c-c c-a is broken; + +A bug in response filtering: + The response filtering seems to have changed again. E.g. 'Info' button in + PG/isar (without a theory context) omits most of the result (commands, + ...). + +A Bugs in x-symbol support: + - visiting multiple files sometimes doesn't display them properly + (setq x-symbol-8bits nil) needed? + - local variables messages about "isa" being unset + - response buffer sometimes not decoded (or 8bit prob again). + B Fixing up PBP: things almost work for lego (apart from getting pbp wrong!) -- there is a bug with (newline-and-indent) though which tries to write into the locked region for some reason. +C Make a generic hook (or hook-constructing macro) to adjust + pretty printer line widths, a la LEGO. Maybe find a better + place to do this that in the proof-shell-insert-hook (should + be triggered by resize events). + C IDEAS FOR SIMPLIFIED PROVER INSTANTIATION. We could make extensive use of defvaralias to automatically declare the settings for each proof assistant. Then the tedious "shadowing" (or copying) is done automatically. - e.g. C Improved configurability of command settings, etc. We should let command settings, etc, be a special type -- cgit v1.2.3