# 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)] =