# HG changeset patch # User wenzelm # Date 1419979503 -3600 # Node ID 5f0bd5afc16d95c5c5532b7400329989221a801c # Parent 711c2446dc9dafa607d61bfc49e170cd59574022 explicit message channel for "legacy", which is nonetheless a variant of "warning"; diff -r 711c2446dc9d -r 5f0bd5afc16d src/Pure/General/output.ML --- a/src/Pure/General/output.ML Tue Dec 30 14:11:06 2014 +0100 +++ b/src/Pure/General/output.ML Tue Dec 30 23:45:03 2014 +0100 @@ -9,6 +9,7 @@ val writeln: string -> unit val tracing: string -> unit val warning: string -> unit + val legacy_feature: string -> unit end; signature OUTPUT = @@ -46,6 +47,7 @@ val information_fn: (output list -> unit) Unsynchronized.ref val tracing_fn: (output list -> unit) Unsynchronized.ref val warning_fn: (output list -> unit) Unsynchronized.ref + val legacy_fn: (output list -> unit) Unsynchronized.ref val error_message_fn: (serial * output list -> unit) Unsynchronized.ref val system_message_fn: (output list -> unit) Unsynchronized.ref val status_fn: (output list -> unit) Unsynchronized.ref @@ -102,6 +104,8 @@ val information_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss); val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss); val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode); +val legacy_fn = Unsynchronized.ref (fn ss => ! warning_fn ss); + val error_message_fn = Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss))); val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss); @@ -117,6 +121,7 @@ fun information s = ! information_fn [output s]; fun tracing s = ! tracing_fn [output s]; fun warning s = ! warning_fn [output s]; +fun legacy_feature s = ! legacy_fn [output ("Legacy feature! " ^ s)]; fun error_message' (i, s) = ! error_message_fn (i, [output s]); fun error_message s = error_message' (serial (), s); fun system_message s = ! system_message_fn [output s]; diff -r 711c2446dc9d -r 5f0bd5afc16d src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Dec 30 14:11:06 2014 +0100 +++ b/src/Pure/PIDE/command.scala Tue Dec 30 23:45:03 2014 +0100 @@ -128,7 +128,7 @@ lazy val protocol_status: Protocol.Status = { val warnings = - if (results.iterator.exists(p => Protocol.is_warning(p._2))) + if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2))) List(Markup(Markup.WARNING, Nil)) else Nil val errors = diff -r 711c2446dc9d -r 5f0bd5afc16d src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Tue Dec 30 14:11:06 2014 +0100 +++ b/src/Pure/PIDE/markup.ML Tue Dec 30 23:45:03 2014 +0100 @@ -160,10 +160,10 @@ val informationN: string val tracingN: string val warningN: string + val legacyN: string val errorN: string val systemN: string val protocolN: string - val legacyN: string val legacy: T val reportN: string val report: T val no_reportN: string val no_report: T val badN: string val bad: T @@ -547,12 +547,11 @@ val informationN = "information"; val tracingN = "tracing"; val warningN = "warning"; +val legacyN = "legacy"; val errorN = "error"; val systemN = "system"; val protocolN = "protocol"; -val (legacyN, legacy) = markup_elem "legacy"; - val (reportN, report) = markup_elem "report"; val (no_reportN, no_report) = markup_elem "no_report"; diff -r 711c2446dc9d -r 5f0bd5afc16d src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue Dec 30 14:11:06 2014 +0100 +++ b/src/Pure/PIDE/markup.scala Tue Dec 30 23:45:03 2014 +0100 @@ -353,6 +353,7 @@ val INFORMATION = "information" val TRACING = "tracing" val WARNING = "warning" + val LEGACY = "legacy" val ERROR = "error" val PROTOCOL = "protocol" val SYSTEM = "system" @@ -365,6 +366,7 @@ val INFORMATION_MESSAGE = "information_message" val TRACING_MESSAGE = "tracing_message" val WARNING_MESSAGE = "warning_message" + val LEGACY_MESSAGE = "legacy_message" val ERROR_MESSAGE = "error_message" val messages = Map( @@ -373,14 +375,13 @@ INFORMATION -> INFORMATION_MESSAGE, TRACING -> TRACING_MESSAGE, WARNING -> WARNING_MESSAGE, + LEGACY -> LEGACY_MESSAGE, ERROR -> ERROR_MESSAGE) val message: String => String = messages.withDefault((s: String) => s) val Return_Code = new Properties.Int("return_code") - val LEGACY = "legacy" - val NO_REPORT = "no_report" val BAD = "bad" diff -r 711c2446dc9d -r 5f0bd5afc16d src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Tue Dec 30 14:11:06 2014 +0100 +++ b/src/Pure/PIDE/protocol.scala Tue Dec 30 23:45:03 2014 +0100 @@ -58,7 +58,7 @@ case Markup.JOINED => forks -= 1 case Markup.RUNNING => touched = true; runs += 1 case Markup.FINISHED => runs -= 1 - case Markup.WARNING => warned = true + case Markup.WARNING | Markup.LEGACY => warned = true case Markup.FAILED | Markup.ERROR => failed = true case _ => } @@ -105,7 +105,7 @@ Markup.FINISHED, Markup.FAILED) val liberal_status_elements = - proper_status_elements + Markup.WARNING + Markup.ERROR + proper_status_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR /* command timing */ @@ -241,15 +241,6 @@ case _ => false } - def is_warning_markup(msg: XML.Tree, name: String): Boolean = - msg match { - case XML.Elem(Markup(Markup.WARNING, _), - List(XML.Elem(markup, _))) => markup.name == name - case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), - List(XML.Elem(markup, _))) => markup.name == name - case _ => false - } - def is_warning(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.WARNING, _), _) => true @@ -257,6 +248,13 @@ case _ => false } + def is_legacy(msg: XML.Tree): Boolean = + msg match { + case XML.Elem(Markup(Markup.LEGACY, _), _) => true + case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true + case _ => false + } + def is_error(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.ERROR, _), _) => true @@ -264,8 +262,6 @@ case _ => false } - def is_legacy(msg: XML.Tree): Boolean = is_warning_markup(msg, Markup.LEGACY) - def is_inlined(msg: XML.Tree): Boolean = !(is_result(msg) || is_tracing(msg) || is_state(msg)) diff -r 711c2446dc9d -r 5f0bd5afc16d src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Dec 30 14:11:06 2014 +0100 +++ b/src/Pure/ROOT.ML Tue Dec 30 23:45:03 2014 +0100 @@ -27,7 +27,6 @@ use "General/properties.ML"; use "General/output.ML"; use "PIDE/markup.ML"; -fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s)); use "General/scan.ML"; use "General/source.ML"; use "General/symbol.ML"; diff -r 711c2446dc9d -r 5f0bd5afc16d src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Tue Dec 30 14:11:06 2014 +0100 +++ b/src/Pure/System/isabelle_process.ML Tue Dec 30 23:45:03 2014 +0100 @@ -123,6 +123,7 @@ Output.tracing_fn := (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)); Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s); + Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s); Output.error_message_fn := (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s); Output.system_message_fn := message Markup.systemN []; diff -r 711c2446dc9d -r 5f0bd5afc16d src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Tue Dec 30 14:11:06 2014 +0100 +++ b/src/Tools/jEdit/etc/options Tue Dec 30 23:45:03 2014 +0100 @@ -88,12 +88,14 @@ option writeln_color : string = "C0C0C0FF" option information_color : string = "C1DFEEFF" option warning_color : string = "FF8C00FF" +option legacy_color : string = "FF8C00FF" option error_color : string = "B22222FF" option writeln_message_color : string = "F0F0F0FF" option state_message_color : string = "F0E4E4FF" option information_message_color : string = "DCEAF3FF" option tracing_message_color : string = "F0F8FFFF" option warning_message_color : string = "EEE8AAFF" +option legacy_message_color : string = "EEE8AAFF" option error_message_color : string = "FFC1C1FF" option spell_checker_color : string = "0000FFFF" option bad_color : string = "FF6A6A64" diff -r 711c2446dc9d -r 5f0bd5afc16d src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Tue Dec 30 14:11:06 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Tue Dec 30 23:45:03 2014 +0100 @@ -46,6 +46,8 @@ Markup.TRACING_MESSAGE -> tracing_pri, Markup.WARNING -> warning_pri, Markup.WARNING_MESSAGE -> warning_pri, + Markup.LEGACY -> legacy_pri, + Markup.LEGACY_MESSAGE -> legacy_pri, Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri) @@ -161,8 +163,8 @@ Markup.SENDBACK, Markup.SIMP_TRACE_PANEL) private val tooltip_message_elements = - Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, - Markup.ERROR, Markup.BAD) + Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR, + Markup.BAD) private val tooltip_descriptions = Map( @@ -182,14 +184,15 @@ Markup.Elements(tooltip_descriptions.keySet) private val gutter_elements = - Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.ERROR) + Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR) private val squiggly_elements = - Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.ERROR) + Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR) private val line_background_elements = Markup.Elements(Markup.WRITELN_MESSAGE, Markup.STATE_MESSAGE, Markup.INFORMATION_MESSAGE, - Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE) + Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.LEGACY_MESSAGE, + Markup.ERROR_MESSAGE) private val separator_elements = Markup.Elements(Markup.SEPARATOR) @@ -198,8 +201,8 @@ Protocol.proper_status_elements + Markup.WRITELN_MESSAGE + Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE + Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + - Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++ - active_elements + Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE + + Markup.BAD + Markup.INTENSIFY ++ active_elements private val foreground_elements = Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, @@ -232,12 +235,14 @@ val writeln_color = color_value("writeln_color") val information_color = color_value("information_color") val warning_color = color_value("warning_color") + val legacy_color = color_value("legacy_color") val error_color = color_value("error_color") val writeln_message_color = color_value("writeln_message_color") val state_message_color = color_value("state_message_color") val information_message_color = color_value("information_message_color") val tracing_message_color = color_value("tracing_message_color") val warning_message_color = color_value("warning_message_color") + val legacy_message_color = color_value("legacy_message_color") val error_message_color = color_value("error_message_color") val spell_checker_color = color_value("spell_checker_color") val bad_color = color_value("bad_color") @@ -591,6 +596,7 @@ Rendering.writeln_pri -> writeln_color, Rendering.information_pri -> information_color, Rendering.warning_pri -> warning_color, + Rendering.legacy_pri -> legacy_color, Rendering.error_pri -> error_color) def squiggly_underline(range: Text.Range): List[Text.Info[Color]] = @@ -615,6 +621,7 @@ Rendering.information_pri -> information_message_color, Rendering.tracing_pri -> tracing_message_color, Rendering.warning_pri -> warning_message_color, + Rendering.legacy_pri -> legacy_message_color, Rendering.error_pri -> error_message_color) def line_background(range: Text.Range): Option[(Color, Boolean)] =