src/Pure/Thy/thy_syntax.scala
changeset 48748 89b4e7d83d6f
parent 48747 ebfe3dd9f3f7
child 48754 c2c1e5944536
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Aug 09 19:51:29 2012 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Aug 09 21:09:24 2012 +0200
     1.3 @@ -77,9 +77,9 @@
     1.4  
     1.5    /** parse spans **/
     1.6  
     1.7 -  def parse_spans(toks: List[Token]): List[List[Token]] =
     1.8 +  def parse_spans(toks: List[Token]): List[Command.Span] =
     1.9    {
    1.10 -    val result = new mutable.ListBuffer[List[Token]]
    1.11 +    val result = new mutable.ListBuffer[Command.Span]
    1.12      val span = new mutable.ListBuffer[Token]
    1.13  
    1.14      def flush() { if (!span.isEmpty) { result += span.toList; span.clear } }
    1.15 @@ -196,36 +196,53 @@
    1.16  
    1.17    /* phase 2: recover command spans */
    1.18  
    1.19 +  @tailrec private def chop_common(
    1.20 +      cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
    1.21 +    (cmds, spans) match {
    1.22 +      case (c :: cs, s :: ss) if c.span == s => chop_common(cs, ss)
    1.23 +      case _ => (cmds, spans)
    1.24 +    }
    1.25 +
    1.26 +  private def trim_common(
    1.27 +      cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
    1.28 +  {
    1.29 +    val (cmds1, spans1) = chop_common(cmds, spans)
    1.30 +    val (rev_cmds2, rev_spans2) = chop_common(cmds1.reverse, spans1.reverse)
    1.31 +    (rev_cmds2.reverse, rev_spans2.reverse)
    1.32 +  }
    1.33 +
    1.34    private def recover_spans(
    1.35      syntax: Outer_Syntax,
    1.36      node_name: Document.Node.Name,
    1.37 +    perspective: Command.Perspective,
    1.38      old_commands: Linear_Set[Command]): Linear_Set[Command] =
    1.39    {
    1.40 -    def bound(commands: Linear_Set[Command], cmd: Command): Command =
    1.41 -      commands.iterator(cmd).dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
    1.42 +    val visible = perspective.commands.iterator.filter(_.is_defined).toSet
    1.43 +
    1.44 +    def next_invisible_command(commands: Linear_Set[Command], from: Command): Command =
    1.45 +      commands.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
    1.46 +        .find(_.is_command) getOrElse commands.last
    1.47  
    1.48      @tailrec def recover(commands: Linear_Set[Command]): Linear_Set[Command] =
    1.49        commands.iterator.find(cmd => !cmd.is_defined) match {
    1.50          case Some(first_undefined) =>
    1.51 -          val first = bound(commands.reverse, first_undefined)
    1.52 -          val last = bound(commands, first_undefined)
    1.53 -          val range = commands.iterator(first, last).toList
    1.54 +          val first = next_invisible_command(commands.reverse, first_undefined)
    1.55 +          val last = next_invisible_command(commands, first_undefined)
    1.56  
    1.57 -          val spans0 = parse_spans(syntax.scan(range.map(_.source).mkString))
    1.58 +          val cmds0 = commands.iterator(first, last).toList
    1.59 +          val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString))
    1.60  
    1.61 -          val (before_edit, spans1) =
    1.62 -            if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
    1.63 -              (Some(first), spans0.tail)
    1.64 -            else (commands.prev(first), spans0)
    1.65 -
    1.66 -          val (after_edit, spans2) =
    1.67 -            if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
    1.68 -              (Some(last), spans1.take(spans1.length - 1))
    1.69 -            else (commands.next(last), spans1)
    1.70 -
    1.71 -          val inserted = spans2.map(span => Command(Document.new_id(), node_name, span))
    1.72 +          val (cmds, spans) = trim_common(cmds0, spans0)
    1.73            val new_commands =
    1.74 -            commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
    1.75 +            cmds match {
    1.76 +              case Nil =>
    1.77 +                assert(spans.isEmpty)
    1.78 +                commands
    1.79 +              case cmd :: _ =>
    1.80 +                val hook = commands.prev(cmd)
    1.81 +                val inserted = spans.map(span => Command(Document.new_id(), node_name, span))
    1.82 +                (commands /: cmds)(_ - _).append_after(hook, inserted)
    1.83 +            }
    1.84            recover(new_commands)
    1.85  
    1.86          case None => commands
    1.87 @@ -271,7 +288,7 @@
    1.88          val node = nodes(name)
    1.89          val commands0 = node.commands
    1.90          val commands1 = edit_text(text_edits, commands0)
    1.91 -        val commands2 = recover_spans(syntax, name, commands1)   // FIXME somewhat slow
    1.92 +        val commands2 = recover_spans(syntax, name, node.perspective, commands1)   // FIXME somewhat slow
    1.93          val commands3 =
    1.94            if (reparse_set.contains(name)) reparse_spans(syntax, name, commands2)  // slow
    1.95            else commands2