Rob,
On 04/09/11 11:49, Rob Arthan wrote:
Phil,
On 3 Sep 2011, at 20:01, Phil Clayton wrote:
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?)
It should be at row 6 column 3, just right of greater-than-or-equals.
My fault. For some reason I failed to merge that line of the new Xpp
file into the one in my home directory. (Normally I merge in the
opposite direction to avoid this happening.)
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.
I have attached a patch that fixes these two (which were intermittent/system
dependent).
Thanks, that fixes it.
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.
But you "far too wide" may be another user's "very nice" (see below).
If there are users who want as much width as possible, then I suppose so.
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?
That is exactly the old behaviour which is bad for people who like to use the
horizontal layout even on smallish screens. The only way to keep everybody
happy is to have separate resources for the width and height of an edit-only
session.
The extra configuration would be appreciated by me but, while I'm the
only one, perhaps it is not worth doing.
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.
That's not really a valid assumption: you may worry about keeping your source
files within a fixed width. but many people don't. When entering text, it is
quite common to use carriage-returns only to separate paragraphs or sentences
and this logical arrangement is convenient for many reasons, e.g., when
searching for phrases. Likewise, in code, many people prefer long lines to
artificially inserted line breaks with no logical significance. (A
line-wrapping mode for formal text in ProofPower documents is on my wish-list).
There are pros and cons. I find it useful to make the text fit e.g. 80
columns not just for general readability but to get a decent view of two
source files on the screen at once. This especially helps
comparing/merging side by side and working with a journal window (which
has sizeable output).
(Even with a line wrapping mode for formal text, I would stick to N
columns because other tools, e.g. visual diff programs, would not have
such a line wrapping mode.)
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?
Aside from my reservations above, it is generally considered to be bad practice
for X applications to resize or move top-level windows programmatically once
they are created unless there is some really compelling reason in the
application logic for doing this. The results of trying to do so are dependent
on the window manager and many window managers will just ignore resize requests
from the program.
Yes, I wondered if it was bad practice for the window to resize itself.
Phil
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
