On Sat, 14 Apr 2012, Lars Hupel wrote:
The main thing is the "private" in this odd position, which is Odersky's
way to make the constructor private, but the keep the type itself
public. This detail seems to have been forgotten in Java -- in fact in a
recent talk some Java guru admitted that -- which was also my starting
point to google for "private constructor" to find the above solution.
In fact, the pattern you used is quite common amongst Java developers,
they just call it "Factory Pattern".
I've heard of this recent addition to the OO vocabulary to fix some early
conceptual problems of the approach. That is "object Graph" part only.
How would a Java person solve the private constructor problem?
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
