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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to