explicit message channel for "legacy", which is nonetheless a variant of "warning";
authorwenzelm
Tue Dec 30 23:45:03 2014 +0100 (2014-12-30 ago)
changeset 592035f0bd5afc16d
parent 59202 711c2446dc9d
child 59204 0cbe0a56d3fa
explicit message channel for "legacy", which is nonetheless a variant of "warning";
src/Pure/General/output.ML
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.scala
src/Pure/ROOT.ML
src/Pure/System/isabelle_process.ML
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/General/output.ML	Tue Dec 30 14:11:06 2014 +0100
     1.2 +++ b/src/Pure/General/output.ML	Tue Dec 30 23:45:03 2014 +0100
     1.3 @@ -9,6 +9,7 @@
     1.4    val writeln: string -> unit
     1.5    val tracing: string -> unit
     1.6    val warning: string -> unit
     1.7 +  val legacy_feature: string -> unit
     1.8  end;
     1.9  
    1.10  signature OUTPUT =
    1.11 @@ -46,6 +47,7 @@
    1.12    val information_fn: (output list -> unit) Unsynchronized.ref
    1.13    val tracing_fn: (output list -> unit) Unsynchronized.ref
    1.14    val warning_fn: (output list -> unit) Unsynchronized.ref
    1.15 +  val legacy_fn: (output list -> unit) Unsynchronized.ref
    1.16    val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
    1.17    val system_message_fn: (output list -> unit) Unsynchronized.ref
    1.18    val status_fn: (output list -> unit) Unsynchronized.ref
    1.19 @@ -102,6 +104,8 @@
    1.20  val information_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.21  val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.22  val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
    1.23 +val legacy_fn = Unsynchronized.ref (fn ss => ! warning_fn ss);
    1.24 +
    1.25  val error_message_fn =
    1.26    Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
    1.27  val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.28 @@ -117,6 +121,7 @@
    1.29  fun information s = ! information_fn [output s];
    1.30  fun tracing s = ! tracing_fn [output s];
    1.31  fun warning s = ! warning_fn [output s];
    1.32 +fun legacy_feature s = ! legacy_fn [output ("Legacy feature! " ^ s)];
    1.33  fun error_message' (i, s) = ! error_message_fn (i, [output s]);
    1.34  fun error_message s = error_message' (serial (), s);
    1.35  fun system_message s = ! system_message_fn [output s];
     2.1 --- a/src/Pure/PIDE/command.scala	Tue Dec 30 14:11:06 2014 +0100
     2.2 +++ b/src/Pure/PIDE/command.scala	Tue Dec 30 23:45:03 2014 +0100
     2.3 @@ -128,7 +128,7 @@
     2.4      lazy val protocol_status: Protocol.Status =
     2.5      {
     2.6        val warnings =
     2.7 -        if (results.iterator.exists(p => Protocol.is_warning(p._2)))
     2.8 +        if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2)))
     2.9            List(Markup(Markup.WARNING, Nil))
    2.10          else Nil
    2.11        val errors =
     3.1 --- a/src/Pure/PIDE/markup.ML	Tue Dec 30 14:11:06 2014 +0100
     3.2 +++ b/src/Pure/PIDE/markup.ML	Tue Dec 30 23:45:03 2014 +0100
     3.3 @@ -160,10 +160,10 @@
     3.4    val informationN: string
     3.5    val tracingN: string
     3.6    val warningN: string
     3.7 +  val legacyN: string
     3.8    val errorN: string
     3.9    val systemN: string
    3.10    val protocolN: string
    3.11 -  val legacyN: string val legacy: T
    3.12    val reportN: string val report: T
    3.13    val no_reportN: string val no_report: T
    3.14    val badN: string val bad: T
    3.15 @@ -547,12 +547,11 @@
    3.16  val informationN = "information";
    3.17  val tracingN = "tracing";
    3.18  val warningN = "warning";
    3.19 +val legacyN = "legacy";
    3.20  val errorN = "error";
    3.21  val systemN = "system";
    3.22  val protocolN = "protocol";
    3.23  
    3.24 -val (legacyN, legacy) = markup_elem "legacy";
    3.25 -
    3.26  val (reportN, report) = markup_elem "report";
    3.27  val (no_reportN, no_report) = markup_elem "no_report";
    3.28  
     4.1 --- a/src/Pure/PIDE/markup.scala	Tue Dec 30 14:11:06 2014 +0100
     4.2 +++ b/src/Pure/PIDE/markup.scala	Tue Dec 30 23:45:03 2014 +0100
     4.3 @@ -353,6 +353,7 @@
     4.4    val INFORMATION = "information"
     4.5    val TRACING = "tracing"
     4.6    val WARNING = "warning"
     4.7 +  val LEGACY = "legacy"
     4.8    val ERROR = "error"
     4.9    val PROTOCOL = "protocol"
    4.10    val SYSTEM = "system"
    4.11 @@ -365,6 +366,7 @@
    4.12    val INFORMATION_MESSAGE = "information_message"
    4.13    val TRACING_MESSAGE = "tracing_message"
    4.14    val WARNING_MESSAGE = "warning_message"
    4.15 +  val LEGACY_MESSAGE = "legacy_message"
    4.16    val ERROR_MESSAGE = "error_message"
    4.17  
    4.18    val messages = Map(
    4.19 @@ -373,14 +375,13 @@
    4.20      INFORMATION -> INFORMATION_MESSAGE,
    4.21      TRACING -> TRACING_MESSAGE,
    4.22      WARNING -> WARNING_MESSAGE,
    4.23 +    LEGACY -> LEGACY_MESSAGE,
    4.24      ERROR -> ERROR_MESSAGE)
    4.25  
    4.26    val message: String => String = messages.withDefault((s: String) => s)
    4.27  
    4.28    val Return_Code = new Properties.Int("return_code")
    4.29  
    4.30 -  val LEGACY = "legacy"
    4.31 -
    4.32    val NO_REPORT = "no_report"
    4.33  
    4.34    val BAD = "bad"
     5.1 --- a/src/Pure/PIDE/protocol.scala	Tue Dec 30 14:11:06 2014 +0100
     5.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Dec 30 23:45:03 2014 +0100
     5.3 @@ -58,7 +58,7 @@
     5.4            case Markup.JOINED => forks -= 1
     5.5            case Markup.RUNNING => touched = true; runs += 1
     5.6            case Markup.FINISHED => runs -= 1
     5.7 -          case Markup.WARNING => warned = true
     5.8 +          case Markup.WARNING | Markup.LEGACY => warned = true
     5.9            case Markup.FAILED | Markup.ERROR => failed = true
    5.10            case _ =>
    5.11          }
    5.12 @@ -105,7 +105,7 @@
    5.13        Markup.FINISHED, Markup.FAILED)
    5.14  
    5.15    val liberal_status_elements =
    5.16 -    proper_status_elements + Markup.WARNING + Markup.ERROR
    5.17 +    proper_status_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
    5.18  
    5.19  
    5.20    /* command timing */
    5.21 @@ -241,15 +241,6 @@
    5.22        case _ => false
    5.23      }
    5.24  
    5.25 -  def is_warning_markup(msg: XML.Tree, name: String): Boolean =
    5.26 -    msg match {
    5.27 -      case XML.Elem(Markup(Markup.WARNING, _),
    5.28 -        List(XML.Elem(markup, _))) => markup.name == name
    5.29 -      case XML.Elem(Markup(Markup.WARNING_MESSAGE, _),
    5.30 -        List(XML.Elem(markup, _))) => markup.name == name
    5.31 -      case _ => false
    5.32 -    }
    5.33 -
    5.34    def is_warning(msg: XML.Tree): Boolean =
    5.35      msg match {
    5.36        case XML.Elem(Markup(Markup.WARNING, _), _) => true
    5.37 @@ -257,6 +248,13 @@
    5.38        case _ => false
    5.39      }
    5.40  
    5.41 +  def is_legacy(msg: XML.Tree): Boolean =
    5.42 +    msg match {
    5.43 +      case XML.Elem(Markup(Markup.LEGACY, _), _) => true
    5.44 +      case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true
    5.45 +      case _ => false
    5.46 +    }
    5.47 +
    5.48    def is_error(msg: XML.Tree): Boolean =
    5.49      msg match {
    5.50        case XML.Elem(Markup(Markup.ERROR, _), _) => true
    5.51 @@ -264,8 +262,6 @@
    5.52        case _ => false
    5.53      }
    5.54  
    5.55 -  def is_legacy(msg: XML.Tree): Boolean = is_warning_markup(msg, Markup.LEGACY)
    5.56 -
    5.57    def is_inlined(msg: XML.Tree): Boolean =
    5.58      !(is_result(msg) || is_tracing(msg) || is_state(msg))
    5.59  
     6.1 --- a/src/Pure/ROOT.ML	Tue Dec 30 14:11:06 2014 +0100
     6.2 +++ b/src/Pure/ROOT.ML	Tue Dec 30 23:45:03 2014 +0100
     6.3 @@ -27,7 +27,6 @@
     6.4  use "General/properties.ML";
     6.5  use "General/output.ML";
     6.6  use "PIDE/markup.ML";
     6.7 -fun legacy_feature s = warning (Markup.markup Markup.legacy ("Legacy feature! " ^ s));
     6.8  use "General/scan.ML";
     6.9  use "General/source.ML";
    6.10  use "General/symbol.ML";
     7.1 --- a/src/Pure/System/isabelle_process.ML	Tue Dec 30 14:11:06 2014 +0100
     7.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Dec 30 23:45:03 2014 +0100
     7.3 @@ -123,6 +123,7 @@
     7.4      Output.tracing_fn :=
     7.5        (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
     7.6      Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
     7.7 +    Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s);
     7.8      Output.error_message_fn :=
     7.9        (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
    7.10      Output.system_message_fn := message Markup.systemN [];
     8.1 --- a/src/Tools/jEdit/etc/options	Tue Dec 30 14:11:06 2014 +0100
     8.2 +++ b/src/Tools/jEdit/etc/options	Tue Dec 30 23:45:03 2014 +0100
     8.3 @@ -88,12 +88,14 @@
     8.4  option writeln_color : string = "C0C0C0FF"
     8.5  option information_color : string = "C1DFEEFF"
     8.6  option warning_color : string = "FF8C00FF"
     8.7 +option legacy_color : string = "FF8C00FF"
     8.8  option error_color : string = "B22222FF"
     8.9  option writeln_message_color : string = "F0F0F0FF"
    8.10  option state_message_color : string = "F0E4E4FF"
    8.11  option information_message_color : string = "DCEAF3FF"
    8.12  option tracing_message_color : string = "F0F8FFFF"
    8.13  option warning_message_color : string = "EEE8AAFF"
    8.14 +option legacy_message_color : string = "EEE8AAFF"
    8.15  option error_message_color : string = "FFC1C1FF"
    8.16  option spell_checker_color : string = "0000FFFF"
    8.17  option bad_color : string = "FF6A6A64"
     9.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Dec 30 14:11:06 2014 +0100
     9.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Dec 30 23:45:03 2014 +0100
     9.3 @@ -46,6 +46,8 @@
     9.4      Markup.TRACING_MESSAGE -> tracing_pri,
     9.5      Markup.WARNING -> warning_pri,
     9.6      Markup.WARNING_MESSAGE -> warning_pri,
     9.7 +    Markup.LEGACY -> legacy_pri,
     9.8 +    Markup.LEGACY_MESSAGE -> legacy_pri,
     9.9      Markup.ERROR -> error_pri,
    9.10      Markup.ERROR_MESSAGE -> error_pri)
    9.11  
    9.12 @@ -161,8 +163,8 @@
    9.13        Markup.SENDBACK, Markup.SIMP_TRACE_PANEL)
    9.14  
    9.15    private val tooltip_message_elements =
    9.16 -    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING,
    9.17 -      Markup.ERROR, Markup.BAD)
    9.18 +    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
    9.19 +      Markup.BAD)
    9.20  
    9.21    private val tooltip_descriptions =
    9.22      Map(
    9.23 @@ -182,14 +184,15 @@
    9.24      Markup.Elements(tooltip_descriptions.keySet)
    9.25  
    9.26    private val gutter_elements =
    9.27 -    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.ERROR)
    9.28 +    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
    9.29  
    9.30    private val squiggly_elements =
    9.31 -    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.ERROR)
    9.32 +    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
    9.33  
    9.34    private val line_background_elements =
    9.35      Markup.Elements(Markup.WRITELN_MESSAGE, Markup.STATE_MESSAGE, Markup.INFORMATION_MESSAGE,
    9.36 -      Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE)
    9.37 +      Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.LEGACY_MESSAGE,
    9.38 +      Markup.ERROR_MESSAGE)
    9.39  
    9.40    private val separator_elements =
    9.41      Markup.Elements(Markup.SEPARATOR)
    9.42 @@ -198,8 +201,8 @@
    9.43      Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
    9.44        Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
    9.45        Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
    9.46 -      Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
    9.47 -      active_elements
    9.48 +      Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
    9.49 +      Markup.BAD + Markup.INTENSIFY ++ active_elements
    9.50  
    9.51    private val foreground_elements =
    9.52      Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
    9.53 @@ -232,12 +235,14 @@
    9.54    val writeln_color = color_value("writeln_color")
    9.55    val information_color = color_value("information_color")
    9.56    val warning_color = color_value("warning_color")
    9.57 +  val legacy_color = color_value("legacy_color")
    9.58    val error_color = color_value("error_color")
    9.59    val writeln_message_color = color_value("writeln_message_color")
    9.60    val state_message_color = color_value("state_message_color")
    9.61    val information_message_color = color_value("information_message_color")
    9.62    val tracing_message_color = color_value("tracing_message_color")
    9.63    val warning_message_color = color_value("warning_message_color")
    9.64 +  val legacy_message_color = color_value("legacy_message_color")
    9.65    val error_message_color = color_value("error_message_color")
    9.66    val spell_checker_color = color_value("spell_checker_color")
    9.67    val bad_color = color_value("bad_color")
    9.68 @@ -591,6 +596,7 @@
    9.69      Rendering.writeln_pri -> writeln_color,
    9.70      Rendering.information_pri -> information_color,
    9.71      Rendering.warning_pri -> warning_color,
    9.72 +    Rendering.legacy_pri -> legacy_color,
    9.73      Rendering.error_pri -> error_color)
    9.74  
    9.75    def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
    9.76 @@ -615,6 +621,7 @@
    9.77      Rendering.information_pri -> information_message_color,
    9.78      Rendering.tracing_pri -> tracing_message_color,
    9.79      Rendering.warning_pri -> warning_message_color,
    9.80 +    Rendering.legacy_pri -> legacy_message_color,
    9.81      Rendering.error_pri -> error_message_color)
    9.82  
    9.83    def line_background(range: Text.Range): Option[(Color, Boolean)] =