1.1 --- a/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 11 18:26:38 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 11 18:28:31 2010 +0100
     1.3 @@ -67,16 +67,19 @@
     1.4        eds match {
     1.5          case e :: es =>
     1.6            command_starts(commands).find {   // FIXME relative search!
     1.7 -            case (cmd, cmd_start) => e.can_edit(cmd.length, cmd_start)
     1.8 +            case (cmd, cmd_start) =>
     1.9 +              e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length
    1.10            } match {
    1.11 -            // FIXME try to append after command
    1.12 -            case Some((cmd, cmd_start)) =>
    1.13 -              val (rest, source) = e.edit(cmd.source, cmd_start)
    1.14 -              val new_commands = commands.insert_after(Some(cmd), unparsed(source)) - cmd
    1.15 +            case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
    1.16 +              val (rest, text) = e.edit(cmd.source, cmd_start)
    1.17 +              val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
    1.18                edit_text(rest.toList ::: es, new_commands)
    1.19  
    1.20 +            case Some((cmd, cmd_start)) =>
    1.21 +              edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
    1.22 +
    1.23              case None =>
    1.24 -              require(e.isInstanceOf[Text_Edit.Insert] && e.start == 0)
    1.25 +              require(e.is_insert && e.start == 0)
    1.26                edit_text(es, commands.insert_after(None, unparsed(e.text)))
    1.27            }
    1.28          case Nil => commands
    1.29 @@ -84,9 +87,9 @@
    1.30      }
    1.31  
    1.32  
    1.33 -    /* phase 2: command range edits */
    1.34 +    /* phase 2: recover command spans */
    1.35  
    1.36 -    def edit_commands(commands: Linear_Set[Command]): Linear_Set[Command] =
    1.37 +    def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
    1.38      {
    1.39        // FIXME relative search!
    1.40        commands.elements.find(is_unparsed) match {
    1.41 @@ -96,12 +99,12 @@
    1.42            val suffix = commands.next(body.last)
    1.43  
    1.44            val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
    1.45 -          val span = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
    1.46 +          val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
    1.47  
    1.48            val (before_edit, spans1) =
    1.49 -            if (!span.isEmpty && Some(span.first) == prefix.map(_.span))
    1.50 -              (prefix, span.tail)
    1.51 -            else (if (prefix.isDefined) commands.prev(prefix.get) else None, span)
    1.52 +            if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
    1.53 +              (prefix, spans0.tail)
    1.54 +            else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
    1.55  
    1.56            val (after_edit, spans2) =
    1.57              if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
    1.58 @@ -111,7 +114,7 @@
    1.59            val inserted = spans2.map(span => new Command(session.create_id(), span))
    1.60            val new_commands =
    1.61              commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
    1.62 -          edit_commands(new_commands)
    1.63 +          parse_spans(new_commands)
    1.64  
    1.65          case None => commands
    1.66        }
    1.67 @@ -122,12 +125,11 @@
    1.68  
    1.69      val commands0 = old_doc.commands
    1.70      val commands1 = edit_text(edits, commands0)
    1.71 -    val commands2 = edit_commands(commands1)
    1.72 +    val commands2 = parse_spans(commands1)
    1.73  
    1.74      val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
    1.75      val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
    1.76  
    1.77 -    // FIXME tune
    1.78      val doc_edits =
    1.79        removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
    1.80        inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))