The proof-pad-classic from calebegg

Maybe also hide error highlights if admission is successful?

Write some better tooltips for commonly used functions

GenerateData.java:59

Clean up error message for stack overflow

Make error highlight more visible?

Saving/Compiling User Experience

On Windows, the save dialog doesn't filter .lisp files. So, if there were .lisp files in the directory, you don't only see those... conversely, the default is to save the current file without an extension. The same thing happens when compiling: there is no default extension and no indication of what extension to use.

Edit: in the latest version, selecting the "lisp files" filter also excludes directories. This is not the expected behavior.

Parser: Check for redefinition

Example:

(defun prod ...)

(defthm prod ...)

The second prod should be underlined with "This function name is already in use" as the tooltip.

Don't move output window if it's visible. Or remember its last location.

Only show error popup if there were no parser errors in that exp

Multi-line symbol lists

Proof bar out of sync with prover

If you put two commands on the same line, you can get ACL2 out of sync with the proof bar. For example, submit and then undo:

(defun a () 1) (defun b() 2)

When it goes undone, :u is only sent once, leaving a defined.

Make read only code easier to understand

Several people didn't get the grey = read only. Not sure what the best thing to do here would be

I have two things I'd like to experiment with:

Flash the proof bar when clicking on read-only code
(Matthew's idea): Allow the cursor to be placed, then automatically undo if they type anything.

Interrupt ACL2 (^C) on Windows

ACL2s's technique kind of sucks:

http://acl2s.ccs.neu.edu/acl2s/doc/impl.html#impl_acl2_wrap

Also, when I tried it, it messed with Swing's painting events. It seems to permanently steal focus from Swing.

I tried getting this working with some Stack Overflow advice and C#, but was not successful. I might try again at some point.

Add `ld` to lexer

Installation Directory on Windows

The 64-bit version automatically selects C:\Program Files(x86) as the install location. It should choose C:\Program Files\ instead.

Find submenu

Apple HIG says: "Provide a Find submenu, if appropriate. You might want to include a Find submenu if find is important functionality in your app. Typically, a Find submenu contains Find (Command-F), Find Next (Command-G), Find Previous (Command-Shift-G), Use Selection for Find (Command-E), and Jump to Selection (Command-J). If you include a Find submenu, the Find menu item name should not include an ellipsis character."

Automatically ^C after 5 s in :program mode auto-admission

Currently, during the automatic :program mode admission, if an expression goes on for a while (such as if the user types a long or infinite calculation in the definitions area) there's no way to regain control (besides explicitly ^Cing). Anything that takes longer than 5s should just be automatically stopped, since it's probably not helpful.

Special case error summaries for common functions?

Eg "zp expects natural numbers, ..."

Parser: Underline defproperty if book hasn't been included

Update recent menu on save too

Automatically include current directory in include-book dialog

Session saving: fail gracefully on lab computers

Autosave

(if (cons ...) ...) warning

Should be consp, almost certainly.

Event hoisting should add below proof line

For some reason (regression?), hoisted events are getting added to the end of the file instead of the proof line, which results in a different form getting auto- admitted.

Ability to add new directories to the include-book dialog box

Macros with multiple outputted top-level expressions

These break the system that checks for the admission index.

Example: defrandom, mini-proveall

Error doesn't show up when hovering below

| x |
|   |
|———|
| m |

m = mouse

When the mouse is here, and you click, the error in the part above gets instantly obscured by the arrow that shows what will admit when you click.

Keyboard shortcut for 'trace'

Maybe ctrl/cmd + enter

Progress bar for proofs

I think the proof tree is basically useless. Except as a sort of progress bar so you can tell when the proof attempt is going south.

I'm thinking it should have a proved / total fraction displayed somewhere prominently alongside a progress bar. It's kind of crappy because the "progress" bar will probably go backwards sometimes, which isn't really what those are supposed to do.

Well, maybe not, actually; if the progress bar is subdivided into equal segments representing the top level nodes of the proof tree and then further subdivided lower down, like a one dimensional tree map, that could work. I don't know if it would be more or less useful than a progress bar that goes backwards sometimes.

REPL-collapsing/expanding arrows are confusing/not useful

Replace them with a show/hide repl option, perhaps.

Opening file from disk opens a blank window as well

Optionally add close parens automatically

Freeze when opening certain files

I opened a file that contains lots of proofs, some of which don't admit (and instead cause the theorem prover to just spin and spin). The proof pad UI hangs because

a form gets sent to Acl.admit that ACL2 will work indefinitely of
lots of forms get sent to Acl2.admit
the output stream buffer fills up
Acl2.admit's flush() hangs

I think it would make sense to change admit so that the worker thread does the flushing as well as the reading-back. That way, the prover might work indefinitely, but the UI will not hang.

"Look up" menu item: either update/disable it when invalid, or make it show a prompt

Something like "There's no help for xs. Look up something else? [_____]" (if your cursor is on/near 'xs')

Callout box for offscreen errors

Parser: Functions in wrong order

(defun f () (f-helper))
(defun f-helper () ...)

First f-helper should have a tooltip that says "Functions in ACL2 must occur below all the functions they call" or similar.

Save output pane contents

Make the menus follow HIGs

Right now, the menus are more or less in the OS X ordering/configuration. Some tweaks would make this better on Windows/Linux.

http://msdn.microsoft.com/en-us/library/windows/desktop/aa511502.aspx#standardMenus

http://developer.gnome.org/hig-book/3.0/menus-standard.html.en

#| This #| is |# nested. |#

will only highlight as a comment until the first |#.

calebegg / proof-pad-classic Goto Github PK

proof-pad-classic's People

Contributors

Stargazers

Watchers

Forkers

proof-pad-classic's Issues

Recommend Projects

Recommend Topics

Recommend Org