# HG changeset patch # User wenzelm # Date 1274345026 -7200 # Node ID 449628c148cfc571eef0765ed9c6b49a1681c43f # Parent aaa7cac3e54aa9a13e3b5a26eb0345d595646c7c explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State]; diff -r aaa7cac3e54a -r 449628c148cf src/Pure/PIDE/command.scala --- 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 } diff -r aaa7cac3e54a -r 449628c148cf src/Pure/PIDE/document.scala --- 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) + } } } diff -r aaa7cac3e54a -r 449628c148cf src/Tools/jEdit/src/jedit/document_view.scala --- 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 } } diff -r aaa7cac3e54a -r 449628c148cf src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- 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) diff -r aaa7cac3e54a -r 449628c148cf src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- 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 diff -r aaa7cac3e54a -r 449628c148cf src/Tools/jEdit/src/jedit/isabelle_token_marker.scala --- 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) diff -r aaa7cac3e54a -r 449628c148cf src/Tools/jEdit/src/jedit/output_dockable.scala --- 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)