--- a/src/Pure/PIDE/document.scala Mon Aug 05 11:08:54 2013 +0200
+++ b/src/Pure/PIDE/document.scala Mon Aug 05 15:03:52 2013 +0200
@@ -28,7 +28,9 @@
{
def + (o: Overlay) = new Overlays(rep + o)
def - (o: Overlay) = new Overlays(rep - o)
+ def is_empty: Boolean = rep.isEmpty
def dest: List[Overlay] = rep.toList
+ def commands: Set[Command] = rep.iterator.map(x => x._1).toSet
}
--- a/src/Pure/Thy/thy_syntax.scala Mon Aug 05 11:08:54 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Mon Aug 05 15:03:52 2013 +0200
@@ -92,11 +92,17 @@
/** perspective **/
- def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
+ def command_perspective(
+ node: Document.Node,
+ perspective: Text.Perspective,
+ overlays: Document.Overlays): (Command.Perspective, Command.Perspective) =
{
- if (perspective.is_empty) Command.Perspective.empty
+ if (perspective.is_empty && overlays.is_empty)
+ (Command.Perspective.empty, Command.Perspective.empty)
else {
- val result = new mutable.ListBuffer[Command]
+ val has_overlay = overlays.commands
+ val visible = new mutable.ListBuffer[Command]
+ val visible_overlay = new mutable.ListBuffer[Command]
@tailrec
def check_ranges(ranges: List[Text.Range], commands: Stream[(Command, Text.Offset)])
{
@@ -104,17 +110,31 @@
case (range :: more_ranges, (command, offset) #:: more_commands) =>
val command_range = command.range + offset
range compare command_range match {
- case -1 => check_ranges(more_ranges, commands)
case 0 =>
- result += command
+ visible += command
+ visible_overlay += command
check_ranges(ranges, more_commands)
- case 1 => check_ranges(ranges, more_commands)
+ case c =>
+ if (has_overlay(command)) visible_overlay += command
+
+ if (c < 0) check_ranges(more_ranges, commands)
+ else check_ranges(ranges, more_commands)
}
+
+ case (Nil, (command, _) #:: more_commands) =>
+ if (has_overlay(command)) visible_overlay += command
+
+ check_ranges(Nil, more_commands)
+
case _ =>
}
}
- check_ranges(perspective.ranges, node.command_range(perspective.range).toStream)
- Command.Perspective(result.toList)
+
+ val commands =
+ if (overlays.is_empty) node.command_range(perspective.range)
+ else node.command_range()
+ check_ranges(perspective.ranges, commands.toStream)
+ (Command.Perspective(visible.toList), Command.Perspective(visible_overlay.toList))
}
}
@@ -317,12 +337,13 @@
case (_, Document.Node.Deps(_)) => node
case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
+ val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays)
val perspective: Document.Node.Perspective_Command =
- Document.Node.Perspective(required, command_perspective(node, text_perspective), overlays)
+ Document.Node.Perspective(required, visible_overlay, overlays)
if (node.same_perspective(perspective)) node
else
node.update_perspective(perspective).update_commands(
- consolidate_spans(syntax, reparse_limit, name, perspective.visible, node.commands))
+ consolidate_spans(syntax, reparse_limit, name, visible, node.commands))
}
}