# HG changeset patch # User wenzelm # Date 1355351767 -3600 # Node ID f496b2b7bafbb97362ea11ac215c58995a25a43f # Parent 6647ba2775c1706eb4fb03c5da3f352a34310f2c rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.; diff -r 6647ba2775c1 -r f496b2b7bafb src/Pure/PIDE/command.scala --- 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 }) diff -r 6647ba2775c1 -r f496b2b7bafb src/Pure/PIDE/markup.ML --- 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"; diff -r 6647ba2775c1 -r f496b2b7bafb src/Pure/PIDE/markup.scala --- 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" diff -r 6647ba2775c1 -r f496b2b7bafb src/Pure/System/session.scala --- 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 { diff -r 6647ba2775c1 -r f496b2b7bafb src/Tools/jEdit/etc/options --- 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" diff -r 6647ba2775c1 -r f496b2b7bafb src/Tools/jEdit/src/output_dockable.scala --- 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) diff -r 6647ba2775c1 -r f496b2b7bafb src/Tools/jEdit/src/rendering.scala --- 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) }