refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.;
authorwenzelm
Thu Aug 09 21:09:24 2012 +0200 (2012-08-09)
changeset 4874889b4e7d83d6f
parent 48747 ebfe3dd9f3f7
child 48749 c197b3c3e7fa
refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.;
tuned signature;
src/Pure/General/linear_set.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/General/linear_set.scala	Thu Aug 09 19:51:29 2012 +0200
     1.2 +++ b/src/Pure/General/linear_set.scala	Thu Aug 09 21:09:24 2012 +0200
     1.3 @@ -76,6 +76,11 @@
     1.4              }
     1.5        }
     1.6  
     1.7 +  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
     1.8 +    ((hook, this) /: elems) {
     1.9 +      case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
    1.10 +    }._2
    1.11 +
    1.12    def delete_after(hook: Option[A]): Linear_Set[A] =
    1.13      hook match {
    1.14        case None =>
    1.15 @@ -105,24 +110,6 @@
    1.16            }
    1.17      }
    1.18  
    1.19 -  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
    1.20 -    ((hook, this) /: elems) {
    1.21 -      case ((last_elem, set), elem) => (Some(elem), set.insert_after(last_elem, elem))
    1.22 -    }._2
    1.23 -
    1.24 -  def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] =
    1.25 -  {
    1.26 -    if (isEmpty) this
    1.27 -    else {
    1.28 -      val next =
    1.29 -        if (from == end) None
    1.30 -        else if (from == None) start
    1.31 -        else from.map(nexts(_))
    1.32 -      if (next == to) this
    1.33 -      else delete_after(from).delete_between(from, to)
    1.34 -    }
    1.35 -  }
    1.36 -
    1.37  
    1.38    /* Set methods */
    1.39  
     2.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Aug 09 19:51:29 2012 +0200
     2.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Aug 09 21:09:24 2012 +0200
     2.3 @@ -77,9 +77,9 @@
     2.4  
     2.5    /** parse spans **/
     2.6  
     2.7 -  def parse_spans(toks: List[Token]): List[List[Token]] =
     2.8 +  def parse_spans(toks: List[Token]): List[Command.Span] =
     2.9    {
    2.10 -    val result = new mutable.ListBuffer[List[Token]]
    2.11 +    val result = new mutable.ListBuffer[Command.Span]
    2.12      val span = new mutable.ListBuffer[Token]
    2.13  
    2.14      def flush() { if (!span.isEmpty) { result += span.toList; span.clear } }
    2.15 @@ -196,36 +196,53 @@
    2.16  
    2.17    /* phase 2: recover command spans */
    2.18  
    2.19 +  @tailrec private def chop_common(
    2.20 +      cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
    2.21 +    (cmds, spans) match {
    2.22 +      case (c :: cs, s :: ss) if c.span == s => chop_common(cs, ss)
    2.23 +      case _ => (cmds, spans)
    2.24 +    }
    2.25 +
    2.26 +  private def trim_common(
    2.27 +      cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
    2.28 +  {
    2.29 +    val (cmds1, spans1) = chop_common(cmds, spans)
    2.30 +    val (rev_cmds2, rev_spans2) = chop_common(cmds1.reverse, spans1.reverse)
    2.31 +    (rev_cmds2.reverse, rev_spans2.reverse)
    2.32 +  }
    2.33 +
    2.34    private def recover_spans(
    2.35      syntax: Outer_Syntax,
    2.36      node_name: Document.Node.Name,
    2.37 +    perspective: Command.Perspective,
    2.38      old_commands: Linear_Set[Command]): Linear_Set[Command] =
    2.39    {
    2.40 -    def bound(commands: Linear_Set[Command], cmd: Command): Command =
    2.41 -      commands.iterator(cmd).dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
    2.42 +    val visible = perspective.commands.iterator.filter(_.is_defined).toSet
    2.43 +
    2.44 +    def next_invisible_command(commands: Linear_Set[Command], from: Command): Command =
    2.45 +      commands.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
    2.46 +        .find(_.is_command) getOrElse commands.last
    2.47  
    2.48      @tailrec def recover(commands: Linear_Set[Command]): Linear_Set[Command] =
    2.49        commands.iterator.find(cmd => !cmd.is_defined) match {
    2.50          case Some(first_undefined) =>
    2.51 -          val first = bound(commands.reverse, first_undefined)
    2.52 -          val last = bound(commands, first_undefined)
    2.53 -          val range = commands.iterator(first, last).toList
    2.54 +          val first = next_invisible_command(commands.reverse, first_undefined)
    2.55 +          val last = next_invisible_command(commands, first_undefined)
    2.56  
    2.57 -          val spans0 = parse_spans(syntax.scan(range.map(_.source).mkString))
    2.58 +          val cmds0 = commands.iterator(first, last).toList
    2.59 +          val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString))
    2.60  
    2.61 -          val (before_edit, spans1) =
    2.62 -            if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
    2.63 -              (Some(first), spans0.tail)
    2.64 -            else (commands.prev(first), spans0)
    2.65 -
    2.66 -          val (after_edit, spans2) =
    2.67 -            if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
    2.68 -              (Some(last), spans1.take(spans1.length - 1))
    2.69 -            else (commands.next(last), spans1)
    2.70 -
    2.71 -          val inserted = spans2.map(span => Command(Document.new_id(), node_name, span))
    2.72 +          val (cmds, spans) = trim_common(cmds0, spans0)
    2.73            val new_commands =
    2.74 -            commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
    2.75 +            cmds match {
    2.76 +              case Nil =>
    2.77 +                assert(spans.isEmpty)
    2.78 +                commands
    2.79 +              case cmd :: _ =>
    2.80 +                val hook = commands.prev(cmd)
    2.81 +                val inserted = spans.map(span => Command(Document.new_id(), node_name, span))
    2.82 +                (commands /: cmds)(_ - _).append_after(hook, inserted)
    2.83 +            }
    2.84            recover(new_commands)
    2.85  
    2.86          case None => commands
    2.87 @@ -271,7 +288,7 @@
    2.88          val node = nodes(name)
    2.89          val commands0 = node.commands
    2.90          val commands1 = edit_text(text_edits, commands0)
    2.91 -        val commands2 = recover_spans(syntax, name, commands1)   // FIXME somewhat slow
    2.92 +        val commands2 = recover_spans(syntax, name, node.perspective, commands1)   // FIXME somewhat slow
    2.93          val commands3 =
    2.94            if (reparse_set.contains(name)) reparse_spans(syntax, name, commands2)  // slow
    2.95            else commands2