Re: [ProofPower] How do you arrange Xpp?
Thanks to Mark and Artur for their feedback. We have one vote each way, so for the time being I won't change this. People like Mark with smallish screens should be aware that the window menu now has a Show/Hide Journal item as well as Show/Hide Script. Even when I using a big screen, I use these a lot when I am doing proofs (I set PPLINELENGTH so that ProofPower formats things to use the full width of the journal window when the script window is hidden). What I may do in a forthcoming version is add a toggle geometry item to the window menu so that the horizontal/vertical distinction can be made dynamically. Regards, Rob. On 22 Jul 2011, at 16:03, Mark wrote: I use Xpp in 1-window mode for general text editing, and I also 2-window mode for developing scripts. I want to develop my text with 80-character width, which is the industry standard. Like many, I only have a 1280x800 screen, and so horizontal mode means that the journal window is very squashed up if the script window stays at 80. So I prefer vertical. I bet Phil is now going to show off about his new, super-hidef screen laptop and suggest horizontal mode... :) Mark. on 22/7/11 3:10 PM, Rob Arthan r...@lemma-one.com wrote: I nearly always use Xpp with the following settings in $HOME/app-defaults/Xpp Xpp*script.rows:32 Xpp*script.columns: 60 Xpp*script.background: white Xpp*script.foreground: black Xpp*journal.rows: 32 Xpp*journal.columns:60 Xpp*namestring.columns: 24 Xpp*journal.background: light blue Xpp*journal.foreground: black Xpp*journal.editable: true Xpp*mainpanes.orientation: HORIZONTAL This differs from the out of the box default in laying out the windows side-by-side and letting you bring up the command dialogue by trying to type into the journal window. I am tempted to change the default settings to the above - it looks a bit less like a standard Motif application, but it makes much better use of modern screens (or at least modern screens that have a landscape aspect ratio). It would be nice to know what other people do before I commit to this change. So please let me know your preferences. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] How do you arrange Xpp?
I meant to add that I always use horizontal mode, so that would have got my vote as Mark predicted! A dynamic toggle would be very useful, I think. Phil On 27/07/11 13:37, Rob Arthan wrote: Thanks to Mark and Artur for their feedback. We have one vote each way, so for the time being I won't change this. People like Mark with smallish screens should be aware that the window menu now has a Show/Hide Journal item as well as Show/Hide Script. Even when I using a big screen, I use these a lot when I am doing proofs (I set PPLINELENGTH so that ProofPower formats things to use the full width of the journal window when the script window is hidden). What I may do in a forthcoming version is add a toggle geometry item to the window menu so that the horizontal/vertical distinction can be made dynamically. Regards, Rob. On 22 Jul 2011, at 16:03, Mark wrote: I use Xpp in 1-window mode for general text editing, and I also 2-window mode for developing scripts. I want to develop my text with 80-character width, which is the industry standard. Like many, I only have a 1280x800 screen, and so horizontal mode means that the journal window is very squashed up if the script window stays at 80. So I prefer vertical. I bet Phil is now going to show off about his new, super-hidef screen laptop and suggest horizontal mode... :) Mark. on 22/7/11 3:10 PM, Rob Arthan r...@lemma-one.com mailto:r...@lemma-one.com wrote: I nearly always use Xpp with the following settings in $HOME/app-defaults/Xpp Xpp*script.rows: 32 Xpp*script.columns: 60 Xpp*script.background: white Xpp*script.foreground: black Xpp*journal.rows: 32 Xpp*journal.columns: 60 Xpp*namestring.columns: 24 Xpp*journal.background: light blue Xpp*journal.foreground: black Xpp*journal.editable: true Xpp*mainpanes.orientation: HORIZONTAL This differs from the out of the box default in laying out the windows side-by-side and letting you bring up the command dialogue by trying to type into the journal window. I am tempted to change the default settings to the above - it looks a bit less like a standard Motif application, but it makes much better use of modern screens (or at least modern screens that have a landscape aspect ratio). It would be nice to know what other people do before I commit to this change. So please let me know your preferences. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com mailto:Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Experimental OpenProofPower release 2.9.1w2.rda.110727
Dear All, It has taken a little bit longer than I would have hoped but I have just completed a new experimental release of OpenProofPower. You can find it here: http://www.lemma-one.com/ProofPower/getting/experimental/OpenProofPower-2.9.1w2.rda.110727.tgz The idea is that an experimental release is a step toward the next stable version (2.9.2 in this case). There may be additional working versions 2.9.1wN to fix problems, but the interfaces in the working versions will be stable within one release. The experimental release directory also contains changed versions of other items, e.g., the mathematical case studies, if those need to be updated for the experimental release. See the CHANGES file for details of the changes relative to 2.9.1w2, but some noteworthy changes relative to 2.9.1w2.rda.110226 are: a) Rewriting with higher-order matching is now supported in HOL. It is enabled using the component proof context 'sho_rw (short for: simple higher-order rewriting). As an example, higher-order rewriting with the theorem prenex_clauses will put a formula in prenex normal form. See if the following turns you into an intuitionist: merge_pcs_rule1 [predicates, 'sho_rw] rewrite_rule[prenex_clauses] induction_thm; b) Thanks to Phil Clayton, ProofPower-Z now supports empty declaration parts in paragraphs (as well as in expressions which were already supported, also thanks to Phil, in 2.9.1w2.rda.110226). c) The guillemet brackets that are used in Spivey Z and ISO Standard Z around the domains of the constructors in a free type definition are now supported in ProofPower-Z. These brackets are entered as %% and %% and are typeset as in the Z Reference Manual or the ISO Standard LaTeX mark-up. The brackets are defined as an outfix operator in the toolkit with defining property %% x %% = x. So you can use them as a general purpose form of brackets that are not eliminated automatically by the parser. d) You can now use == as an alternative to %def% in abbreviation definitions and binding displays in ProofPower-Z. e) There are new underlining bracket characters in the font. These appear on screen as underlined brackets and cause the text they enclose to be underlined when typeset. f) A new operator is defined in ProofPower-Z whose name is _ %ulbegin% _ %ulend% _ (where %ulbegin% and %ulend% are the ASCII names for the underlining bracket characters - so this typesets as three underscores with the middle one underlined). It is defined so that x %ulbegin% R %ulend% y holds iff (x, y) is a member of the relation R. This effectively generalises the feature in Spivey Z whereby underlined identifiers act as infix relation symbols. In ProofPower-Z you can now use any expression as an infix relation by underlining it. My thanks to everyone who has helped with this release and my apologies to anyone who contributed requests for features that haven't been implemented yet. Your requests are much appreciated and are on the to-do list. Regards, Rob.___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
