# HG changeset patch
# User wenzelm
# Date 1330276784 -3600
# Node ID fb160aa7a9a8273bdfafe9d26b5741a5c603b7a3
# Parent  4a74fbd6f28bedf10e18954160b033c5a76611d1
more abstract class Document.State.Assignment;

diff -r 4a74fbd6f28b -r fb160aa7a9a8 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Feb 26 17:54:35 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Feb 26 18:19:44 2012 +0100
@@ -279,16 +279,16 @@
 
     object Assignment
     {
-      val init: Assignment = Assignment()
+      val init: Assignment = new Assignment()
     }
 
-    case class Assignment(
+    class Assignment private(
       val command_execs: Map[Command_ID, Exec_ID] = Map.empty,
       val last_execs: Map[String, Option[Command_ID]] = Map.empty,
       val is_finished: Boolean = false)
     {
       def check_finished: Assignment = { require(is_finished); this }
-      def unfinished: Assignment = copy(is_finished = false)
+      def unfinished: Assignment = new Assignment(command_execs, last_execs, false)
 
       def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])],
         add_last_execs: List[(String, Option[Command_ID])]): Assignment =
@@ -299,7 +299,7 @@
             case (res, (command_id, None)) => res - command_id
             case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id)
           }
-        Assignment(command_execs1, last_execs ++ add_last_execs, true)
+        new Assignment(command_execs1, last_execs ++ add_last_execs, true)
       }
     }