src/Pure/PIDE/document.scala
changeset 56514 db929027e701
parent 56489 884e8f37492c
child 56590 d01d183e84ea
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Apr 10 14:27:35 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Apr 10 14:36:29 2014 +0200
     1.3 @@ -536,9 +536,11 @@
     1.4        id == st.command.id ||
     1.5        (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
     1.6  
     1.7 -    private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] =
     1.8 +    private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] = None
     1.9 +    /* FIXME
    1.10        (execs.get(id) orElse commands.get(id)).map(st =>
    1.11          ((Text.Chunk.Id(st.command.id), st.command.chunk)))
    1.12 +    */
    1.13  
    1.14      private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
    1.15        (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>