Re: [isabelle-dev] [PATCH 0 of 3] Reduce Isabelle/jEdit output window overflow.
On Fri, 22 Mar 2013, David Greenaway wrote: PATCH 2: When determining how long a string of spaces is, use 'width( ) * n' instead of 'width(mix) * n / 3'. That was actually a regression -- the measurement was there before I made the mix-based unit, to get better results for exotic font spacing, but I've forgotten to upgrade the blanks measure; see a981a5c8a505. PATCH 3: When measuring strings, use Font.getStringBounds instead of FontMetrics.stringWidth. The latter doesn't take into account anti-aliasing or kerning, while the former is what is actually used when rendering the strings to the screen. That seems to be the most important point here. It requires some further investigation how jEdit measures things in general, so see if it agrees with the actual painting. There might be some deeper problem of Graphics2D painting vs. font metrics here, that needs to be investigated. If you can tell more, pointing to sources by the jEdit guys or Oracle, I will listen attentively. the ScalaDoc style guides [1] could be a little more concrete on where I went wrong, I would be happy to reformat the patches. [1]: http://docs.scala-lang.org/style/scaladoc.html This one does not apply to Isabelle/Scala sources. ScalaDoc is no universal standard, and it does not lead to well-document sources. You can see the results of some decades of JavaDoc practice when you look through the main JDK sources, which I am occasionally forced to do. General Scala coding style is still an open question, and Isabelle/Scala has its own style inherited from Isabelle/ML. I would imagine it must be quite frustrating when upstream maintainers refuse to accept community contributions. No, I am just a bit more realistic about how software development processes work. There are no universal principles of community contributions, but the process somehow determins the quality of the result. Have you ever tried to submit patches to the Linux kernel? Concerning jEdit development, I am in fact more worried about people messing things up by contributed patches. My patch got accepted, because nobody had a real clue, and I was persistent enough to pretend that it was the right thing -- German keyboard input on Mac OS X with Java 7. It certainly was right for our situation of cross-platform Isabelle/jEdit with Java 7, but might cause issues with more obscure legacy configurations of someone else somewhere. This is also the reason why I now wait and see, instead of posting a few more jEdit patches that I have in the pipeline. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning
On Fri, 2013-03-22 at 13:25 +0100, Makarius wrote:
On Fri, 22 Mar 2013, Andreas Lochbihler wrote:
{(x, y). P} is pretty syntax for
Collect (prod_case (%x y. P)), so in your case, you get
Collect (prod_case (%v v. v : {''a'', ''b''}))
See how the second v in %v v. ... hides the former.
There is no warning because it is perfectly normal to rebind a variable
name in a lambda abstraction.
I agree that it is perfectly normal, just like term λx x x. x, and no
warning or error is to be expected.
Clearly, different people have different expectations. {(v,v). P v}
is not a lambda abstraction (regardless of how it is represented
internally). But it is similar to established mathematical notation, so
users might (and, as this thread again shows, do) expect it to denote
some subset of the identity relation. See also
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-April/msg00028.html
Best,
Tjark
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning
Some sort of visual indication that the same variable is being bound twice
might be useful, though that sort of thing is easy to overlook.
Larry
On 22 Mar 2013, at 13:15, Tjark Weber webe...@in.tum.de wrote:
On Fri, 2013-03-22 at 13:25 +0100, Makarius wrote:
On Fri, 22 Mar 2013, Andreas Lochbihler wrote:
{(x, y). P} is pretty syntax for
Collect (prod_case (%x y. P)), so in your case, you get
Collect (prod_case (%v v. v : {''a'', ''b''}))
See how the second v in %v v. ... hides the former.
There is no warning because it is perfectly normal to rebind a variable
name in a lambda abstraction.
I agree that it is perfectly normal, just like term λx x x. x, and no
warning or error is to be expected.
Clearly, different people have different expectations. {(v,v). P v}
is not a lambda abstraction (regardless of how it is represented
internally). But it is similar to established mathematical notation, so
users might (and, as this thread again shows, do) expect it to denote
some subset of the identity relation. See also
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-April/msg00028.html
Best,
Tjark
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning
On Fri, 22 Mar 2013, Tjark Weber wrote:
I agree that it is perfectly normal, just like term λx x x. x, and no
warning or error is to be expected.
Clearly, different people have different expectations. {(v,v). P v}
is not a lambda abstraction (regardless of how it is represented
internally).
So how about λ(v. v). v then?
Anyway, when I've got exposed to this slightly sugared lambda-calculus in
Isabelle for the first time in 1993, I found its simplicity and uniformity
a great relieve, compared to all these adhoc explanations about binders in
informal mathematics. You merely need to learn very few priniciples, and
then you know how it works. Of course, you need to develop a sense what a
binding occurrence of a variable is.
Color schemes in the editor can help to teach people what these principles
of binding and scoping are. In the 1990-ies, black, blue, green variables
were a big thing. Today, it is just a tiny little step to visualize scope
groups in Isabelle/jEdit in a similar way you ee in Netbeans etc. for
Java. (You can already following the implicit hyperlinks in Isabelle2013.)
and, as this thread again shows, do) expect it to denote some subset of
the identity relation. See also
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-April/msg00028.html
So I won't have to recycle the old jokes again -- its all there on the
thread from 1 year ago.
Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
