java: prefer ArrayList to Vector
commitd15691045342fb67796a1368698ad8ee4c5799b9
authorAkim Demaille <akim.demaille@gmail.com>
Tue, 3 Nov 2020 07:21:35 +0000 (3 08:21 +0100)
committerAkim Demaille <akim.demaille@gmail.com>
Tue, 3 Nov 2020 07:46:54 +0000 (3 08:46 +0100)
treec2130520923c5b68f9373c06412fda64010c1585
parent1995d9e2f26d180665364de378e90792fce567fb
java: prefer ArrayList to Vector

Vector is synchronized, which is completely useless in our case (and
not even relevant when concurrency matters).  No seasoned Java
programmer would use it.
Reported by Uxio Prego.

* data/skeletons/lalr1.java: Replace Vector with ArrayList.
Unfortunately its API is not as rich, and lacks lastElement and
setSize.
data/skeletons/lalr1.java