diff options
-rw-r--r-- | CHANGES | 7 | ||||
-rw-r--r-- | FAQ | 7 | ||||
-rw-r--r-- | Makefile.devel | 2 | ||||
-rw-r--r-- | todo | 151 |
4 files changed, 83 insertions, 84 deletions
@@ -137,8 +137,11 @@ Reduce contrast for mouse highlighting of regions. *** Added `proof-shell-identifier-under-mouse-cmd' Allows PG to conveniently send a command to the prover which passes -the identifier under the mouse as an argument. Bound globally to -Control-Meta-Mouse-button1. +the identifier under the mouse, or the active region, as an argument. +Bound globally to Control-Meta-Mouse-button1. + +Presently only configured in Isabelle/Isar, to parse terms (inside +strings) and theorems (outside). ** GNU Emacs compatibility, simplified font-lock, handling nested comments @@ -47,7 +47,12 @@ A. This is an XEmacs bug. What you can do is prevent the use ----------------------------------------------------------------- -Q. I have a problem installing/using Proof General, what can I do? +Q. I have a problem installing/using Proof General. + For example, I see the message + + (file-error "Cannot open load file" "executable") + + when I start the program. A. Please check the documentation carefully, particularly the requirements for a full-featured and recent Emacs version, as diff --git a/Makefile.devel b/Makefile.devel index bab65e27..f1499679 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -232,7 +232,7 @@ tags: $(EL) # with a way of cleaning the last day from the ChangeLog. # ChangeLog: FORCE - rcs2log -h "dcs.ed.ac.uk" $(DEVELOPERS) | sed 's|/home/proofgen/src/ProofGeneral/||g' > ChangeLog.prefix + rcs2log -h "dcs.ed.ac.uk" $(DEVELOPERS) -i 4 | sed 's|/home/proofgen/src/ProofGeneral/||g' > ChangeLog.prefix if [ -f ChangeLog ]; then mv ChangeLog ChangeLog.old; else echo > ChangeLog.old; fi cat ChangeLog.prefix ChangeLog.old > ChangeLog rm ChangeLog.prefix ChangeLog.old @@ -6,6 +6,10 @@ This is an outline file. Use C-c C-n, C-c C-p or menu to navigate. * Proof General Short List of Things to Do for next version +*** Emacs Bug Roundup + --- xemacs support for nested comments + --- xemacs undo in read-only regions + *** Clean up X-symbol support -- token configuration for latest version of X-Symbol (Gerwin Klein) -- remove on/off setting for all buffers (too slow), use @@ -58,50 +62,24 @@ X (Low) e.g. probably not worth spending time on *** [ Don't query save before retraction ?? ] -*** A settings configuration for Isabelle: add backwards - compatibility for older versions of Isabelle. - Waiting for Isabelle to provide some easy version - checking. - -*** B Cleanup display during settings processing. +*** C Implement optional arg to next/undo which doesn't update + display (so user can retain something else on screen) *** A fix display anomaly for Isar output with shrink windows: display splits window unexpectedly. -*** B document and simplify proof-script-span-context-menu-extensions - -*** C Add output highlighting to minibuffer in proof-shell-message. - (Quite tricky to get text properties onto text in minibuffer...) - -*** X A more flexible way of choosing which instance of PG we want, - allowing matches on the buffer before choosing the mode function. - -*** D Isabelle PG: Non-blocking for .thy loading from .ML files. +*** B Cleanup display during settings processing. *** B Generic adjusting of pretty-printer line width (currently implemented in several instances) -*** D Make code robust against accidental buffer kills - by regenerating auxiliary buffers automatically. - -*** D Bugs with extents: - Sometimes probs if try to assert a whole file while one is - being processed: (proof-set-queue-start end) call in - proof-done-advancing finds that queue span is detached. - Code is now robust for this. But why detach anyway? - -*** C Extensions with semantic tokens - Look at the Semantic Navigator package. Implements persistent - database of tokens. +*** B document and simplify proof-script-span-context-menu-extensions *** B Documentation: Check new doc for hiding; add doc for dependencies, tracing. Moving spans; navigating through locked region. Favourite menu. -*** C Fix byte compilation - Problem with proof-ass macro mechanism -- gets expanded during compilation. - *** B generalize from Isabelle's "atomic scripting" theory file mode to allow other instances which do not allow incremental processing of files in major or auxiliary file types. @@ -110,56 +88,60 @@ X (Low) e.g. probably not worth spending time on *** B Move over to new better designed parsing function mechanism. +*** B Generalize electric terminator mode for other parsing mechanisms. + +*** B Add parameter for help function so HOL help works nicely + +*** C Add output highlighting to minibuffer in proof-shell-message. + (Quite tricky to get text properties onto text in minibuffer...) + +*** C Extensions with semantic tokens + Look at the Semantic Navigator package. Implements persistent + database of tokens. + +*** C Fix byte compilation + Problem with proof-ass macro mechanism -- gets expanded during compilation. + +*** D Isabelle PG: Non-blocking for .thy loading from .ML files. + +*** D Bugs with extents: + Sometimes probs if try to assert a whole file while one is + being processed: (proof-set-queue-start end) call in + proof-done-advancing finds that queue span is detached. + Code is now robust for this. But why detach anyway? + *** D ChangeLog generation still not right. Probs: duplicated entries when runs several times in same day. Suggested fix: use rcs2log to generate the entire log, just take a sensible number of lines from it. (Ideal would be to get until a given date) -*** C Fix the doc makefiles to adapt the image flag in PG-adapting.tex - properly, for dvi/ps targets - -*** B Generalize electric terminator mode for other parsing mechanisms. +*** B proof-shell-restart should clear response buffer (only noticed with + proof-tidy-response=nil) -*** B Add parameter for help function so HOL help works nicely +*** B TESTING. + - Add automatic testing mechanism to test user-level functions PG + - Test schedule for things to try with a new instantiation -*** D Make tags support in lego.el and coq.el a bit more generic. - Use customization option proof-tags-support. +*** B Add a new configuration setting for matching proof commands + which have no undo effect --- should be treated like comments + for undo. Perhaps would be useful for Isabelle, HOL, at least, + although it's tricky to see how it would be completely *safe*. + [ See discussion with Pierre re Coq undo command categories ] -*** D Display functions: does auto-delete-windows work with - window-dedicated as it should? (I thought it would switch - between 2/3 bufs as appropriate?). +*** C Fix the doc makefiles to adapt the image flag in PG-adapting.tex + properly, for dvi/ps targets *** C Clean up assert-until-point stuff: should have just one function, as a subroutine of assert-next-command; and no bizarre never-used arguments! -*** B proof-shell-restart should clear response buffer (only noticed with - proof-tidy-response=nil) - -*** D Continue programme of making adaptation easier. - -*** D Fix up sources to conform to library header conventions - see (lispref)Library Headers. - -*** D Proof shell exit function -- could try sending an interrupt first - if the process is busy, just to be polite (and avoid the 10 second - wait before it gets killed). - *** C make pretty printer line width altering generic. 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). -*** D X-Symbol: is there a function to input in the minibuffer using - a token language? - -*** D Investigate possible toolbar refresh problems. - Sometimes extra clicks *are* needed. Why? - -*** C Consider supporting imenu instead, or as well as, func-menu. - *** C Improved configurability of command settings, etc. We should let command settings, etc, be a special type which can be one of three things: @@ -188,14 +170,7 @@ X (Low) e.g. probably not worth spending time on mechanism in shell buffer: use M-n M-p to scroll up and down through previous and forthcoming (matching) commands. -*** B TESTING. - - Add automatic testing mechanism to test user-level functions PG - - Test schedule for things to try with a new instantiation - -*** D Is there a way to make colours defined for x work in mswindows too? - - defface specs with (type x) seem to work fine with (type mswindows) too. - Hassle to duplicate, is there an easy way to cover both? +*** C Consider supporting imenu instead, or as well as, func-menu. *** C Improve proof-easy-config mechanism. @@ -205,11 +180,32 @@ X (Low) e.g. probably not worth spending time on Use custom to set everything to its default value from proof-config, before invoking the body. -*** B Add a new configuration setting for matching proof commands - which have no undo effect --- should be treated like comments - for undo. Perhaps would be useful for Isabelle, HOL, at least, - although it's tricky to see how it would be completely *safe*. - [ See discussion with Pierre re Coq undo command categories ] +*** D Make tags support in lego.el and coq.el a bit more generic. + Use customization option proof-tags-support. + +*** D Display functions: does auto-delete-windows work with + window-dedicated as it should? (I thought it would switch + between 2/3 bufs as appropriate?). + +*** D Continue programme of making adaptation easier. + +*** D Fix up sources to conform to library header conventions + see (lispref)Library Headers. + +*** D Proof shell exit function -- could try sending an interrupt first + if the process is busy, just to be polite (and avoid the 10 second + wait before it gets killed). + +*** D X-Symbol: is there a function to input in the minibuffer using + a token language? + +*** D Investigate possible toolbar refresh problems. + Sometimes extra clicks *are* needed. Why? + +*** D Is there a way to make colours defined for x work in mswindows too? + + defface specs with (type x) seem to work fine with (type mswindows) too. + Hassle to duplicate, is there an easy way to cover both? *** C Implement proof-generic-find-and-forget <...>-count-undos, to simplify prover-specific code. @@ -420,7 +416,6 @@ X (Low) e.g. probably not worth spending time on a long buffer. Generally a performance problem with proof-segment-up-to. - *** D Implement proof-find-previous-terminator and bind it to C-c C-a (45min) @@ -461,6 +456,8 @@ X (Low) e.g. probably not worth spending time on [Maybe a design principle is that spans should coincide with undoable regions] +*** X A more flexible way of choosing which instance of PG we want, + allowing matches on the buffer before choosing the mode function. ** 3. Things to do for the documentation @@ -752,14 +749,8 @@ Output written on ProofGeneral.pdf (2 pages, 54702 bytes). List of things postponed from PG 3.4: need to be merged above -*** Stefan Monnier's big patch (Coq stuff, imenu, other) - -*** Isar tracing error: (error/warning) Error in process filter: (error Nesting too deep for parser) - *** Coq pbp focussing --- does this part work at least? Test case. -*** Christophe's changes suggested for handling x-sym / highlighting. - *** Comment at the end for Isabelle theory files!!!! *** X-Symbol 4.4 backwards compatibility for Coq and friends. |