--- a/src/Pure/PIDE/document.scala Wed Apr 02 20:22:12 2014 +0200
+++ b/src/Pure/PIDE/document.scala Wed Apr 02 20:41:44 2014 +0200
@@ -212,7 +212,7 @@
private def full_range: Text.Range = full_index._2
- def range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
+ def iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
{
if (!commands.isEmpty && full_range.contains(i)) {
val (cmd0, start0) = full_index._1(i / Commands.block_size)
@@ -253,11 +253,11 @@
if (new_commands eq _commands.commands) this
else new Node(get_blob, header, perspective, Node.Commands(new_commands))
- def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
- _commands.range(i)
+ def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
+ _commands.iterator(i)
- def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
- command_range(range.start) takeWhile { case (_, start) => start < range.stop }
+ def command_iterator(range: Text.Range): Iterator[(Command, Text.Offset)] =
+ command_iterator(range.start) takeWhile { case (_, start) => start < range.stop }
def command_start(cmd: Command): Option[Text.Offset] =
Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
@@ -733,14 +733,14 @@
status: Boolean = false): List[Text.Info[A]] =
{
val former_range = revert(range)
- val (file_name, command_range_iterator) =
+ val (file_name, command_iterator) =
load_commands match {
case command :: _ => (node_name.node, Iterator((command, 0)))
- case _ => ("", node.command_range(former_range))
+ case _ => ("", node.command_iterator(former_range))
}
val markup_index = Command.Markup_Index(status, file_name)
(for {
- (command, command_start) <- command_range_iterator
+ (command, command_start) <- command_iterator
chunk <- command.chunks.get(file_name).iterator
states = state.command_states(version, command)
res = result(states)
--- a/src/Pure/Thy/thy_syntax.scala Wed Apr 02 20:22:12 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Wed Apr 02 20:41:44 2014 +0200
@@ -141,9 +141,9 @@
}
val commands =
- if (overlays.is_empty) node.command_range(perspective.range)
- else node.command_range()
- check_ranges(perspective.ranges, commands.toStream)
+ (if (overlays.is_empty) node.command_iterator(perspective.range)
+ else node.command_iterator()).toStream
+ check_ranges(perspective.ranges, commands)
(Command.Perspective(visible.toList), Command.Perspective(visible_overlay.toList))
}
}
--- a/src/Tools/jEdit/src/document_view.scala Wed Apr 02 20:22:12 2014 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Wed Apr 02 20:41:44 2014 +0200
@@ -224,15 +224,15 @@
text_area.invalidateScreenLineRange(0, visible_lines)
else {
val visible_range = JEdit_Lib.visible_range(text_area).get
- val visible_cmds =
- snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
- if (visible_cmds.exists(changed.commands)) {
+ val visible_iterator =
+ snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1)
+ if (visible_iterator.exists(changed.commands)) {
for {
line <- (0 until visible_lines).iterator
start = text_area.getScreenLineStartOffset(line) if start >= 0
end = text_area.getScreenLineEndOffset(line) if end >= 0
range = Text.Range(start, end)
- line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
+ line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1)
if line_cmds.exists(changed.commands)
} text_area.invalidateScreenLineRange(line, line)
}
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Apr 02 20:22:12 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Apr 02 20:41:44 2014 +0200
@@ -158,7 +158,7 @@
opt_snapshot match {
case Some(snapshot) =>
val root = data.root
- for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
+ for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) {
val markup =
snapshot.state.command_markup(
snapshot.version, command, Command.Markup_Index.markup,
--- a/src/Tools/jEdit/src/jedit_editor.scala Wed Apr 02 20:22:12 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Wed Apr 02 20:41:44 2014 +0200
@@ -74,9 +74,9 @@
val node = snapshot.version.nodes(doc_view.model.node_name)
val caret = snapshot.revert(text_area.getCaretPosition)
if (caret < buffer.getLength) {
- val caret_commands = node.command_range(caret)
- if (caret_commands.hasNext) {
- val (cmd0, _) = caret_commands.next
+ val caret_command_iterator = node.command_iterator(caret)
+ if (caret_command_iterator.hasNext) {
+ val (cmd0, _) = caret_command_iterator.next
node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
}
else None
@@ -154,11 +154,11 @@
case None => None
case Some((node, _)) =>
val file_name = command.node_name.node
- val sources =
+ val sources_iterator =
node.commands.iterator.takeWhile(_ != command).map(_.source) ++
(if (offset == 0) Iterator.empty
else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
- val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
+ val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
Some(new Hyperlink { def follow(view: View) { goto_file(view, file_name, line, column) } })
}
}
--- a/src/Tools/jEdit/src/rich_text_area.scala Wed Apr 02 20:22:12 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Wed Apr 02 20:41:44 2014 +0200
@@ -359,7 +359,7 @@
r2 <- r1.try_restrict(chunk_range)
} yield r2
- val padded_markup =
+ val padded_markup_iterator =
if (markup.isEmpty)
Iterator(Text.Info(chunk_range, chunk_color))
else
@@ -370,7 +370,7 @@
var x1 = x + w
gfx.setFont(chunk_font)
- for (Text.Info(range, color) <- padded_markup if !range.is_singularity) {
+ for (Text.Info(range, color) <- padded_markup_iterator if !range.is_singularity) {
val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
gfx.setColor(color)