On 04/14/2012 07:43 PM, Makarius wrote:
The starting point of the whole affair was the problem of having a
public class where the default constructor (or any further ones) are
private.
I did not know how to do it, until some Java expert talk about the
potential future of Java (after 1.7 or 1.8) explained that default
constructors were always as public as the class they belong to. This
solved my problem, because I knew what to google for concerning Scala,
namely "private constructor".
Accordingly the solution in Scala is:
final class Graph[Key, A] private(rep: SortedMap[Key, (A,
(SortedSet[Key], SortedSet[Key]))])
^^^^^^^
Your conversation with the Java expert must have involved some
misunderstanding:
In Java:
public final class Graph {
private final SortedMap<...> rep;
// private constructor:
private Graph(SortedMap<...> rep) {
this.rep = rep;
}
// public static "factory methods"
public static Graph empty() {
}
...
}
Note that the so-called "default constructor" is only added when no
constructor is defined explicitly. So the above is fine, modulo the
usual Java verbosity.
For good contemporary Java coding practices, Joshua Bloch is the reference:
http://www.amazon.com/Effective-Java-Edition-Joshua-Bloch/dp/0321356683/
Alex
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
