Rob,
28/03/15 16:03, Rob Arthan wrote:
On 27 Mar 2015, at 14:41, Phil Clayton <phil.clay...@lineone.net
<mailto:phil.clay...@lineone.net>> wrote:
You currently have
208D SUBSCRIPT LEFT PARENTHESIS for %ulbegin%
208E SUBSCRIPT RIGHT PARENTHESIS for %ulend%
but these parentheses don't have underscores like the ProofPower
glyphs. One option is
298B LEFT SQUARE BRACKET WITH UNDERBAR
298C RIGHT SQUARE BRACKET WITH UNDERBAR
They appear as ⦋ (298B) and ⦌ (298C) but I think they're too close to
refinement symbols. I think this could be a case where you probably
want to combine another glyph with the existing parenthesis using the
combining diacritics. I think the best options are
0331 COMBINING MACRON BELOW
which gives ̱( ̱)
These work in my email client and terminal. Alternatively
0332 COMBINING LOW LINE
which gives (̲ )̲
These don't overlay correctly in my email client or terminal but are a
single wide character.
I am chary about using the COMBINING characters as it seems likely to
increase the chances that any given text-processing system will go wrong
in some way. The use of underlined brackets in the ProofPower font was a
bit of an arbitrary choice. So I have changed to the following which
look like the beginning and end of underlining.
2A3D RIGHTHAND INTERIOR PRODUCT: ⨽
2A3C INTERIOR PRODUCT: ⨼
I agree that it could be too soon to depend on combining characters.
The less common ones aren't quite working on my 3-4 year old Linux
installation. These new characters don't sit quite as low as one would
like, to emphasize underlining, but I can't suggest anything better
without combining characters.
For epsilon, I can see why
03F5 GREEK LUNATE EPSILON SYMBOL
has been used instead of
03B5 GREEK SMALL LETTER EPSILON
- it is the correct shape for the equivalent LaTeX character.
I don’t know why we used \varepsilon in LaTeX rather than \epsilon for
this. (I think there is slight tendency to use the lunate epsilon for
the Hilbert choice operator in the literature, but the ordinary is often
used too and seems to be more common these days, and in Z you expect it
just to be the ordinary greek letter.)
l
I was finding that the lunate epsilon is very similar to the
membership operator. The lower case LaTeX mathematical greek letters
appear italicized so I wonder whether the standard should have used e.g.
𝜃 (1D703) instead of θ (03B8)
𝜆 (1D706) instead of λ (03BB)
𝜇 (1D707) instead of μ (03BC)
so you would have chosen
𝜖 (1D716) instead of ϵ (03F5)
That would have meant also that any Greek authors of Z don't find
themselves deprived of certain letters. As things stand, I agree with
your choice.
I think it is an excellent idea to use the mathematical greek letters. I
have done that, fixing a mistake with 𝜓 in passing and treating epsilon
the same as all the others now.
I wasn't sure about the uppercase greek letters because the LaTeX
counterparts are not italicized. On reflection, I agree with your
decision. My main concern was that the following letters, now in
italics, would look wrong for n-ary product and sum:
𝛱 (1D6F1)
𝛴 (1D6F4)
Of course, such operators should actually use the dedicated characters
as follows:
∏ (220F N-ARY PRODUCT)
∑ (2211 N-ARY SUMMATION)
There are some multi-character operators that could be translated to a
single character operator that would result in Unicode documents more
in line with ISO Z.
\%down%s ---> ⧹ (29F9) for schema hiding
%filter%%down%s ---> ⨡ (2A21) for schema projection
%rcomp%%down%s ---> ⨟ (2A1F) for schema composition
This would require ProofPower-Z to be updated to add the new symbols.
I mention it now because the transition to Unicode could be used as
an opportunity to eliminate the non-ISO forms from Unicode documents,
if you wished to transition to the ISO symbol.
Either way, you probably want to add schema projection and composition
to the ML function utf8_to_pp_replacement_data.
I don’t think you had updated your clone of the pputf8 contrib.
utf8_to_pp_replacement_data was a half-hearted attempt to introduce a
bit more compatibility with ISO Z that I decided to abandon. A proper
translation between ProofPower-Z and ISO Z needs to be on parse trees
rather than on streams of lexical tokens.
Yes, sorry, I hadn't updated my clone.
I notice in pp-contrib/src/pputf8 you have files
a.txt
t.tgz
Did you mean to commit those?
I agree that it would be good to start accepting keywords with
single-character Unicode equivalents for the Z operators as variant
syntax for the forms with subscripts.
There is also schema piping. I assume that the existing operator '>>'
can be dropped in favour of ⨠ (2A20 Z NOTATION SCHEMA PIPING) because,
with only parser support existing, nobody would be using it to date.
The following are not well supported on my system:
01F13C SQUARED LATIN CAPITAL LETTER M for %SML%
01F143 SQUARED LATIN CAPITAL LETTER T for %<:%
01F149 SQUARED LATIN CAPITAL LETTER Z for %SZT%
What do you consider converting them to the expanded form, e.g.
%SZT% ---> ⌜↘Z↕
?
That is what the original pputf8 scheme did, but I didn’t think it would
be very popular in the long term.
I think a single character is preferable and ideally it would be
somehow based on the opening corner '⌜'. I wonder if there is a
combining trick possible here.
I think it is quite important for these to work, so I have changed to
using circled lower-case letters.
These appear as expected on my system. It would be nice if we could
find an 'opening' symbol but I don't have any good ideas.
My immediate plan is to integrate the translation into ProofPower
itself, so that Unicode input and output are options you can select with
set_flag (similar to the way that you can currently select ASCII output,
by calling set_flag(“use_extended_chars”, false)). I will provide
separate flags for input and output.
Great - I look forward to seeing Z fly past in my shell!! Now I need
to work out how to get the same key mapping working in Linux generally.
Please let us know how you get on with that.
I'm planning to try something with xkb. Other suggestions are welcome
though!
Regards,
Phil
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
