# HG changeset patch
# User wenzelm
# Date 1606400197 -3600
# Node ID cb07791d86b864637b79001e11070029d9c8e5ea
# Parent  59a7f82a7180f57d4a3a8e6191118e4e4acb011b
more strict;

diff -r 59a7f82a7180 -r cb07791d86b8 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)