More jEdit Tool Support

[Daniel Spiewak]

I mentioned previously that I have created a jEdit mode for SASyLF.
Unfortunately, that mode doesn't really do much more than syntax
highlight and auto-indent. It's nifty, but lacking in completeness.
So, taking another step toward a fully-featured SASyLF IDE, I have now
created a Commando command for SASyLF, as well as a series of regular
expressions designed to parse the SASyLF output and produce error
annotations within the editor. Unfortunately, these two features are
a little more-than-trivial to enable (even with my magic XML files),
so if you want this to work, you're going to have to put in a little
elbow grease. Note that this guide assumes that you have already
installed the SASyLF editor mode

1. Install the "Console" and "ErrorList" plugins within jEdit using
Plugin Manager
2. Get the command mode from here: http://www.cs.uwm.edu/~dspiewak/jedit/commando/sasylf.xml
3. Install this XML file into ~/.jedit/console/commando
4. If jEdit is running, select Plugins>A-K>Console>Regen dynamic menus
5. Select Plugins>Plugin Options
6. On the left, select Console>Compile & Run
7. Scroll down until you see the entry for "sasylf" (it's at the very
bottom, *not* alphabetical)
8. In the first column ("Compiler"), select "sasylf" from the drop-
down list for the "sasylf" entry (from left to right, the line should
now read "sasylf sasylf none")
9. Mash down on the "OK" button

Thus ends phase one. You should now be able to invoke the "Compile
Current Buffer..." command from the Console sub-menu (used earlier to
regen). I have this command mapped to C+B (you can do this from
Utilities>Global Options...>Shortcuts).

When editing a .slf file, this will pop up a dialog box with a single
input field labeled "Path to SASyLF". The value of this field will be
pre-filled to "~/cs732/bin/sasylf" (reflecting my system). Change
this to the *fully-qualified* path to the sasylf command. Note that
you can change this default by editing the XML file downloaded in step
#2. Just look for the line which has the above text; can't miss it.

Once your file paths are all happy, hit the "OK" button in the build
dialog. The Console pane will open and SASyLF will be invoked against
your currently-open file. If all goes well, you will be able to read
the SASyLF output within the console pane.

In order to get error annotations within the editor pane, you have to
proceed to phase two.

1. Select Plugins>Plugin Options...
2. On the right, select Console>Error Patterns
3. Toward the bottom of the dialog, select the "+" button and enter
"SASyLF" in the ensuing dialog
4. Enter the following values in the corresponding fields:

Error Regexp: ([^\.]+\.slf):(\d+) ([^w].+)
Warning Regexp: ([^\.]+\.slf):(\d+) warning: (([^f]).+)
Filename: $1
Line number: $2
Error message: $3

5. [Optional] If you like, you may paste some example SASyLF output
in the "Test Area" and check your expressions using the "Test/Commit"
button. Try this step if something doesn't work at the end.
6. Select "OK"

After the above is completed, you should be able to build SASyLF and
then see errors underlined in the editor as red, warnings underlined
as yellow. Note that the ubiquitous "forward reference to theorem"
warning is not highlighted to avoid clutter.

As always, if you have any questions, comments or problems, please
ask.

Daniel

[Daniel Spiewak]

Oh, I forgot to mention. You can mouse over the error highlights and
see what the error message is in a hover (Eclipse-style). Very useful
for tracking down errors quickly in a large proof.

Daniel