author | wenzelm |
Thu, 26 Nov 2020 15:16:37 +0100 | |
changeset 72719 | cb07791d86b8 |
parent 72718 | 59a7f82a7180 |
child 72720 | f2d641e856ac |
--- 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)