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.

> 
>> 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).

> 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).

>  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.

> 
> 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).


> 
> 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.

> 
> 
>> 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.

Good.

Regards,

Rob.

Attachment: patch-2.9.1w2.rda.110814.rda.110903.gz
Description: GNU Zip compressed data

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to