src/Pure/PIDE/protocol.scala
changeset 59735 24bee1b11fce
parent 59714 ae322325adbb
child 60879 3dc649cfd512
     1.1 --- a/src/Pure/PIDE/protocol.scala	Tue Mar 17 09:22:21 2015 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Mar 17 15:21:41 2015 +0100
     1.3 @@ -329,7 +329,7 @@
     1.4      }
     1.5  
     1.6      protocol_command("Document.define_command",
     1.7 -      (Document_ID(command.id) :: encode(command.name) :: blobs_yxml :: toks_yxml ::
     1.8 +      (Document_ID(command.id) :: encode(command.span.name) :: blobs_yxml :: toks_yxml ::
     1.9          toks.map(tok => encode(tok.source))): _*)
    1.10    }
    1.11