1.1 --- a/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 11 01:40:18 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 11 12:17:47 2010 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4    var phase1: Linear_Set[Command] = null
     1.5    var phase2: Linear_Set[Command] = null
     1.6    var phase3: List[Edit] = null
     1.7 -  var raw_source = ""
     1.8 +  var raw_source: String = null
     1.9  
    1.10  
    1.11  
    1.12 @@ -58,18 +58,17 @@
    1.13    {
    1.14      require(old_doc.assignment.is_finished)
    1.15  
    1.16 -    System.err.println(edits)
    1.17      phase0 = edits
    1.18  
    1.19  
    1.20      /* unparsed dummy commands */
    1.21  
    1.22      def unparsed(source: String) =
    1.23 -      new Command(session.create_id(), List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
    1.24 +      new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
    1.25  
    1.26 -    def is_unparsed(command: Command) = command.span.exists(_.is_unparsed)
    1.27 +    def is_unparsed(command: Command) = command.id == null
    1.28  
    1.29 -    require(!old_doc.commands.exists(is_unparsed))
    1.30 +    assert(!old_doc.commands.exists(is_unparsed))
    1.31  
    1.32  
    1.33      /* phase 1: edit individual command source */
    1.34 @@ -82,7 +81,7 @@
    1.35          case e :: es =>
    1.36            command_starts(commands).find {   // FIXME relative search!
    1.37              case (cmd, cmd_start) => e.can_edit(cmd.length, cmd_start)
    1.38 -          } match {
    1.39 +          } match {  // FIXME try to append after command
    1.40              case Some((cmd, cmd_start)) =>
    1.41                val (rest, source) = e.edit(cmd.source, cmd_start)
    1.42                // FIXME Linear_Set.edit (?)
    1.43 @@ -116,6 +115,7 @@
    1.44  
    1.45            val source =
    1.46              (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)).mkString
    1.47 +          assert(source != "")
    1.48            raw_source = source
    1.49            
    1.50            val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(source))
    1.51 @@ -140,7 +140,8 @@
    1.52          case None =>
    1.53        }
    1.54      }
    1.55 -
    1.56 +    edit_commands()
    1.57 +    
    1.58      phase2 = commands
    1.59  
    1.60  
    1.61 @@ -149,9 +150,9 @@
    1.62      val removed_commands = old_doc.commands.elements.filter(!commands.contains(_)).toList
    1.63      val inserted_commands = commands.elements.filter(!old_doc.commands.contains(_)).toList
    1.64  
    1.65 -    // FIXME tune
    1.66 +    // FIXME proper order
    1.67      val doc_edits =
    1.68 -      removed_commands.reverse.map(cmd => (Some(cmd), None)) :::
    1.69 +      removed_commands.reverse.map(cmd => (commands.prev(cmd), None)) :::
    1.70        inserted_commands.map(cmd => (commands.prev(cmd), Some(cmd)))
    1.71  
    1.72      val former_states = old_doc.assignment.join -- removed_commands