The Community Z Tools plugin displays a dockable window listing important Z characters and Z constructs, plus several buttons for running the CZT tools. The plugin currently supports two markup formats for Z: the LaTeX markup and the Unicode markup.
You can simply click on a Z character or construct to insert it into your current buffer, using the currently selected markup. The top line ("Paragraphs") inserts complete Z paragraphs, with uppercase placeholders for the parts that you should fill in, while most of the other constructs insert just one Z symbol or operator. For example, clicking on "Sch[]", with LaTeX markup selected, will insert a generic schema construct, like this:
\begin{schema}{NAME}[ TYPE ] DECLS \where PREDS \end{schema}You should replace NAME by the name of your schema, TYPE by the generic type parameter(s), DECLS by a sequence of declarations and PREDS by a sequence of predicates.
The combo box at the left top corner of the plugin allows you to choose which markup you wish to use. This is initialized to "LaTeX Markup" each time you start jEdit, but you can change the markup at any time using this combo box. The usual goal is to set it to reflect the contents of the buffer you are editing. Your choice of markup has two effects:
The "Typecheck" button parses and typechecks the file in the current buffer. It always uses the file contents, rather than the current buffer contents. If the current buffer contains unsaved changes, you will be asked whether you want to continue. Saying "Yes" will continue with the parsing using the on-disk version, which will not contain your unsaved changes. Saying "No" stops the parsing and allows you to save the buffer. The result of the typechecking is displayed in the jEdit status bar. Any errors can be viewed using the ErrorList plugin.
The other two buttons in the CZT plugin convert the file in the current buffer into other markup formats. The specification can be converted to Unicode if LaTeX markup is chosen (or into LaTeX if Unicode markup is chosen), or can be translated into ZML -- XML markup for Z. If parsing and translating was successful, a new temporary buffer containing the output of the conversion is opened. In case of an error, the error list can be consulted.
Hints:
x'
,
use the '
character from the "Schemas" line of
the CZT plugin. (In LaTeX, this just inserts the normal ASCII
prime character, but in Unicode it inserts a special prime
symbol. To prime a schema or expression, you must put a
space inbetween the schema name and the prime. This space
must be a normal space character in Unicode markup, but a special
spacing command like tilde (~
) in LaTeX markup.\_
,
newlines as \\
and spaces as ~
.
In Unicode markup these can just be written as normal
ASCII characters.+
by the superscript that you want.
\
)
but is different (it is bolder and more sloped). The schema
hiding operator is also visually similar, but is even larger
and bolder.