# HG changeset patch
# User wenzelm
# Date 1474403510 -7200
# Node ID 70973a1b4ec0af5c183a4a287c2f0ad6efc57894
# Parent  500646ef617a3c067f96948ecc9cb5d2ae14a365
tuned -- fewer warnings;

diff -r 500646ef617a -r 70973a1b4ec0 src/Pure/Tools/build_stats.scala
--- 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 _ =>
       }
     }
diff -r 500646ef617a -r 70973a1b4ec0 src/Pure/library.scala
--- 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() }
   }
diff -r 500646ef617a -r 70973a1b4ec0 src/Tools/jEdit/src/symbols_dockable.scala
--- 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