1.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Jan 11 18:28:31 2010 +0100
1.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Jan 11 20:51:58 2010 +0100
1.3 @@ -25,10 +25,10 @@
1.4 {
1.5 def choose_color(command: Command, doc: Document): Color =
1.6 {
1.7 - doc.current_state(command).status match {
1.8 - case Command.Status.UNPROCESSED => new Color(255, 228, 225)
1.9 - case Command.Status.FINISHED => new Color(234, 248, 255)
1.10 - case Command.Status.FAILED => new Color(255, 193, 193)
1.11 + doc.current_state(command).map(_.status) match {
1.12 + case Some(Command.Status.UNPROCESSED) => new Color(255, 228, 225)
1.13 + case Some(Command.Status.FINISHED) => new Color(234, 248, 255)
1.14 + case Some(Command.Status.FAILED) => new Color(255, 193, 193)
1.15 case _ => Color.red
1.16 }
1.17 }
1.18 @@ -146,7 +146,7 @@
1.19 val offset = model.from_current(document, text_area.xyToOffset(x, y))
1.20 document.command_at(offset) match {
1.21 case Some((command, command_start)) =>
1.22 - document.current_state(command).type_at(offset - command_start).getOrElse(null)
1.23 + document.current_state(command).get.type_at(offset - command_start).getOrElse(null)
1.24 case None => null
1.25 }
1.26 }
2.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Jan 11 18:28:31 2010 +0100
2.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Jan 11 20:51:58 2010 +0100
2.3 @@ -45,7 +45,7 @@
2.4 val offset = model.from_current(document, original_offset)
2.5 document.command_at(offset) match {
2.6 case Some((command, command_start)) =>
2.7 - document.current_state(command).ref_at(offset - command_start) match {
2.8 + document.current_state(command).get.ref_at(offset - command_start) match {
2.9 case Some(ref) =>
2.10 val begin = model.to_current(document, command_start + ref.start)
2.11 val line = buffer.getLineOfOffset(begin)
3.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Jan 11 18:28:31 2010 +0100
3.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Jan 11 20:51:58 2010 +0100
3.3 @@ -45,7 +45,7 @@
3.4 case Some(model) =>
3.5 val document = model.recent_document()
3.6 for ((command, command_start) <- document.command_range(0) if !stopped) {
3.7 - root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
3.8 + root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
3.9 {
3.10 val content = command.source(node.start, node.stop)
3.11 val id = command.id
4.1 --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Mon Jan 11 18:28:31 2010 +0100
4.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Mon Jan 11 20:51:58 2010 +0100
4.3 @@ -116,7 +116,7 @@
4.4 var next_x = start
4.5 for {
4.6 (command, command_start) <- document.command_range(from(start), from(stop))
4.7 - markup <- document.current_state(command).highlight.flatten
4.8 + markup <- document.current_state(command).get.highlight.flatten
4.9 val abs_start = to(command_start + markup.start)
4.10 val abs_stop = to(command_start + markup.stop)
4.11 if (abs_stop > start)
5.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jan 11 18:28:31 2010 +0100
5.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jan 11 20:51:58 2010 +0100
5.3 @@ -38,9 +38,7 @@
5.4 Swing_Thread.now { Document_Model(view.getBuffer) } match {
5.5 case None =>
5.6 case Some(model) =>
5.7 - val body =
5.8 - if (cmd == null) Nil // FIXME ??
5.9 - else model.recent_document.current_state(cmd).results
5.10 + val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil
5.11 html_panel.render(body)
5.12 }
5.13
6.1 --- a/src/Tools/jEdit/src/proofdocument/document.scala Mon Jan 11 18:28:31 2010 +0100
6.2 +++ b/src/Tools/jEdit/src/proofdocument/document.scala Mon Jan 11 20:51:58 2010 +0100
6.3 @@ -123,25 +123,28 @@
6.4
6.5 /* phase 3: resulting document edits */
6.6
6.7 - val commands0 = old_doc.commands
6.8 - val commands1 = edit_text(edits, commands0)
6.9 - val commands2 = parse_spans(commands1)
6.10 + val result = Library.timeit("text_edits") {
6.11 + val commands0 = old_doc.commands
6.12 + val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
6.13 + val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
6.14
6.15 - val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
6.16 - val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
6.17 + val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
6.18 + val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
6.19
6.20 - val doc_edits =
6.21 - removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
6.22 - inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
6.23 + val doc_edits =
6.24 + removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
6.25 + inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
6.26
6.27 - val former_states = old_doc.assignment.join -- removed_commands
6.28 + val former_states = old_doc.assignment.join -- removed_commands
6.29
6.30 - phase0 = edits
6.31 - phase1 = commands1
6.32 - phase2 = commands2
6.33 - phase3 = doc_edits
6.34 + phase0 = edits
6.35 + phase1 = commands1
6.36 + phase2 = commands2
6.37 + phase3 = doc_edits
6.38
6.39 - (doc_edits, new Document(new_id, commands2, former_states))
6.40 + (doc_edits, new Document(new_id, commands2, former_states))
6.41 + }
6.42 + result
6.43 }
6.44 }
6.45
6.46 @@ -184,9 +187,9 @@
6.47 tmp_states = Map()
6.48 }
6.49
6.50 - def current_state(cmd: Command): State =
6.51 + def current_state(cmd: Command): Option[State] =
6.52 {
6.53 require(assignment.is_finished)
6.54 - (assignment.join)(cmd).current_state
6.55 + (assignment.join).get(cmd).map(_.current_state)
6.56 }
6.57 }