more uniform treatment of "bad" like other messages (with serial number);

--- a/src/Pure/Isar/token.ML	Tue Dec 27 17:33:57 2016 +0100
+++ b/src/Pure/Isar/token.ML	Wed Dec 28 10:39:50 2016 +0100
@@ -275,7 +275,7 @@
   | Verbatim => (Markup.verbatim, "")
   | Cartouche => (Markup.cartouche, "")
   | Comment => (Markup.comment, "")
-  | Error msg => (Markup.bad, msg)
+  | Error msg => (Markup.bad (), msg)
   | _ => (Markup.empty, "");
 
 fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), ""));

--- a/src/Pure/ML/ml_lex.ML	Tue Dec 27 17:33:57 2016 +0100
+++ b/src/Pure/ML/ml_lex.ML	Wed Dec 28 10:39:50 2016 +0100
@@ -147,7 +147,7 @@
   | Char => (Markup.ML_char, "")
   | String => (if SML then Markup.SML_string else Markup.ML_string, "")
   | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
-  | Error msg => (Markup.bad, msg)
+  | Error msg => (Markup.bad (), msg)
   | _ => (Markup.empty, "");
 
 in

--- a/src/Pure/PIDE/command.ML	Tue Dec 27 17:33:57 2016 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Dec 28 10:39:50 2016 +0100
@@ -116,7 +116,7 @@
       Input.source_explode (Token.input_of tok)
       |> map_filter (fn (sym, pos) =>
           if Symbol.is_malformed sym
-          then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
+          then SOME ((pos, Markup.bad ()), "Malformed symbolic character") else NONE);
     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
     val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
   in (is_malformed, reports) end;
@@ -242,7 +242,7 @@
         let
           val _ = status tr Markup.failed;
           val _ = status tr Markup.finished;
-          val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else ();
+          val _ = if null errs then (report tr (Markup.bad ()); Exn.interrupt ()) else ();
         in {failed = true, command = tr, state = st} end
     | SOME st' =>
         let

--- a/src/Pure/PIDE/execution.ML	Tue Dec 27 17:33:57 2016 +0100
+++ b/src/Pure/PIDE/execution.ML	Wed Dec 28 10:39:50 2016 +0100
@@ -116,7 +116,7 @@
                   Exn.Exn exn =>
                    (status task [Markup.failed];
                     status task [Markup.finished];
-                    Output.report [Markup.markup_only Markup.bad];
+                    Output.report [Markup.markup_only (Markup.bad ())];
                     if exec_id = 0 then ()
                     else List.app (Future.error_message pos) (Runtime.exn_messages_ids exn))
                 | Exn.Res _ =>

--- a/src/Pure/PIDE/markup.ML	Tue Dec 27 17:33:57 2016 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Dec 28 10:39:50 2016 +0100
@@ -173,7 +173,7 @@
   val protocolN: string
   val reportN: string val report: T
   val no_reportN: string val no_report: T
-  val badN: string val bad: T
+  val badN: string val bad: unit -> T
   val intensifyN: string val intensify: T
   val browserN: string
   val graphviewN: string
@@ -573,7 +573,8 @@
 val (reportN, report) = markup_elem "report";
 val (no_reportN, no_report) = markup_elem "no_report";
 
-val (badN, bad) = markup_elem "bad";
+val badN = "bad";
+fun bad () = (badN, serial_properties (serial ()));
 
 val (intensifyN, intensify) = markup_elem "intensify";
 

--- a/src/Pure/Pure.thy	Tue Dec 27 17:33:57 2016 +0100
+++ b/src/Pure/Pure.thy	Wed Dec 28 10:39:50 2016 +0100
@@ -991,7 +991,7 @@
 local
 
 fun report_back () =
-  Output.report [Markup.markup Markup.bad "Explicit backtracking"];
+  Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"];
 
 val _ =
   Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"

--- a/src/Pure/Syntax/syntax_ext.ML	Tue Dec 27 17:33:57 2016 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML	Wed Dec 28 10:39:50 2016 +0100
@@ -217,7 +217,7 @@
   (case xsym of
     Delim s =>
       if Position.is_reported pos andalso exists Symbol.is_utf8 (Symbol.explode s) then
-        [((pos, Markup.bad),
+        [((pos, Markup.bad ()),
           "Mixfix delimiter contains raw Unicode -- this is non-portable and unreliable")]
       else []
   | _ => []);

--- a/src/Pure/Syntax/syntax_phases.ML	Tue Dec 27 17:33:57 2016 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Wed Dec 28 10:39:50 2016 +0100
@@ -375,7 +375,7 @@
 
 fun parse_failed ctxt pos msg kind =
   cat_error msg ("Failed to parse " ^ kind ^
-    Markup.markup_report (Context_Position.reported_text ctxt pos Markup.bad ""));
+    Markup.markup_report (Context_Position.reported_text ctxt pos (Markup.bad ()) ""));
 
 fun parse_sort ctxt =
   Syntax.parse_input ctxt Term_XML.Decode.sort Markup.language_sort
@@ -746,7 +746,7 @@
       | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
       | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
       | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
-      | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad, x))
+      | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad (), x))
       | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
       | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
       | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))

--- a/src/Pure/Tools/print_operation.ML	Tue Dec 27 17:33:57 2016 +0100
+++ b/src/Pure/Tools/print_operation.ML	Wed Dec 28 10:39:50 2016 +0100
@@ -49,7 +49,7 @@
     (fn {state, args, writeln_result, ...} =>
       let
         val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
-        fun err s = Pretty.mark_str (Markup.bad, s);
+        fun err s = Pretty.mark_str (Markup.bad (), s);
         fun print name =
           (case AList.lookup (op =) (Synchronized.value print_operations) name of
             SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])

--- a/src/Pure/skip_proof.ML	Tue Dec 27 17:33:57 2016 +0100
+++ b/src/Pure/skip_proof.ML	Wed Dec 28 10:39:50 2016 +0100
@@ -19,7 +19,7 @@
 
 fun report ctxt =
   if Context_Position.is_visible ctxt then
-    Output.report [Markup.markup Markup.bad "Skipped proof"]
+    Output.report [Markup.markup (Markup.bad ()) "Skipped proof"]
   else ();
 
 

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Dec 27 17:33:57 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Wed Dec 28 10:39:50 2016 +0100
@@ -502,13 +502,9 @@
       snapshot.cumulate[List[Text.Info[Command.Results.Entry]]](
         range, Nil, JEdit_Rendering.tooltip_message_elements, _ =>
         {
-          case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
+          case (msgs, Text.Info(info_range,
+            XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
           if body.nonEmpty =>
-            val entry: Command.Results.Entry = (Document_ID.make(), msg)
-            Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
-
-          case (msgs, Text.Info(info_range,
-            XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) =>
             val entry: Command.Results.Entry =
               serial -> XML.Elem(Markup(Markup.message(name), props), body)
             Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)