maintain commands together with index -- avoid redundant reconstruction of full_index;
authorwenzelm
Wed Aug 07 20:32:54 2013 +0200 (2013-08-07)
changeset 529018be75f53db82
parent 52900 d29bf6db8a2d
child 52902 7196e1ce1cd8
maintain commands together with index -- avoid redundant reconstruction of full_index;
src/Pure/PIDE/document.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Aug 07 19:59:58 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Aug 07 20:32:54 2013 +0200
     1.3 @@ -124,71 +124,83 @@
     1.4  
     1.5      /* commands */
     1.6  
     1.7 -    def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
     1.8 -      : Iterator[(Command, Text.Offset)] =
     1.9 +    object Commands
    1.10 +    {
    1.11 +      def apply(commands: Linear_Set[Command]): Commands = new Commands(commands)
    1.12 +      val empty: Commands = apply(Linear_Set.empty)
    1.13 +
    1.14 +      def starts(commands: Iterator[Command], offset: Text.Offset = 0)
    1.15 +        : Iterator[(Command, Text.Offset)] =
    1.16 +      {
    1.17 +        var i = offset
    1.18 +        for (command <- commands) yield {
    1.19 +          val start = i
    1.20 +          i += command.length
    1.21 +          (command, start)
    1.22 +        }
    1.23 +      }
    1.24 +
    1.25 +      private val block_size = 1024
    1.26 +    }
    1.27 +
    1.28 +    final class Commands private(val commands: Linear_Set[Command])
    1.29      {
    1.30 -      var i = offset
    1.31 -      for (command <- commands) yield {
    1.32 -        val start = i
    1.33 -        i += command.length
    1.34 -        (command, start)
    1.35 +      private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
    1.36 +      {
    1.37 +        val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
    1.38 +        var next_block = 0
    1.39 +        var last_stop = 0
    1.40 +        for ((command, start) <- Commands.starts(commands.iterator)) {
    1.41 +          last_stop = start + command.length
    1.42 +          while (last_stop + 1 > next_block) {
    1.43 +            blocks += (command -> start)
    1.44 +            next_block += Commands.block_size
    1.45 +          }
    1.46 +        }
    1.47 +        (blocks.toArray, Text.Range(0, last_stop))
    1.48 +      }
    1.49 +
    1.50 +      private def full_range: Text.Range = full_index._2
    1.51 +
    1.52 +      def range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
    1.53 +      {
    1.54 +        if (!commands.isEmpty && full_range.contains(i)) {
    1.55 +          val (cmd0, start0) = full_index._1(i / Commands.block_size)
    1.56 +          Node.Commands.starts(commands.iterator(cmd0), start0) dropWhile {
    1.57 +            case (cmd, start) => start + cmd.length <= i }
    1.58 +        }
    1.59 +        else Iterator.empty
    1.60        }
    1.61      }
    1.62 -
    1.63 -    private val block_size = 1024
    1.64    }
    1.65  
    1.66    final class Node private(
    1.67      val header: Node.Header = Node.bad_header("Bad theory header"),
    1.68      val perspective: Node.Perspective_Command =
    1.69        Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty),
    1.70 -    val commands: Linear_Set[Command] = Linear_Set.empty)
    1.71 +    _commands: Node.Commands = Node.Commands.empty)
    1.72    {
    1.73      def clear: Node = new Node(header = header)
    1.74  
    1.75      def update_header(new_header: Node.Header): Node =
    1.76 -      new Node(new_header, perspective, commands)
    1.77 +      new Node(new_header, perspective, _commands)
    1.78  
    1.79      def update_perspective(new_perspective: Node.Perspective_Command): Node =
    1.80 -      new Node(header, new_perspective, commands)
    1.81 +      new Node(header, new_perspective, _commands)
    1.82  
    1.83      def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
    1.84        perspective.required == other_perspective.required &&
    1.85        perspective.visible.same(other_perspective.visible) &&
    1.86        perspective.overlays == other_perspective.overlays
    1.87  
    1.88 -    def update_commands(new_commands: Linear_Set[Command]): Node =
    1.89 -      new Node(header, perspective, new_commands)
    1.90 -
    1.91 -
    1.92 -    /* commands */
    1.93 +    def commands: Linear_Set[Command] = _commands.commands
    1.94  
    1.95 -    private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
    1.96 -    {
    1.97 -      val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
    1.98 -      var next_block = 0
    1.99 -      var last_stop = 0
   1.100 -      for ((command, start) <- Node.command_starts(commands.iterator)) {
   1.101 -        last_stop = start + command.length
   1.102 -        while (last_stop + 1 > next_block) {
   1.103 -          blocks += (command -> start)
   1.104 -          next_block += Node.block_size
   1.105 -        }
   1.106 -      }
   1.107 -      (blocks.toArray, Text.Range(0, last_stop))
   1.108 -    }
   1.109 -
   1.110 -    def full_range: Text.Range = full_index._2
   1.111 +    def update_commands(new_commands: Linear_Set[Command]): Node =
   1.112 +      if (new_commands eq _commands) this
   1.113 +      else new Node(header, perspective, Node.Commands(new_commands))
   1.114  
   1.115      def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
   1.116 -    {
   1.117 -      if (!commands.isEmpty && full_range.contains(i)) {
   1.118 -        val (cmd0, start0) = full_index._1(i / Node.block_size)
   1.119 -        Node.command_starts(commands.iterator(cmd0), start0) dropWhile {
   1.120 -          case (cmd, start) => start + cmd.length <= i }
   1.121 -      }
   1.122 -      else Iterator.empty
   1.123 -    }
   1.124 +      _commands.range(i)
   1.125  
   1.126      def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
   1.127        command_range(range.start) takeWhile { case (_, start) => start < range.stop }
   1.128 @@ -200,7 +212,7 @@
   1.129      }
   1.130  
   1.131      def command_start(cmd: Command): Option[Text.Offset] =
   1.132 -      Node.command_starts(commands.iterator).find(_._1 == cmd).map(_._2)
   1.133 +      Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
   1.134    }
   1.135  
   1.136  
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Aug 07 19:59:58 2013 +0200
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Aug 07 20:32:54 2013 +0200
     2.3 @@ -193,7 +193,7 @@
     2.4    {
     2.5      eds match {
     2.6        case e :: es =>
     2.7 -        Document.Node.command_starts(commands.iterator).find {
     2.8 +        Document.Node.Commands.starts(commands.iterator).find {
     2.9            case (cmd, cmd_start) =>
    2.10              e.can_edit(cmd.source, cmd_start) ||
    2.11                e.is_insert && e.start == cmd_start + cmd.length