1.1 --- a/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 11 18:28:31 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 11 20:51:58 2010 +0100
     1.3 @@ -123,25 +123,28 @@
     1.4  
     1.5      /* phase 3: resulting document edits */
     1.6  
     1.7 -    val commands0 = old_doc.commands
     1.8 -    val commands1 = edit_text(edits, commands0)
     1.9 -    val commands2 = parse_spans(commands1)
    1.10 +    val result = Library.timeit("text_edits") {
    1.11 +      val commands0 = old_doc.commands
    1.12 +      val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
    1.13 +      val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
    1.14  
    1.15 -    val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
    1.16 -    val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
    1.17 +      val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
    1.18 +      val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
    1.19  
    1.20 -    val doc_edits =
    1.21 -      removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
    1.22 -      inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
    1.23 +      val doc_edits =
    1.24 +        removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
    1.25 +        inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
    1.26  
    1.27 -    val former_states = old_doc.assignment.join -- removed_commands
    1.28 +      val former_states = old_doc.assignment.join -- removed_commands
    1.29  
    1.30 -    phase0 = edits
    1.31 -    phase1 = commands1
    1.32 -    phase2 = commands2
    1.33 -    phase3 = doc_edits
    1.34 +      phase0 = edits
    1.35 +      phase1 = commands1
    1.36 +      phase2 = commands2
    1.37 +      phase3 = doc_edits
    1.38  
    1.39 -    (doc_edits, new Document(new_id, commands2, former_states))
    1.40 +      (doc_edits, new Document(new_id, commands2, former_states))
    1.41 +    }
    1.42 +    result
    1.43    }
    1.44  }
    1.45  
    1.46 @@ -184,9 +187,9 @@
    1.47      tmp_states = Map()
    1.48    }
    1.49  
    1.50 -  def current_state(cmd: Command): State =
    1.51 +  def current_state(cmd: Command): Option[State] =
    1.52    {
    1.53      require(assignment.is_finished)
    1.54 -    (assignment.join)(cmd).current_state
    1.55 +    (assignment.join).get(cmd).map(_.current_state)
    1.56    }
    1.57  }