726 elements: Elements, |
726 elements: Elements, |
727 result: Command.Results => (A, Text.Markup) => Option[A], |
727 result: Command.Results => (A, Text.Markup) => Option[A], |
728 status: Boolean = false): List[Text.Info[A]] = |
728 status: Boolean = false): List[Text.Info[A]] = |
729 { |
729 { |
730 val former_range = revert(range) |
730 val former_range = revert(range) |
731 thy_load_commands match { |
731 val (file_name, command_range_iterator) = |
732 case thy_load_command :: _ => |
732 thy_load_commands match { |
733 val file_name = node_name.node |
733 case command :: _ => (node_name.node, Iterator((command, 0))) |
734 val markup_index = Command.Markup_Index(status, file_name) |
734 case _ => ("", node.command_range(former_range)) |
735 (for { |
735 } |
736 chunk <- thy_load_command.chunks.get(file_name).iterator |
736 val markup_index = Command.Markup_Index(status, file_name) |
737 states = state.command_states(version, thy_load_command) |
737 (for { |
738 res = result(Command.State.merge_results(states)) |
738 (command, command_start) <- command_range_iterator |
739 range = former_range.restrict(chunk.range) |
739 chunk <- command.chunks.get(file_name).iterator |
740 markup = Command.State.merge_markup(states, markup_index, range, elements) |
740 states = state.command_states(version, command) |
741 Text.Info(r0, a) <- markup.cumulate[A](range, info, elements, |
741 res = result(Command.State.merge_results(states)) |
742 { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) } |
742 range = (former_range - command_start).restrict(chunk.range) |
743 ).iterator |
743 markup = Command.State.merge_markup(states, markup_index, range, elements) |
744 } yield Text.Info(convert(r0), a)).toList |
744 Text.Info(r0, a) <- markup.cumulate[A](range, info, elements, |
745 |
745 { |
746 case _ => |
746 case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) |
747 val markup_index = Command.Markup_Index(status, "") |
747 }).iterator |
748 (for { |
748 } yield Text.Info(convert(r0 + command_start), a)).toList |
749 (command, command_start) <- node.command_range(former_range) |
|
750 states = state.command_states(version, command) |
|
751 res = result(Command.State.merge_results(states)) |
|
752 range = (former_range - command_start).restrict(command.range) |
|
753 markup = Command.State.merge_markup(states, markup_index, range, elements) |
|
754 Text.Info(r0, a) <- markup.cumulate[A](range, info, elements, |
|
755 { |
|
756 case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) |
|
757 }).iterator |
|
758 } yield Text.Info(convert(r0 + command_start), a)).toList |
|
759 } |
|
760 } |
749 } |
761 |
750 |
762 def select[A]( |
751 def select[A]( |
763 range: Text.Range, |
752 range: Text.Range, |
764 elements: Elements, |
753 elements: Elements, |