--- a/Admin/components/components.sha1 Thu Nov 03 08:10:56 2016 +0100
+++ b/Admin/components/components.sha1 Thu Nov 03 17:51:10 2016 +0100
@@ -154,6 +154,7 @@
e7cf20e3b27c894c6127c7a37042c1667f57385e scala-2.11.6.tar.gz
4810c1b00719115df235be1c5991aa6ea7186134 scala-2.11.7.tar.gz
3eca4b80710996fff87ed1340dcea2c5f6ebf4f7 scala-2.11.8.tar.gz
+0004e53f885fb165b50c95686dec40d99ab0bdbd scala-2.12.0.tar.gz
b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz
5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz
43b5afbcad575ab6817d2289756ca22fd2ef43a9 spass-3.8ds.tar.gz
--- a/Admin/components/main Thu Nov 03 08:10:56 2016 +0100
+++ b/Admin/components/main Thu Nov 03 17:51:10 2016 +0100
@@ -10,7 +10,7 @@
jortho-1.0-2
kodkodi-1.5.2
polyml-5.6-1
-scala-2.11.8
+scala-2.12.0
ssh-java-20161009
spass-3.8ds
sqlite-jdbc-3.8.11.2
--- a/src/Pure/System/invoke_scala.scala Thu Nov 03 08:10:56 2016 +0100
+++ b/src/Pure/System/invoke_scala.scala Thu Nov 03 17:51:10 2016 +0100
@@ -125,4 +125,3 @@
Markup.INVOKE_SCALA -> invoke_scala _,
Markup.CANCEL_SCALA -> cancel_scala _)
}
-
--- a/src/Tools/jEdit/src/theories_dockable.scala Thu Nov 03 08:10:56 2016 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Thu Nov 03 17:51:10 2016 +0100
@@ -178,8 +178,8 @@
private class Node_Renderer extends ListView.Renderer[Document.Node.Name]
{
- def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
- name: Document.Node.Name, index: Int): Component =
+ def componentFor(list: ListView[_ <: isabelle.Document.Node.Name], isSelected: Boolean,
+ focused: Boolean, name: Document.Node.Name, index: Int): Component =
{
val component = Node_Renderer_Component
component.node_name = name
--- a/src/Tools/jEdit/src/timing_dockable.scala Thu Nov 03 08:10:56 2016 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Thu Nov 03 17:51:10 2016 +0100
@@ -65,8 +65,8 @@
class Renderer extends ListView.Renderer[Entry]
{
- def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
- entry: Entry, index: Int): Component =
+ def componentFor(list: ListView[_ <: Timing_Dockable.this.Entry],
+ isSelected: Boolean, focused: Boolean, entry: Entry, index: Int): Component =
{
val component = Renderer_Component
component.entry = entry