# HG changeset patch # User wenzelm # Date 1347981640 -7200 # Node ID c451856129cd98d1493dc3d8b871baebf66b86fd # Parent c5a8592fb5d3bd28cbf19f46cffabbfd30c519c3 more explicit message markup and rendering; diff -r c5a8592fb5d3 -r c451856129cd src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Sep 18 15:55:29 2012 +0200 +++ b/src/Pure/PIDE/command.scala Tue Sep 18 17:20:40 2012 +0200 @@ -60,10 +60,13 @@ case XML.Elem(Markup(name, atts), body) => atts match { case Isabelle_Markup.Serial(i) => - val result = XML.Elem(Markup(name, Position.purge(atts)), body) - val st0 = copy(results = results + (i -> result)) + val props = Position.purge(atts) + val result = XML.Elem(Markup(name, props), body) + val result_message = XML.Elem(Markup(Isabelle_Markup.message(name), props), body) + + val st0 = copy(results = results + (i -> result_message)) val st1 = - if (Protocol.is_tracing(message)) st0 + if (Protocol.is_tracing(result)) st0 else (st0 /: Protocol.message_positions(command, message))( (st, range) => st.add_markup(Text.Info(range, result))) diff -r c5a8592fb5d3 -r c451856129cd src/Pure/PIDE/isabelle_markup.scala --- a/src/Pure/PIDE/isabelle_markup.scala Tue Sep 18 15:55:29 2012 +0200 +++ b/src/Pure/PIDE/isabelle_markup.scala Tue Sep 18 17:20:40 2012 +0200 @@ -231,6 +231,16 @@ val STDERR = "stderr" val EXIT = "exit" + val WRITELN_MESSAGE = "writeln_message" + val TRACING_MESSAGE = "tracing_message" + val WARNING_MESSAGE = "warning_message" + val ERROR_MESSAGE = "error_message" + + val message: String => String = + Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE, + WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE) + .withDefault((name: String) => name + "_message") + val Return_Code = new Properties.Int("return_code") val LEGACY = "legacy" diff -r c5a8592fb5d3 -r c451856129cd src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Tue Sep 18 15:55:29 2012 +0200 +++ b/src/Pure/PIDE/protocol.scala Tue Sep 18 17:20:40 2012 +0200 @@ -135,18 +135,21 @@ def is_tracing(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true + case XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _) => true case _ => false } def is_warning(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true + case XML.Elem(Markup(Isabelle_Markup.WARNING_MESSAGE, _), _) => true case _ => false } def is_error(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true + case XML.Elem(Markup(Isabelle_Markup.ERROR_MESSAGE, _), _) => true case _ => false } @@ -154,6 +157,8 @@ msg match { case XML.Elem(Markup(Isabelle_Markup.WRITELN, _), List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true + case XML.Elem(Markup(Isabelle_Markup.WRITELN_MESSAGE, _), + List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true case _ => false } diff -r c5a8592fb5d3 -r c451856129cd src/Tools/jEdit/etc/isabelle-jedit.css --- a/src/Tools/jEdit/etc/isabelle-jedit.css Tue Sep 18 15:55:29 2012 +0200 +++ b/src/Tools/jEdit/etc/isabelle-jedit.css Tue Sep 18 17:20:40 2012 +0200 @@ -2,10 +2,10 @@ .message { margin-top: 0.3ex; background-color: #F0F0F0; } -.writeln { } -.tracing { background-color: #F0F8FF; } -.warning { background-color: #EEE8AA; } -.error { background-color: #FFC1C1; } +.writeln_message { } +.tracing_message { background-color: #F0F8FF; } +.warning_message { background-color: #EEE8AA; } +.error_message { background-color: #FFC1C1; } .report { display: none; } diff -r c5a8592fb5d3 -r c451856129cd src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Tue Sep 18 15:55:29 2012 +0200 +++ b/src/Tools/jEdit/etc/options Tue Sep 18 17:20:40 2012 +0200 @@ -31,6 +31,10 @@ option warning_color : string = "FF8C00FF" option error_color : string = "B22222FF" option error1_color : string = "B2222232" +option writeln_message_color : string = "F0F0F0FF" +option tracing_message_color : string = "F0F8FFFF" +option warning_message_color : string = "EEE8AAFF" +option error_message_color : string = "FFC1C1FF" option bad_color : string = "FF6A6A64" option intensify_color : string = "FFCC6664" option quoted_color : string = "8B8B8B19" diff -r c5a8592fb5d3 -r c451856129cd src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Tue Sep 18 15:55:29 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Tue Sep 18 17:20:40 2012 +0200 @@ -109,6 +109,10 @@ val warning_color = color_value("warning_color") val error_color = color_value("error_color") val error1_color = color_value("error1_color") + val writeln_message_color = color_value("writeln_message_color") + val tracing_message_color = color_value("tracing_message_color") + val warning_message_color = color_value("warning_message_color") + val error_message_color = color_value("error_message_color") val bad_color = color_value("bad_color") val intensify_color = color_value("intensify_color") val quoted_color = color_value("quoted_color") @@ -359,11 +363,21 @@ Text.Info(r, result) <- snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])]( range, (Some(Protocol.Status.init), None), - Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY), + Some(Protocol.command_status_markup + Isabelle_Markup.WRITELN_MESSAGE + + Isabelle_Markup.TRACING_MESSAGE + Isabelle_Markup.WARNING_MESSAGE + + Isabelle_Markup.ERROR_MESSAGE + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY), { case (((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(Isabelle_Markup.WRITELN_MESSAGE, _), _))) => + (None, Some(writeln_message_color)) + case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _))) => + (None, Some(tracing_message_color)) + case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING_MESSAGE, _), _))) => + (None, Some(warning_message_color)) + case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR_MESSAGE, _), _))) => + (None, Some(error_message_color)) case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) => (None, Some(bad_color)) case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.INTENSIFY, _), _))) => diff -r c5a8592fb5d3 -r c451856129cd src/Tools/jEdit/src/output2_dockable.scala --- a/src/Tools/jEdit/src/output2_dockable.scala Tue Sep 18 15:55:29 2012 +0200 +++ b/src/Tools/jEdit/src/output2_dockable.scala Tue Sep 18 17:20:40 2012 +0200 @@ -69,11 +69,8 @@ val new_output = if (!restriction.isDefined || restriction.get.contains(new_state.command)) - new_state.results.iterator.map(_._2).filter( - { // FIXME not scalable - case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing - case _ => true - }).toList + new_state.results.iterator.map(_._2) + .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList // FIXME not scalable else current_output if (new_output != current_output) diff -r c5a8592fb5d3 -r c451856129cd src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Tue Sep 18 15:55:29 2012 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Tue Sep 18 17:20:40 2012 +0200 @@ -100,11 +100,8 @@ val new_body = if (!restriction.isDefined || restriction.get.contains(new_state.command)) - new_state.results.iterator.map(_._2).filter( - { // FIXME not scalable - case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing - case _ => true - }).toList + new_state.results.iterator.map(_._2) + .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList // FIXME not scalable else current_body if (new_body != current_body) html_panel.render(new_body)