src/Pure/System/session.scala
changeset 45469 479c07072992
parent 45446 24444588fddd
child 45499 76c2e3ddc183
equal deleted inserted replaced
45468:7daef43592d0 45469:479c07072992
   241       val name = change.name
   241       val name = change.name
   242       val doc_edits = change.doc_edits
   242       val doc_edits = change.doc_edits
   243 
   243 
   244       def id_command(command: Command)
   244       def id_command(command: Command)
   245       {
   245       {
   246         if (global_state().lookup_command(command.id).isEmpty) {
   246         if (!global_state().defined_command(command.id)) {
   247           global_state.change(_.define_command(command))
   247           global_state.change(_.define_command(command))
   248           prover.get.define_command(command.id, Symbol.encode(command.source))
   248           prover.get.define_command(command.id, Symbol.encode(command.source))
   249         }
   249         }
   250       }
   250       }
   251       doc_edits foreach {
   251       doc_edits foreach {