# HG changeset patch # User wenzelm # Date 1495204991 -7200 # Node ID bd45c8ebc214de6276a1ddf0cbdeab2fe1404870 # Parent 300beacd9875306fd268bdec39bf9d56a0532611 updated to scala-2.12.2; diff -r 300beacd9875 -r bd45c8ebc214 Admin/components/main --- a/Admin/components/main Fri May 19 16:14:24 2017 +0200 +++ b/Admin/components/main Fri May 19 16:43:11 2017 +0200 @@ -12,7 +12,7 @@ nunchaku-0.3 polyml-5.6-1 postgresql-9.4.1212 -scala-2.11.8 +scala-2.12.2 ssh-java-20161009 spass-3.8ds sqlite-jdbc-3.8.11.2 diff -r 300beacd9875 -r bd45c8ebc214 src/Pure/General/antiquote.scala --- a/src/Pure/General/antiquote.scala Fri May 19 16:14:24 2017 +0200 +++ b/src/Pure/General/antiquote.scala Fri May 19 16:43:11 2017 +0200 @@ -55,4 +55,3 @@ } } } - diff -r 300beacd9875 -r bd45c8ebc214 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Fri May 19 16:14:24 2017 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Fri May 19 16:43:11 2017 +0200 @@ -166,7 +166,7 @@ private class Node_Renderer extends ListView.Renderer[Document.Node.Name] { - def componentFor(list: ListView[_], isSelected: Boolean, + def componentFor(list: ListView[_ <: isabelle.Document.Node.Name], isSelected: Boolean, focused: Boolean, name: Document.Node.Name, index: Int): Component = { val component = Node_Renderer_Component diff -r 300beacd9875 -r bd45c8ebc214 src/Tools/jEdit/src/timing_dockable.scala --- a/src/Tools/jEdit/src/timing_dockable.scala Fri May 19 16:14:24 2017 +0200 +++ b/src/Tools/jEdit/src/timing_dockable.scala Fri May 19 16:43:11 2017 +0200 @@ -65,7 +65,7 @@ class Renderer extends ListView.Renderer[Entry] { - def componentFor(list: ListView[_], + def componentFor(list: ListView[_ <: Timing_Dockable.this.Entry], isSelected: Boolean, focused: Boolean, entry: Entry, index: Int): Component = { val component = Renderer_Component