src/Pure/PIDE/document.scala
changeset 72957 cb07791d86b8
parent 72956 59a7f82a7180
child 72959 79f5e843e5ec
equal deleted inserted replaced
72956:59a7f82a7180 72957:cb07791d86b8
   730     def defined_blob(digest: SHA1.Digest): Boolean = blobs.contains(digest)
   730     def defined_blob(digest: SHA1.Digest): Boolean = blobs.contains(digest)
   731 
   731 
   732     def define_command(command: Command): State =
   732     def define_command(command: Command): State =
   733     {
   733     {
   734       val id = command.id
   734       val id = command.id
   735       copy(commands = commands + (id -> command.init_state))
   735       if (commands.isDefinedAt(id)) fail
       
   736       else copy(commands = commands + (id -> command.init_state))
   736     }
   737     }
   737 
   738 
   738     def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
   739     def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
   739 
   740 
   740     def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
   741     def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)