# HG changeset patch
# User wenzelm
# Date 1478191870 -3600
# Node ID 85adb337e32f941c6910ce3695410d62bd78f74e
# Parent  cc2da001465b3feba28084f8196d4b300bc01114
updated to scala-2.12.0;

diff -r cc2da001465b -r 85adb337e32f Admin/components/components.sha1
--- 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
diff -r cc2da001465b -r 85adb337e32f Admin/components/main
--- 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
diff -r cc2da001465b -r 85adb337e32f src/Pure/System/invoke_scala.scala
--- 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 _)
 }
-
diff -r cc2da001465b -r 85adb337e32f src/Tools/jEdit/src/theories_dockable.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
diff -r cc2da001465b -r 85adb337e32f src/Tools/jEdit/src/timing_dockable.scala
--- 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