# HG changeset patch # User wenzelm # Date 1274565549 -7200 # Node ID dd3540a489f7ce4ce02e842365840a0819e2f024 # Parent e8906d992b692415d8d90f5fd47ef6fb7409773f parse_spans: cover full range including adjacent well-formed commands -- intermediate ignored and malformed commands are reparsed as well; diff -r e8906d992b69 -r dd3540a489f7 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat May 22 23:53:09 2010 +0200 +++ b/src/Pure/PIDE/document.scala Sat May 22 23:59:09 2010 +0200 @@ -82,25 +82,27 @@ def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] = { - // FIXME relative search! commands.iterator.find(is_unparsed) match { case Some(first_unparsed) => - val prefix = commands.prev(first_unparsed) - val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList - val suffix = commands.next(body.last) + val first = + commands.rev_iterator(first_unparsed).find(_.is_command) getOrElse commands.head + val last = + commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last + val range = + commands.iterator(first).takeWhile(_ != last).toList ::: List(last) - val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)) + val sources = range.flatMap(_.span.map(_.source)) val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString)) val (before_edit, spans1) = - if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span)) - (prefix, spans0.tail) - else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0) + if (!spans0.isEmpty && first.is_command && first.span == spans0.head) + (Some(first), spans0.tail) + else (commands.prev(first), spans0) val (after_edit, spans2) = - if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span)) - (suffix, spans1.take(spans1.length - 1)) - else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1) + if (!spans1.isEmpty && last.is_command && last.span == spans1.last) + (Some(last), spans1.take(spans1.length - 1)) + else (commands.next(last), spans1) val inserted = spans2.map(span => new Command(session.create_id(), span)) val new_commands =