tuned -- fewer warnings;

--- a/src/Pure/Tools/build_stats.scala	Tue Sep 20 22:29:51 2016 +0200
+++ b/src/Pure/Tools/build_stats.scala	Tue Sep 20 22:31:50 2016 +0200
@@ -62,7 +62,7 @@
           val gc = Time.seconds(g)
           timing += (name -> Timing(elapsed, cpu, gc))
           threads += (name -> t)
-        case ML_Option(option) => ml_options += option
+        case ML_Option(a, b) => ml_options += (a -> b)
         case _ =>
       }
     }

--- a/src/Pure/library.scala	Tue Sep 20 22:29:51 2016 +0200
+++ b/src/Pure/library.scala	Tue Sep 20 22:31:50 2016 +0200
@@ -19,6 +19,8 @@
 
   def using[A <: { def close() }, B](x: A)(f: A => B): B =
   {
+    import scala.language.reflectiveCalls
+
     try { f(x) }
     finally { if (x != null) x.close() }
   }

--- a/src/Tools/jEdit/src/symbols_dockable.scala	Tue Sep 20 22:29:51 2016 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala	Tue Sep 20 22:31:50 2016 +0200
@@ -61,7 +61,7 @@
           Multi_Map(
             (for {
               (abbr, txt0) <- abbrevs
-              val txt = Symbol.encode(txt0)
+              txt = Symbol.encode(txt0)
               if !Symbol.iterator(txt).
                 forall(s => s.length == 1 && s(0) != Completion.caret_indicator)
             } yield (txt, abbr)): _*).iterator_list.toList