Rob,
Thanks for the latest release. I have been using this for a while now
and have a few comments.
On 14/08/11 16:18, Rob Arthan wrote:
a) For visual compatibility with the ISO standard, a symbol for unary
minus in Z has been added to the font and defined as a synonym of the
unary minus written as a tilde in the theory z_numbers. The symbol
displays and typesets as short minus sign. %cat%/ (i.e., a frown
followed by a backslash) is now defined as an alias for distributed
concatenation written %dcat% in the theory z_sequences.
The new minus sign appears to be missing from the palette. (Am I going
blind?)
b) In xpp, you can now switch dynamically between the horizontal and
vertical layout using a new item in the window geometry. N.b., this is
accompanied by a change in the way you specify the initial layout and
geometry in app-defaults/Xpp. See the CHANGES file for more details.
The switching is useful. A few observations:
1. When there is no journal window, Show Geometry causes a crash:
xpp: fatal error: signal 11: memory fault: ...
(It may not crash the first time.) Also, Ctrl+T causes a crash, even
though there is no menu item Toggle Geometry without a journal window.
2. I have an issue with the design when using horizontal mode. My
app-defaults/Xpp sets column widths assuming there will be a journal
window. However, I am often opening file just to view/edit, i.e. no
journal window, and always have to resize the window which is far too
wide. I would have a similar issue the other way around. Is it
possible for the width of the editor window to be the same whether or
not Xpp is started with a journal window?
For vertical mode, the current behaviour seems preferable. I think
different behaviour for the different orientations makes sense because
of the asymmetric nature of documents: bounded width, unbounded height.
3. Given the above observation about document shape, should toggling
attempt to maintain width by resizing the Xpp window? I have had
various ideas along these lines. Have you thought about that?
c) z_%forall%_intro_conv1 and z_%exists%_intro_conv1 no longer fail if
bound variables declared by schemas-as-declarations had been renamed.
Instead they introduce schema renamings as necessary to convert the
declarations back into valid Z. This fixes a bug reported by Phil
Clayton whereby stripping either failed or produced a result that was
not fully simplified.
Thanks, this is working now.
Phil
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
