more strict;
authorwenzelm
Thu, 26 Nov 2020 15:16:37 +0100
changeset 72719 cb07791d86b8
parent 72718 59a7f82a7180
child 72720 f2d641e856ac
more strict;
src/Pure/PIDE/document.scala
--- 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)