src/Pure/PIDE/document.scala
changeset 65187 9250f944ec0f
parent 64867 e7220f4de11f
child 65195 ffab6f460a82
equal deleted inserted replaced
65186:4659e87c3795 65187:9250f944ec0f
   855           result: List[Command.State] => (A, Text.Markup) => Option[A],
   855           result: List[Command.State] => (A, Text.Markup) => Option[A],
   856           status: Boolean = false): List[Text.Info[A]] =
   856           status: Boolean = false): List[Text.Info[A]] =
   857         {
   857         {
   858           val former_range = revert(range).inflate_singularity
   858           val former_range = revert(range).inflate_singularity
   859           val (chunk_name, command_iterator) =
   859           val (chunk_name, command_iterator) =
   860             commands_loading match {
   860             commands_loading.headOption match {
   861               case command :: _ => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0)))
   861               case None => (Symbol.Text_Chunk.Default, node.command_iterator(former_range))
   862               case _ => (Symbol.Text_Chunk.Default, node.command_iterator(former_range))
   862               case Some(command) => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0)))
   863             }
   863             }
   864           val markup_index = Command.Markup_Index(status, chunk_name)
   864           val markup_index = Command.Markup_Index(status, chunk_name)
   865           (for {
   865           (for {
   866             (command, command_start) <- command_iterator
   866             (command, command_start) <- command_iterator
   867             chunk <- command.chunks.get(chunk_name).iterator
   867             chunk <- command.chunks.get(chunk_name).iterator