1.1 --- a/src/Tools/jEdit/src/proofdocument/command.scala	Mon Jan 11 01:40:18 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/command.scala	Mon Jan 11 12:17:47 2010 +0100
     1.3 @@ -35,10 +35,6 @@
     1.4      val span: Thy_Syntax.Span)
     1.5    extends Session.Entity
     1.6  {
     1.7 -  // FIXME override equality as well
     1.8 -  override def hashCode = id.hashCode
     1.9 -
    1.10 -
    1.11    /* classification */
    1.12  
    1.13    def is_command: Boolean = !span.isEmpty && span.first.is_command

     2.1 --- a/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 11 01:40:18 2010 +0100
     2.2 +++ b/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 11 12:17:47 2010 +0100
     2.3 @@ -45,7 +45,7 @@
     2.4    var phase1: Linear_Set[Command] = null
     2.5    var phase2: Linear_Set[Command] = null
     2.6    var phase3: List[Edit] = null
     2.7 -  var raw_source = ""
     2.8 +  var raw_source: String = null
     2.9  
    2.10  
    2.11  
    2.12 @@ -58,18 +58,17 @@
    2.13    {
    2.14      require(old_doc.assignment.is_finished)
    2.15  
    2.16 -    System.err.println(edits)
    2.17      phase0 = edits
    2.18  
    2.19  
    2.20      /* unparsed dummy commands */
    2.21  
    2.22      def unparsed(source: String) =
    2.23 -      new Command(session.create_id(), List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
    2.24 +      new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
    2.25  
    2.26 -    def is_unparsed(command: Command) = command.span.exists(_.is_unparsed)
    2.27 +    def is_unparsed(command: Command) = command.id == null
    2.28  
    2.29 -    require(!old_doc.commands.exists(is_unparsed))
    2.30 +    assert(!old_doc.commands.exists(is_unparsed))
    2.31  
    2.32  
    2.33      /* phase 1: edit individual command source */
    2.34 @@ -82,7 +81,7 @@
    2.35          case e :: es =>
    2.36            command_starts(commands).find {   // FIXME relative search!
    2.37              case (cmd, cmd_start) => e.can_edit(cmd.length, cmd_start)
    2.38 -          } match {
    2.39 +          } match {  // FIXME try to append after command
    2.40              case Some((cmd, cmd_start)) =>
    2.41                val (rest, source) = e.edit(cmd.source, cmd_start)
    2.42                // FIXME Linear_Set.edit (?)
    2.43 @@ -116,6 +115,7 @@
    2.44  
    2.45            val source =
    2.46              (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)).mkString
    2.47 +          assert(source != "")
    2.48            raw_source = source
    2.49            
    2.50            val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(source))
    2.51 @@ -140,7 +140,8 @@
    2.52          case None =>
    2.53        }
    2.54      }
    2.55 -
    2.56 +    edit_commands()
    2.57 +    
    2.58      phase2 = commands
    2.59  
    2.60  
    2.61 @@ -149,9 +150,9 @@
    2.62      val removed_commands = old_doc.commands.elements.filter(!commands.contains(_)).toList
    2.63      val inserted_commands = commands.elements.filter(!old_doc.commands.contains(_)).toList
    2.64  
    2.65 -    // FIXME tune
    2.66 +    // FIXME proper order
    2.67      val doc_edits =
    2.68 -      removed_commands.reverse.map(cmd => (Some(cmd), None)) :::
    2.69 +      removed_commands.reverse.map(cmd => (commands.prev(cmd), None)) :::
    2.70        inserted_commands.map(cmd => (commands.prev(cmd), Some(cmd)))
    2.71  
    2.72      val former_states = old_doc.assignment.join -- removed_commands