# HG changeset patch # User wenzelm # Date 1498332228 -7200 # Node ID d91108ba94747cc4de4c857a8ed720b9098adc22 # Parent a41435469559bf904683d909c1c2bd49df51c462 back to scala-2.12.2, after a41435469559; diff -r a41435469559 -r d91108ba9474 Admin/components/main --- a/Admin/components/main Sat Jun 24 09:17:35 2017 +0200 +++ b/Admin/components/main Sat Jun 24 21:23:48 2017 +0200 @@ -12,7 +12,7 @@ nunchaku-0.3 polyml-5.6-1 postgresql-42.1.1 -scala-2.11.8 +scala-2.12.2 ssh-java-20161009 spass-3.8ds sqlite-jdbc-3.18.0-1 diff -r a41435469559 -r d91108ba9474 src/HOL/Codegenerator_Test/Generate.thy --- a/src/HOL/Codegenerator_Test/Generate.thy Sat Jun 24 09:17:35 2017 +0200 +++ b/src/HOL/Codegenerator_Test/Generate.thy Sat Jun 24 21:23:48 2017 +0200 @@ -18,3 +18,4 @@ export_code _ checking SML OCaml? Haskell? Scala end + diff -r a41435469559 -r d91108ba9474 src/Pure/General/antiquote.scala --- a/src/Pure/General/antiquote.scala Sat Jun 24 09:17:35 2017 +0200 +++ b/src/Pure/General/antiquote.scala Sat Jun 24 21:23:48 2017 +0200 @@ -55,4 +55,3 @@ } } } - diff -r a41435469559 -r d91108ba9474 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Sat Jun 24 09:17:35 2017 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Sat Jun 24 21:23:48 2017 +0200 @@ -179,7 +179,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 a41435469559 -r d91108ba9474 src/Tools/jEdit/src/timing_dockable.scala --- a/src/Tools/jEdit/src/timing_dockable.scala Sat Jun 24 09:17:35 2017 +0200 +++ b/src/Tools/jEdit/src/timing_dockable.scala Sat Jun 24 21:23:48 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