src/Pure/PIDE/document.scala
changeset 72957 cb07791d86b8
parent 72956 59a7f82a7180
child 72959 79f5e843e5ec
--- a/src/Pure/PIDE/document.scala	Thu Nov 26 14:48:22 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Nov 26 15:16:37 2020 +0100
@@ -732,7 +732,8 @@
     def define_command(command: Command): State =
     {
       val id = command.id
-      copy(commands = commands + (id -> command.init_state))
+      if (commands.isDefinedAt(id)) fail
+      else copy(commands = commands + (id -> command.init_state))
     }
 
     def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)