# HG changeset patch # User wenzelm # Date 1330277128 -3600 # Node ID 7f741b2c82a334f6b2d6ab2e867190a04ffcb9e8 # Parent fb160aa7a9a8273bdfafe9d26b5741a5c603b7a3 more abstract class Document.State; diff -r fb160aa7a9a8 -r 7f741b2c82a3 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sun Feb 26 18:19:44 2012 +0100 +++ b/src/Pure/PIDE/document.scala Sun Feb 26 18:25:28 2012 +0100 @@ -307,7 +307,7 @@ State().define_version(Version.init, Assignment.init).assign(Version.init.id)._2 } - sealed case class State( + sealed case class State private( val versions: Map[Version_ID, Version] = Map.empty, val commands: Map[Command_ID, Command.State] = Map.empty, // static markup from define_command val execs: Map[Exec_ID, Command.State] = Map.empty, // dynamic markup from execution