# HG changeset patch
# User wenzelm
# Date 1446830135 -3600
# Node ID 94ab348eaab2065b802c06a89e5be69debbf2490
# Parent  d07d0d5a572b27dc1a7cf99bf008874bacf8e8bd
tuned;

diff -r d07d0d5a572b -r 94ab348eaab2 src/Pure/Concurrent/mailbox.scala
--- a/src/Pure/Concurrent/mailbox.scala	Fri Nov 06 14:43:05 2015 +0100
+++ b/src/Pure/Concurrent/mailbox.scala	Fri Nov 06 18:15:35 2015 +0100
@@ -17,7 +17,7 @@
 
 class Mailbox[A] private()
 {
-  private val mailbox = Synchronized(List.empty[A])
+  private val mailbox = Synchronized[List[A]](Nil)
   override def toString: String = mailbox.value.reverse.mkString("Mailbox(", ",", ")")
 
   def send(msg: A): Unit = mailbox.change(msg :: _)
diff -r d07d0d5a572b -r 94ab348eaab2 src/Pure/Concurrent/par_list.scala
--- a/src/Pure/Concurrent/par_list.scala	Fri Nov 06 14:43:05 2015 +0100
+++ b/src/Pure/Concurrent/par_list.scala	Fri Nov 06 18:15:35 2015 +0100
@@ -13,7 +13,7 @@
   def managed_results[A, B](f: A => B, xs: List[A]): List[Exn.Result[B]] =
     if (xs.isEmpty || xs.tail.isEmpty) xs.map(x => Exn.capture { f(x) })
     else {
-      val state = Synchronized((List.empty[Future[B]], false))
+      val state = Synchronized[(List[Future[B]], Boolean)]((Nil, false))
 
       def cancel_other(self: Int = -1): Unit =
         state.change { case (futures, canceled) =>
diff -r d07d0d5a572b -r 94ab348eaab2 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Nov 06 14:43:05 2015 +0100
+++ b/src/Pure/PIDE/session.scala	Fri Nov 06 18:15:35 2015 +0100
@@ -24,7 +24,7 @@
 
   class Outlet[A](dispatcher: Consumer_Thread[() => Unit])
   {
-    private val consumers = Synchronized(List.empty[Consumer[A]])
+    private val consumers = Synchronized[List[Consumer[A]]](Nil)
 
     def += (c: Consumer[A]) { consumers.change(Library.update(c)) }
     def -= (c: Consumer[A]) { consumers.change(Library.remove(c)) }
@@ -330,7 +330,7 @@
 
   private object prover
   {
-    private val variable = Synchronized(None: Option[Prover])
+    private val variable = Synchronized[Option[Prover]](None)
 
     def defined: Boolean = variable.value.isDefined
     def get: Prover = variable.value.get
diff -r d07d0d5a572b -r 94ab348eaab2 src/Pure/Tools/print_operation.scala
--- a/src/Pure/Tools/print_operation.scala	Fri Nov 06 14:43:05 2015 +0100
+++ b/src/Pure/Tools/print_operation.scala	Fri Nov 06 18:15:35 2015 +0100
@@ -20,7 +20,7 @@
 
   class Handler extends Session.Protocol_Handler
   {
-    private val print_operations = Synchronized(Nil: List[(String, String)])
+    private val print_operations = Synchronized[List[(String, String)]](Nil)
 
     def get: List[(String, String)] = print_operations.value
 
diff -r d07d0d5a572b -r 94ab348eaab2 src/Tools/Graphview/graphview.scala
--- a/src/Tools/Graphview/graphview.scala	Fri Nov 06 14:43:05 2015 +0100
+++ b/src/Tools/Graphview/graphview.scala	Fri Nov 06 18:15:35 2015 +0100
@@ -156,7 +156,7 @@
 
   object Selection
   {
-    private val state = Synchronized(List.empty[Graph_Display.Node])
+    private val state = Synchronized[List[Graph_Display.Node]](Nil)
 
     def get(): List[Graph_Display.Node] = state.value
     def contains(node: Graph_Display.Node): Boolean = get().contains(node)
diff -r d07d0d5a572b -r 94ab348eaab2 src/Tools/Graphview/mutator_event.scala
--- a/src/Tools/Graphview/mutator_event.scala	Fri Nov 06 14:43:05 2015 +0100
+++ b/src/Tools/Graphview/mutator_event.scala	Fri Nov 06 18:15:35 2015 +0100
@@ -21,7 +21,7 @@
 
   class Bus
   {
-    private val receivers = Synchronized(List.empty[Receiver])
+    private val receivers = Synchronized[List[Receiver]](Nil)
 
     def += (r: Receiver) { receivers.change(Library.insert(r)) }
     def -= (r: Receiver) { receivers.change(Library.remove(r)) }
diff -r d07d0d5a572b -r 94ab348eaab2 src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Fri Nov 06 14:43:05 2015 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Fri Nov 06 18:15:35 2015 +0100
@@ -22,7 +22,7 @@
 
 class Monitor_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  private val rev_stats = Synchronized(Nil: List[Properties.T])
+  private val rev_stats = Synchronized[List[Properties.T]](Nil)
 
 
   /* chart data -- owned by GUI thread */
diff -r d07d0d5a572b -r 94ab348eaab2 src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Fri Nov 06 14:43:05 2015 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala	Fri Nov 06 18:15:35 2015 +0100
@@ -137,7 +137,7 @@
 
   private class Interpreter
   {
-    private val running = Synchronized(None: Option[Thread])
+    private val running = Synchronized[Option[Thread]](None)
     def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) }
 
     private val settings = new GenericRunnerSettings(report_error)