explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
--- a/src/Pure/PIDE/command.scala Thu May 20 10:31:20 2010 +0200
+++ b/src/Pure/PIDE/command.scala Thu May 20 10:43:46 2010 +0200
@@ -20,6 +20,7 @@
val UNPROCESSED = Value("UNPROCESSED")
val FINISHED = Value("FINISHED")
val FAILED = Value("FAILED")
+ val UNDEFINED = Value("UNDEFINED")
}
case class HighlightInfo(highlight: String) { override def toString = highlight }
--- a/src/Pure/PIDE/document.scala Thu May 20 10:31:20 2010 +0200
+++ b/src/Pure/PIDE/document.scala Thu May 20 10:43:46 2010 +0200
@@ -175,9 +175,12 @@
System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
}
- def current_state(cmd: Command): Option[State] =
+ def current_state(cmd: Command): State =
{
require(assignment.is_finished)
- (assignment.join).get(cmd).map(_.current_state)
+ (assignment.join).get(cmd) match {
+ case Some(cmd_state) => cmd_state.current_state
+ case None => new State(cmd, Command.Status.UNDEFINED, Nil, cmd.empty_markup)
+ }
}
}
--- a/src/Tools/jEdit/src/jedit/document_view.scala Thu May 20 10:31:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu May 20 10:43:46 2010 +0200
@@ -25,11 +25,11 @@
{
def choose_color(command: Command, doc: Document): Color =
{
- doc.current_state(command).map(_.status) match {
- case Some(Command.Status.UNPROCESSED) => new Color(255, 228, 225)
- case Some(Command.Status.FINISHED) => new Color(234, 248, 255)
- case Some(Command.Status.FAILED) => new Color(255, 193, 193)
- case _ => Color.red
+ doc.current_state(command).status match {
+ case Command.Status.UNPROCESSED => new Color(255, 228, 225)
+ case Command.Status.FINISHED => new Color(234, 248, 255)
+ case Command.Status.FAILED => new Color(255, 193, 193)
+ case Command.Status.UNDEFINED => Color.red
}
}
@@ -146,7 +146,7 @@
val offset = model.from_current(document, text_area.xyToOffset(x, y))
document.command_at(offset) match {
case Some((command, command_start)) =>
- document.current_state(command).get.type_at(offset - command_start).getOrElse(null)
+ document.current_state(command).type_at(offset - command_start) getOrElse null
case None => null
}
}
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu May 20 10:31:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu May 20 10:43:46 2010 +0200
@@ -46,7 +46,7 @@
val offset = model.from_current(document, original_offset)
document.command_at(offset) match {
case Some((command, command_start)) =>
- document.current_state(command).get.ref_at(offset - command_start) match {
+ document.current_state(command).ref_at(offset - command_start) match {
case Some(ref) =>
val begin = model.to_current(document, command_start + ref.start)
val line = buffer.getLineOfOffset(begin)
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu May 20 10:31:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu May 20 10:43:46 2010 +0200
@@ -130,7 +130,7 @@
val root = data.root
val document = model.recent_document()
for ((command, command_start) <- document.command_range(0) if !stopped) {
- root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
+ root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
{
val content = command.source(node.start, node.stop).replace('\n', ' ')
val id = command.id
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu May 20 10:31:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu May 20 10:43:46 2010 +0200
@@ -116,7 +116,7 @@
var next_x = start
for {
(command, command_start) <- document.command_range(from(start), from(stop))
- markup <- document.current_state(command).get.highlight.flatten
+ markup <- document.current_state(command).highlight.flatten
val abs_start = to(command_start + markup.start)
val abs_stop = to(command_start + markup.stop)
if (abs_stop > start)
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Thu May 20 10:31:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Thu May 20 10:43:46 2010 +0200
@@ -46,7 +46,7 @@
val document = model.recent_document
document.command_at(view.getTextArea.getCaretPosition) match {
case Some((cmd, _)) =>
- output_actor ! Render(document.current_state(cmd).map(_.results) getOrElse Nil)
+ output_actor ! Render(document.current_state(cmd).results)
case None =>
}
case None =>
@@ -76,9 +76,7 @@
if (follow.selected) Document_Model(view.getBuffer) else None
} match {
case None =>
- case Some(model) =>
- val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil
- html_panel.render(body)
+ case Some(model) => html_panel.render(model.recent_document.current_state(cmd).results)
}
case bad => System.err.println("output_actor: ignoring bad message " + bad)