rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
--- a/src/Pure/PIDE/command.scala Wed Dec 12 21:50:42 2012 +0100
+++ b/src/Pure/PIDE/command.scala Wed Dec 12 23:36:07 2012 +0100
@@ -38,7 +38,8 @@
(this /: msgs)((state, msg) =>
msg match {
case elem @ XML.Elem(markup, Nil) =>
- state.add_status(markup).add_markup(Text.Info(command.proper_range, elem))
+ state.add_status(markup)
+ .add_markup(Text.Info(command.proper_range, elem)) // FIXME cumulation order!?
case _ => System.err.println("Ignored status message: " + msg); state
})
--- a/src/Pure/PIDE/markup.ML Wed Dec 12 21:50:42 2012 +0100
+++ b/src/Pure/PIDE/markup.ML Wed Dec 12 23:36:07 2012 +0100
@@ -96,11 +96,11 @@
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 sendbackN: string
val dialogN: string val dialog: string -> string -> T
- val graphviewN: string
val intensifyN: string val intensify: T
val taskN: string
val acceptedN: string val accepted: T
@@ -341,16 +341,15 @@
(* 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 graphviewN = "graphview";
-
-val paddingN = "padding";
-val padding_line = (paddingN, lineN);
-
val (intensifyN, intensify) = markup_elem "intensify";
--- a/src/Pure/PIDE/markup.scala Wed Dec 12 21:50:42 2012 +0100
+++ b/src/Pure/PIDE/markup.scala Wed Dec 12 23:36:07 2012 +0100
@@ -215,16 +215,24 @@
/* 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")
- val GRAPHVIEW = "graphview"
-
- val PADDING = "padding"
- val PADDING_LINE = (PADDING, LINE)
+ 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"
--- a/src/Pure/System/session.scala Wed Dec 12 21:50:42 2012 +0100
+++ b/src/Pure/System/session.scala Wed Dec 12 23:36:07 2012 +0100
@@ -426,7 +426,7 @@
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.REPORT, Position.Id(id)), List(dialog_result))))
+ XML.Elem(Markup(Markup.STATUS, Position.Id(id)), List(dialog_result))))
case Messages(msgs) =>
msgs foreach {
--- a/src/Tools/jEdit/etc/options Wed Dec 12 21:50:42 2012 +0100
+++ b/src/Tools/jEdit/etc/options Wed Dec 12 23:36:07 2012 +0100
@@ -43,7 +43,7 @@
option hyperlink_color : string = "000000FF"
option active_color : string = "DCDCDCFF"
option active_hover_color : string = "9DC75DFF"
-option active_result_color : string = "666633FF"
+option active_result_color : string = "999966FF"
option keyword1_color : string = "006699FF"
option keyword2_color : string = "009966FF"
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Dec 12 21:50:42 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Wed Dec 12 23:36:07 2012 +0100
@@ -70,8 +70,14 @@
}
val new_output =
- if (!restriction.isDefined || restriction.get.contains(new_state.command))
- new_state.results.iterator.map(_._2).toList
+ 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)) })
+ }
else current_output
if (new_output != current_output)
--- a/src/Tools/jEdit/src/rendering.scala Wed Dec 12 21:50:42 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Wed Dec 12 23:36:07 2012 +0100
@@ -250,8 +250,7 @@
}
- private val active_include =
- Set(Markup.SENDBACK, Markup.DIALOG, Markup.DIALOG_RESULT, Markup.GRAPHVIEW)
+ private val active_include = Set(Markup.SENDBACK, Markup.DIALOG, Markup.GRAPHVIEW)
def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
snapshot.select_markup(range, Some(active_include),
@@ -409,8 +408,8 @@
private val background1_include =
Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
- Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
- active_include
+ Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
+ Markup.DIALOG_RESULT ++ active_include
def background1(range: Text.Range): Stream[Text.Info[Color]] =
{
@@ -418,28 +417,35 @@
else
for {
Text.Info(r, result) <-
- snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
- range, (Some(Protocol.Status.init), None), Some(background1_include),
+ snapshot.cumulate_markup[(Map[String, String], Option[Protocol.Status], Option[Color])](
+ range, (Map.empty, Some(Protocol.Status.init), None), Some(background1_include),
{
- case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
+ case (((dialogs, Some(status), color), Text.Info(_, XML.Elem(markup, _))))
if (Protocol.command_status_markup(markup.name)) =>
- (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(_, XML.Elem(Markup(Markup.DIALOG_RESULT, _), _))) =>
- (None, Some(active_result_color))
- case (_, Text.Info(_, XML.Elem(Markup(name, _), _))) if active_include(name) =>
- (None, Some(active_color))
+ (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))
})
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)
}