# HG changeset patch
# User wenzelm
# Date 1344539364 -7200
# Node ID 89b4e7d83d6f8c92afd0e2d42db758467bbf37a4
# Parent  ebfe3dd9f3f753bb269808f10b8abaa84b97a6ab
refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.;
tuned signature;

diff -r ebfe3dd9f3f7 -r 89b4e7d83d6f src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Thu Aug 09 19:51:29 2012 +0200
+++ b/src/Pure/General/linear_set.scala	Thu Aug 09 21:09:24 2012 +0200
@@ -76,6 +76,11 @@
             }
       }
 
+  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
+    ((hook, this) /: elems) {
+      case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
+    }._2
+
   def delete_after(hook: Option[A]): Linear_Set[A] =
     hook match {
       case None =>
@@ -105,24 +110,6 @@
           }
     }
 
-  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
-    ((hook, this) /: elems) {
-      case ((last_elem, set), elem) => (Some(elem), set.insert_after(last_elem, elem))
-    }._2
-
-  def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] =
-  {
-    if (isEmpty) this
-    else {
-      val next =
-        if (from == end) None
-        else if (from == None) start
-        else from.map(nexts(_))
-      if (next == to) this
-      else delete_after(from).delete_between(from, to)
-    }
-  }
-
 
   /* Set methods */
 
diff -r ebfe3dd9f3f7 -r 89b4e7d83d6f src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Aug 09 19:51:29 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Aug 09 21:09:24 2012 +0200
@@ -77,9 +77,9 @@
 
   /** parse spans **/
 
-  def parse_spans(toks: List[Token]): List[List[Token]] =
+  def parse_spans(toks: List[Token]): List[Command.Span] =
   {
-    val result = new mutable.ListBuffer[List[Token]]
+    val result = new mutable.ListBuffer[Command.Span]
     val span = new mutable.ListBuffer[Token]
 
     def flush() { if (!span.isEmpty) { result += span.toList; span.clear } }
@@ -196,36 +196,53 @@
 
   /* phase 2: recover command spans */
 
+  @tailrec private def chop_common(
+      cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
+    (cmds, spans) match {
+      case (c :: cs, s :: ss) if c.span == s => chop_common(cs, ss)
+      case _ => (cmds, spans)
+    }
+
+  private def trim_common(
+      cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
+  {
+    val (cmds1, spans1) = chop_common(cmds, spans)
+    val (rev_cmds2, rev_spans2) = chop_common(cmds1.reverse, spans1.reverse)
+    (rev_cmds2.reverse, rev_spans2.reverse)
+  }
+
   private def recover_spans(
     syntax: Outer_Syntax,
     node_name: Document.Node.Name,
+    perspective: Command.Perspective,
     old_commands: Linear_Set[Command]): Linear_Set[Command] =
   {
-    def bound(commands: Linear_Set[Command], cmd: Command): Command =
-      commands.iterator(cmd).dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
+    val visible = perspective.commands.iterator.filter(_.is_defined).toSet
+
+    def next_invisible_command(commands: Linear_Set[Command], from: Command): Command =
+      commands.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
+        .find(_.is_command) getOrElse commands.last
 
     @tailrec def recover(commands: Linear_Set[Command]): Linear_Set[Command] =
       commands.iterator.find(cmd => !cmd.is_defined) match {
         case Some(first_undefined) =>
-          val first = bound(commands.reverse, first_undefined)
-          val last = bound(commands, first_undefined)
-          val range = commands.iterator(first, last).toList
+          val first = next_invisible_command(commands.reverse, first_undefined)
+          val last = next_invisible_command(commands, first_undefined)
 
-          val spans0 = parse_spans(syntax.scan(range.map(_.source).mkString))
+          val cmds0 = commands.iterator(first, last).toList
+          val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString))
 
-          val (before_edit, spans1) =
-            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 && last.is_command && last.span == spans1.last)
-              (Some(last), spans1.take(spans1.length - 1))
-            else (commands.next(last), spans1)
-
-          val inserted = spans2.map(span => Command(Document.new_id(), node_name, span))
+          val (cmds, spans) = trim_common(cmds0, spans0)
           val new_commands =
-            commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
+            cmds match {
+              case Nil =>
+                assert(spans.isEmpty)
+                commands
+              case cmd :: _ =>
+                val hook = commands.prev(cmd)
+                val inserted = spans.map(span => Command(Document.new_id(), node_name, span))
+                (commands /: cmds)(_ - _).append_after(hook, inserted)
+            }
           recover(new_commands)
 
         case None => commands
@@ -271,7 +288,7 @@
         val node = nodes(name)
         val commands0 = node.commands
         val commands1 = edit_text(text_edits, commands0)
-        val commands2 = recover_spans(syntax, name, commands1)   // FIXME somewhat slow
+        val commands2 = recover_spans(syntax, name, node.perspective, commands1)   // FIXME somewhat slow
         val commands3 =
           if (reparse_set.contains(name)) reparse_spans(syntax, name, commands2)  // slow
           else commands2