identify dialogs via official serial and maintain as result message;
clarified Protocol.is_inlined: suppress result/tracing/state messages uniformly;
cumulate_markup/select_markup depending on command state;
explicit Rendering.output_messages;
tuned source structure;
--- a/src/Pure/PIDE/active.ML Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/active.ML Thu Dec 13 13:52:18 2012 +0100
@@ -12,7 +12,7 @@
val sendback_markup_implicit: string -> string
val sendback_markup: string -> string
val dialog: unit -> (string -> Markup.T) * string future
- val dialog_result: string -> string -> unit
+ val dialog_result: serial -> string -> unit
end;
structure Active: ACTIVE =
@@ -42,22 +42,20 @@
(* dialog via document content *)
-val new_name = string_of_int o Synchronized.counter ();
-
-val dialogs = Synchronized.var "Active.dialogs" (Symtab.empty: string future Symtab.table);
+val dialogs = Synchronized.var "Active.dialogs" (Inttab.empty: string future Inttab.table);
fun dialog () =
let
- val name = new_name ();
- fun abort () = Synchronized.change dialogs (Symtab.delete_safe name);
+ val i = serial ();
+ fun abort () = Synchronized.change dialogs (Inttab.delete_safe i);
val promise = Future.promise abort : string future;
- val _ = Synchronized.change dialogs (Symtab.update_new (name, promise));
- fun mk_markup result = Markup.properties (explicit_id ()) (Markup.dialog name result);
+ val _ = Synchronized.change dialogs (Inttab.update_new (i, promise));
+ fun mk_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
in (mk_markup, promise) end;
-fun dialog_result name result =
+fun dialog_result i result =
Synchronized.change_result dialogs
- (fn tab => (Symtab.lookup tab name, Symtab.delete_safe name tab))
+ (fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab))
|> (fn NONE => () | SOME promise => Future.fulfill promise result);
end;
--- a/src/Pure/PIDE/command.scala Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/command.scala Thu Dec 13 13:52:18 2012 +0100
@@ -73,10 +73,10 @@
val st0 = copy(results = results + (i -> message1))
val st1 =
- if (Protocol.is_tracing(message)) st0
- else
+ if (Protocol.is_inlined(message))
(st0 /: Protocol.message_positions(command, message))(
(st, range) => st.add_markup(Text.Info(range, message2)))
+ else st0
st1
case _ => System.err.println("Ignored message without serial number: " + message); this
--- a/src/Pure/PIDE/document.scala Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/document.scala Thu Dec 13 13:52:18 2012 +0100
@@ -280,9 +280,9 @@
def revert(range: Text.Range): Text.Range
def eq_markup(other: Snapshot): Boolean
def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
- result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
+ result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
def select_markup[A](range: Text.Range, elements: Option[Set[String]],
- result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
+ result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
}
type Assign = List[(Document.Command_ID, Option[Document.Exec_ID])] // exec state assignment
@@ -506,29 +506,34 @@
})
def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
- result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
+ result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
{
val former_range = revert(range)
for {
(command, command_start) <- node.command_range(former_range).toStream
- Text.Info(r0, a) <- state.command_state(version, command).markup.
+ st = state.command_state(version, command)
+ res = result(st)
+ Text.Info(r0, a) <- st.markup.
cumulate[A]((former_range - command_start).restrict(command.range), info, elements,
{
case (a, Text.Info(r0, b))
- if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
- result((a, Text.Info(convert(r0 + command_start), b)))
+ if res.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
+ res((a, Text.Info(convert(r0 + command_start), b)))
})
} yield Text.Info(convert(r0 + command_start), a)
}
def select_markup[A](range: Text.Range, elements: Option[Set[String]],
- result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]] =
+ result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]] =
{
- val result1 =
+ def result1(st: Command.State) =
+ {
+ val res = result(st)
new PartialFunction[(Option[A], Text.Markup), Option[A]] {
- def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2)
- def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2))
+ def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = res.isDefinedAt(arg._2)
+ def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(res(arg._2))
}
+ }
for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1))
yield Text.Info(r, x)
}
--- a/src/Pure/PIDE/markup.ML Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/markup.ML Thu Dec 13 13:52:18 2012 +0100
@@ -96,12 +96,6 @@
val proof_stateN: string val proof_state: int -> T
val stateN: string val state: T
val subgoalN: string val subgoal: T
- val graphviewN: string
- val sendbackN: string
- val paddingN: string
- val padding_line: string * string
- val dialogN: string val dialog: string -> string -> T
- val intensifyN: string val intensify: T
val taskN: string
val acceptedN: string val accepted: T
val forkedN: string val forked: T
@@ -122,6 +116,12 @@
val reportN: string val report: T
val no_reportN: string val no_report: T
val badN: string val bad: T
+ val intensifyN: string val intensify: T
+ val graphviewN: string
+ val sendbackN: string
+ val paddingN: string
+ val padding_line: string * string
+ val dialogN: string val dialog: serial -> string -> T
val functionN: string
val assign_execs: Properties.T
val removed_versions: Properties.T
@@ -339,20 +339,6 @@
val (subgoalN, subgoal) = markup_elem "subgoal";
-(* active areas *)
-
-val graphviewN = "graphview";
-
-val sendbackN = "sendback";
-val paddingN = "padding";
-val padding_line = (paddingN, lineN);
-
-val dialogN = "dialog";
-fun dialog name result = (dialogN, [(nameN, name), ("result", result)]);
-
-val (intensifyN, intensify) = markup_elem "intensify";
-
-
(* command status *)
val taskN = "task";
@@ -385,6 +371,20 @@
val (badN, bad) = markup_elem "bad";
+val (intensifyN, intensify) = markup_elem "intensify";
+
+
+(* active areas *)
+
+val graphviewN = "graphview";
+
+val sendbackN = "sendback";
+val paddingN = "padding";
+val padding_line = (paddingN, lineN);
+
+val dialogN = "dialog";
+fun dialog i result = (dialogN, [(serialN, print_int i), ("result", result)]);
+
(* protocol message functions *)
--- a/src/Pure/PIDE/markup.scala Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/markup.scala Thu Dec 13 13:52:18 2012 +0100
@@ -213,30 +213,6 @@
val SUBGOAL = "subgoal"
- /* active areas */
-
- val GRAPHVIEW = "graphview"
-
- val SENDBACK = "sendback"
- val PADDING = "padding"
- val PADDING_LINE = (PADDING, LINE)
-
- val DIALOG = "dialog"
- val DIALOG_RESULT = "dialog_result"
- val Result = new Properties.String("result")
-
- object Dialog_Args
- {
- def unapply(props: Properties.T): Option[(String, String)] =
- (props, props) match {
- case (Markup.Name(name), Markup.Result(result)) => Some((name, result))
- case _ => None
- }
- }
-
- val INTENSIFY = "intensify"
-
-
/* command status */
val TASK = "task"
@@ -270,6 +246,7 @@
val INIT = "init"
val STATUS = "status"
val REPORT = "report"
+ val RESULT = "result"
val WRITELN = "writeln"
val TRACING = "tracing"
val WARNING = "warning"
@@ -298,6 +275,20 @@
val BAD = "bad"
+ val INTENSIFY = "intensify"
+
+
+ /* active areas */
+
+ val GRAPHVIEW = "graphview"
+
+ val SENDBACK = "sendback"
+ val PADDING = "padding"
+ val PADDING_LINE = (PADDING, LINE)
+
+ val DIALOG = "dialog"
+ val Result = new Properties.String("result")
+
/* protocol message functions */
--- a/src/Pure/PIDE/protocol.ML Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/protocol.ML Thu Dec 13 13:52:18 2012 +0100
@@ -77,8 +77,8 @@
val _ =
Isabelle_Process.protocol_command "Document.dialog_result"
- (fn [name, result] =>
- Active.dialog_result name result
+ (fn [serial, result] =>
+ Active.dialog_result (Markup.parse_int serial) result
handle exn => if Exn.is_interrupt exn then () else reraise exn);
val _ =
--- a/src/Pure/PIDE/protocol.scala Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala Thu Dec 13 13:52:18 2012 +0100
@@ -145,6 +145,15 @@
/* specific messages */
+ def is_inlined(msg: XML.Tree): Boolean =
+ !(is_result(msg) || is_tracing(msg) || is_state(msg))
+
+ def is_result(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.RESULT, _), _) => true
+ case _ => false
+ }
+
def is_tracing(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Markup.TRACING, _), _) => true
@@ -152,6 +161,15 @@
case _ => false
}
+ def is_state(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.WRITELN, _),
+ List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+ case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
+ List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+ case _ => false
+ }
+
def is_warning(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Markup.WARNING, _), _) => true
@@ -166,14 +184,41 @@
case _ => false
}
- def is_state(msg: XML.Tree): Boolean =
- msg match {
- case XML.Elem(Markup(Markup.WRITELN, _),
- List(XML.Elem(Markup(Markup.STATE, _), _))) => true
- case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
- List(XML.Elem(Markup(Markup.STATE, _), _))) => true
- case _ => false
- }
+
+ /* dialogs */
+
+ object Dialog_Args
+ {
+ def unapply(props: Properties.T): Option[(Document.ID, Long, String)] =
+ (props, props, props) match {
+ case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
+ Some((id, serial, result))
+ case _ => None
+ }
+ }
+
+ object Dialog
+ {
+ def unapply(tree: XML.Tree): Option[(Document.ID, Long, String)] =
+ tree match {
+ case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
+ Some((id, serial, result))
+ case _ => None
+ }
+ }
+
+ object Dialog_Result
+ {
+ def apply(serial: Long, result: String): XML.Elem =
+ XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), List(XML.Text(result)))
+
+ def unapply(tree: XML.Tree): Option[(Long, String)] =
+ tree match {
+ case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), List(XML.Text(result))) =>
+ Some((serial, result))
+ case _ => None
+ }
+ }
/* reported positions */
@@ -205,7 +250,7 @@
}
val set = positions(Set.empty, message)
- if (set.isEmpty && !is_state(message))
+ if (set.isEmpty)
set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
else set
}
@@ -271,9 +316,9 @@
/* dialog via document content */
- def dialog_result(name: String, result: String)
+ def dialog_result(serial: Long, result: String)
{
- input("Document.dialog_result", name, result)
+ input("Document.dialog_result", Properties.Value.Long(serial), result)
}
--- a/src/Pure/ROOT.ML Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/ROOT.ML Thu Dec 13 13:52:18 2012 +0100
@@ -98,6 +98,8 @@
use "Concurrent/mailbox.ML";
use "Concurrent/cache.ML";
+use "PIDE/active.ML";
+
(* fundamental structures *)
@@ -251,7 +253,6 @@
use "Thy/term_style.ML";
use "Thy/thy_output.ML";
use "Thy/thy_syntax.ML";
-use "PIDE/active.ML";
use "PIDE/command.ML";
use "Isar/outer_syntax.ML";
use "General/graph_display.ML";
--- a/src/Pure/System/session.scala Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/System/session.scala Thu Dec 13 13:52:18 2012 +0100
@@ -26,7 +26,7 @@
case class Global_Options(options: Options)
case object Caret_Focus
case class Raw_Edits(edits: List[Document.Edit_Text])
- case class Dialog_Result(id: Document.ID, name: String, result: String)
+ case class Dialog_Result(id: Document.ID, serial: Long, result: String)
case class Commands_Changed(
assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
@@ -420,13 +420,9 @@
reply(())
- case Session.Dialog_Result(id, name, result) if prover.isDefined =>
- prover.get.dialog_result(name, result)
-
- val dialog_result =
- XML.Elem(Markup(Markup.DIALOG_RESULT, Markup.Name(name) ::: Markup.Result(result)), Nil)
- handle_output(new Isabelle_Process.Output(
- XML.Elem(Markup(Markup.STATUS, Position.Id(id)), List(dialog_result))))
+ case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
+ prover.get.dialog_result(serial, result)
+ handle_output(new Isabelle_Process.Output(Protocol.Dialog_Result(serial, result)))
case Messages(msgs) =>
msgs foreach {
@@ -479,6 +475,6 @@
def update(edits: List[Document.Edit_Text])
{ session_actor !? Session.Raw_Edits(edits) }
- def dialog_result(id: Document.ID, name: String, result: String)
- { session_actor ! Session.Dialog_Result(id, name, result) }
+ def dialog_result(id: Document.ID, serial: Long, result: String)
+ { session_actor ! Session.Dialog_Result(id, serial, result) }
}
--- a/src/Tools/jEdit/src/active.scala Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Tools/jEdit/src/active.scala Thu Dec 13 13:52:18 2012 +0100
@@ -44,23 +44,6 @@
if (!snapshot.is_outdated) {
elem match {
- case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
- props match {
- case Position.Id(exec_id) =>
- try_replace_command(exec_id, text)
- case _ =>
- if (props.exists(_ == Markup.PADDING_LINE))
- Isabelle.insert_line_padding(text_area, text)
- else text_area.setSelectedText(text)
- }
-
- case XML.Elem(Markup(Markup.DIALOG, props), _) =>
- (props, props, props) match {
- case (Position.Id(id), Markup.Name(name), Markup.Result(result)) =>
- model.session.dialog_result(id, name, result)
- case _ =>
- }
-
case XML.Elem(Markup(Markup.GRAPHVIEW, Position.Id(exec_id)), body) =>
default_thread_pool.submit(() =>
{
@@ -72,7 +55,24 @@
Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
})
+ case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
+ props match {
+ case Position.Id(exec_id) =>
+ try_replace_command(exec_id, text)
+ case _ =>
+ if (props.exists(_ == Markup.PADDING_LINE))
+ Isabelle.insert_line_padding(text_area, text)
+ else text_area.setSelectedText(text)
+ }
+
case _ =>
+ // FIXME pattern match problem in scala-2.9.2 (!??)
+ elem match {
+ case Protocol.Dialog(id, serial, result) =>
+ model.session.dialog_result(id, serial, result)
+
+ case _ =>
+ }
}
}
}
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Thu Dec 13 13:52:18 2012 +0100
@@ -71,12 +71,8 @@
val new_output =
if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
- // FIXME avoid intrusion of Protocol
- // FIXME proper cumulation order!?
- val status = new_state.status.filterNot(m => Protocol.command_status_markup(m.name))
-
- val results = new_state.results.iterator.map(_._2).toList
- results.map(tree => (tree /: status) { case (t, m) => XML.Elem(m, List(t)) })
+ val rendering = Rendering(new_snapshot, PIDE.options.value)
+ rendering.output_messages(new_state)
}
else current_output
--- a/src/Tools/jEdit/src/rendering.scala Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Thu Dec 13 13:52:18 2012 +0100
@@ -165,7 +165,7 @@
val results =
snapshot.cumulate_markup[(Protocol.Status, Int)](
range, (Protocol.Status.init, 0),
- Some(Protocol.command_status_markup + Markup.WARNING + Markup.ERROR),
+ Some(Protocol.command_status_markup + Markup.WARNING + Markup.ERROR), _ =>
{
case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
@@ -198,7 +198,7 @@
def highlight(range: Text.Range): Option[Text.Info[Color]] =
{
- snapshot.select_markup(range, Some(highlight_include),
+ snapshot.select_markup(range, Some(highlight_include), _ =>
{
case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if highlight_include(name) =>
Text.Info(snapshot.convert(info_range), highlight_color)
@@ -210,7 +210,7 @@
def hyperlink(range: Text.Range): Option[Text.Info[Hyperlink]] =
{
- snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include),
+ snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include), _ =>
{
case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
if Path.is_ok(name) =>
@@ -250,11 +250,11 @@
}
- private val active_include = Set(Markup.SENDBACK, Markup.DIALOG, Markup.GRAPHVIEW)
+ private val active_include = Set(Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG)
def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
- snapshot.select_markup(range, Some(active_include),
- {
+ snapshot.select_markup(range, Some(active_include), command_state =>
+ { // FIXME inactive dialog
case Text.Info(info_range, elem @ XML.Elem(markup, _))
if active_include(markup.name) => Text.Info(snapshot.convert(info_range), elem)
}) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
@@ -264,7 +264,7 @@
{
val msgs =
snapshot.cumulate_markup[SortedMap[Long, XML.Tree]](range, SortedMap.empty,
- Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)),
+ Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
{
case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
if name == Markup.WRITELN ||
@@ -308,7 +308,7 @@
val tips =
snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
- range, Text.Info(range, Nil), Some(tooltip_elements),
+ range, Text.Info(range, Nil), Some(tooltip_elements), _ =>
{
case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
val kind1 = space_explode('_', kind).mkString(" ")
@@ -335,7 +335,7 @@
def gutter_message(range: Text.Range): Option[Icon] =
{
val results =
- snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)),
+ snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)), _ =>
{
case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
body match {
@@ -360,7 +360,7 @@
{
val results =
snapshot.cumulate_markup[Int](range, 0,
- Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)),
+ Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)), _ =>
{
case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
if name == Markup.WRITELN ||
@@ -386,7 +386,7 @@
def line_background(range: Text.Range): Option[(Color, Boolean)] =
{
val results =
- snapshot.cumulate_markup[Int](range, 0, Some(messages_include),
+ snapshot.cumulate_markup[Int](range, 0, Some(messages_include), _ =>
{
case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
if name == Markup.WRITELN_MESSAGE ||
@@ -397,7 +397,7 @@
val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
val is_separator = pri > 0 &&
- snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)),
+ snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)), _ =>
{
case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => true
}).exists(_.info)
@@ -406,10 +406,16 @@
}
+ def output_messages(st: Command.State): List[XML.Tree] =
+ {
+ st.results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
+ }
+
+
private val background1_include =
Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
- Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
- Markup.DIALOG_RESULT ++ active_include
+ Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
+ active_include
def background1(range: Text.Range): Stream[Text.Info[Color]] =
{
@@ -417,49 +423,47 @@
else
for {
Text.Info(r, result) <-
- snapshot.cumulate_markup[(Map[String, String], Option[Protocol.Status], Option[Color])](
- range, (Map.empty, Some(Protocol.Status.init), None), Some(background1_include),
+ snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
+ range, (Some(Protocol.Status.init), None), Some(background1_include), command_state =>
{
- case (((dialogs, Some(status), color), Text.Info(_, XML.Elem(markup, _))))
+ case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
if (Protocol.command_status_markup(markup.name)) =>
- (dialogs, Some(Protocol.command_status(status, markup)), color)
- case ((dialogs, _, _), Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
- (dialogs, None, Some(bad_color))
- case ((dialogs, _, _), Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
- (dialogs, None, Some(intensify_color))
- case ((dialogs, status, color), Text.Info(_,
- XML.Elem(Markup(Markup.DIALOG_RESULT, Markup.Dialog_Args(name, result)), _))) =>
- (dialogs + (name -> result), status, color)
- case ((dialogs, _, _), Text.Info(_,
- XML.Elem(Markup(Markup.DIALOG, Markup.Dialog_Args(name, result)), _))) =>
- if (dialogs.get(name) == Some(result))
- (dialogs, None, Some(active_result_color))
- else (dialogs, None, Some(active_color))
- case ((dialogs, _, _), Text.Info(_, XML.Elem(Markup(name, _), _)))
- if active_include(name) =>
- (dialogs, None, Some(active_color))
+ (Some(Protocol.command_status(status, markup)), color)
+ case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
+ (None, Some(bad_color))
+ case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
+ (None, Some(intensify_color))
+ case (_, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
+ command_state.results.get(serial) match {
+ case Some(Protocol.Dialog_Result(_, res)) if res == result =>
+ (None, Some(active_result_color))
+ case _ =>
+ (None, Some(active_color))
+ }
+ case (_, Text.Info(_, XML.Elem(markup, _))) if active_include(markup.name) =>
+ (None, Some(active_color))
})
color <-
(result match {
- case (_, Some(status), opt_color) =>
+ case (Some(status), opt_color) =>
if (status.is_unprocessed) Some(unprocessed1_color)
else if (status.is_running) Some(running1_color)
else opt_color
- case (_, _, opt_color) => opt_color
+ case (_, opt_color) => opt_color
})
} yield Text.Info(r, color)
}
def background2(range: Text.Range): Stream[Text.Info[Color]] =
- snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)),
+ snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)), _ =>
{
case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
})
def foreground(range: Text.Range): Stream[Text.Info[Color]] =
- snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)),
+ snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)), _ =>
{
case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
@@ -499,7 +503,7 @@
{
if (color == Token_Markup.hidden_color) Stream(Text.Info(range, color))
else
- snapshot.cumulate_markup(range, color, Some(text_color_elements),
+ snapshot.cumulate_markup(range, color, Some(text_color_elements), _ =>
{
case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
if text_colors.isDefinedAt(m) => text_colors(m)