# HG changeset patch
# User wenzelm
# Date 1314458774 -7200
# Node ID 5e5e6ad3922c687da5832f9efa3fecf52a00efe2
# Parent  51f167047edfd9fb1d14a40a47878f769c06c81c
explicit markup for legacy warnings;

diff -r 51f167047edf -r 5e5e6ad3922c src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Aug 27 16:22:59 2011 +0200
+++ b/src/Pure/General/markup.ML	Sat Aug 27 17:26:14 2011 +0200
@@ -110,6 +110,7 @@
   val versionN: string
   val assignN: string val assign: int -> T
   val serialN: string
+  val legacyN: string val legacy: T
   val promptN: string val prompt: T
   val readyN: string val ready: T
   val reportN: string val report: T
@@ -358,6 +359,7 @@
 
 val serialN = "serial";
 
+val (legacyN, legacy) = markup_elem "legacy";
 val (promptN, prompt) = markup_elem "prompt";
 val (readyN, ready) = markup_elem "ready";
 
diff -r 51f167047edf -r 5e5e6ad3922c src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sat Aug 27 16:22:59 2011 +0200
+++ b/src/Pure/General/markup.scala	Sat Aug 27 17:26:14 2011 +0200
@@ -259,6 +259,8 @@
   val STDOUT = "stdout"
   val EXIT = "exit"
 
+  val LEGACY = "legacy"
+
   val NO_REPORT = "no_report"
 
   val BAD = "bad"
diff -r 51f167047edf -r 5e5e6ad3922c src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Sat Aug 27 16:22:59 2011 +0200
+++ b/src/Pure/General/output.ML	Sat Aug 27 17:26:14 2011 +0200
@@ -9,7 +9,6 @@
   val writeln: string -> unit
   val tracing: string -> unit
   val warning: string -> unit
-  val legacy_feature: string -> unit
 end;
 
 signature OUTPUT =
@@ -113,8 +112,6 @@
 fun report s = ! Private_Hooks.report_fn (output s);
 fun raw_message props s = ! Private_Hooks.raw_message_fn props (output s);
 
-fun legacy_feature s = warning ("Legacy feature! " ^ s);
-
 end;
 
 structure Basic_Output: BASIC_OUTPUT = Output;
diff -r 51f167047edf -r 5e5e6ad3922c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Aug 27 16:22:59 2011 +0200
+++ b/src/Pure/ROOT.ML	Sat Aug 27 17:26:14 2011 +0200
@@ -31,6 +31,7 @@
 use "General/output.ML";
 use "General/timing.ML";
 use "General/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 51f167047edf -r 5e5e6ad3922c src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Aug 27 16:22:59 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Aug 27 17:26:14 2011 +0200
@@ -44,7 +44,8 @@
     def >= (that: Icon): Boolean = this.priority >= that.priority
   }
   val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-information.png"))
-  val error_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-error.png"))
+  val legacy_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-warning.png"))
+  val error_icon = new Icon(3, Isabelle.load_icon("16x16/status/dialog-error.png"))
 
 
   /* command status */
@@ -96,7 +97,11 @@
 
   val gutter_message: Markup_Tree.Select[Icon] =
   {
-    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
+    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
+      body match {
+        case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
+        case _ => warning_icon
+      }
     case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
   }