sneak message into "bad" markup as property -- to be displayed after YXML parsing;

--- a/src/Pure/ML/ml_lex.ML	Fri Aug 10 15:14:45 2012 +0200
+++ b/src/Pure/ML/ml_lex.ML	Fri Aug 10 15:57:22 2012 +0200
@@ -115,7 +115,7 @@
   | String    => Isabelle_Markup.ML_string
   | Space     => Markup.empty
   | Comment   => Isabelle_Markup.ML_comment
-  | Error _   => Isabelle_Markup.bad
+  | Error msg => Isabelle_Markup.bad msg
   | EOF       => Markup.empty;
 
 fun token_markup kind x =

--- a/src/Pure/PIDE/isabelle_markup.ML	Fri Aug 10 15:14:45 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Fri Aug 10 15:57:22 2012 +0200
@@ -95,7 +95,8 @@
   val promptN: string val prompt: Markup.T
   val reportN: string val report: Markup.T
   val no_reportN: string val no_report: Markup.T
-  val badN: string val bad: Markup.T
+  val messageN: string
+  val badN: string val bad: string -> Markup.T
   val functionN: string
   val assign_execs: Properties.T
   val removed_versions: Properties.T
@@ -286,7 +287,11 @@
 val (reportN, report) = markup_elem "report";
 val (no_reportN, no_report) = markup_elem "no_report";
 
-val (badN, bad) = markup_elem "bad";
+val messageN = "message"
+val badN = "bad"
+
+fun bad "" = (badN, [])
+  | bad msg = (badN, [(messageN, msg)]);
 
 
 (* protocol message functions *)

--- a/src/Pure/PIDE/isabelle_markup.scala	Fri Aug 10 15:14:45 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Fri Aug 10 15:57:22 2012 +0200
@@ -236,6 +236,7 @@
 
   val NO_REPORT = "no_report"
 
+  val Message = new Properties.String("message")
   val BAD = "bad"
 
 

--- a/src/Pure/Syntax/syntax_phases.ML	Fri Aug 10 15:14:45 2012 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Aug 10 15:57:22 2012 +0200
@@ -318,7 +318,7 @@
 fun parse_failed ctxt pos msg kind =
   cat_error msg ("Failed to parse " ^ kind ^
     Markup.markup Isabelle_Markup.report
-      (Context_Position.reported_text ctxt pos Isabelle_Markup.bad ""));
+      (Context_Position.reported_text ctxt pos (Isabelle_Markup.bad "") ""));
 
 fun parse_sort ctxt =
   Syntax.parse_token ctxt Term_XML.Decode.sort Isabelle_Markup.sort
@@ -609,7 +609,7 @@
       | token_trans "_tvar" x = SOME (Pretty.mark_str (Isabelle_Markup.tvar, x))
       | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
       | token_trans "_bound" x = SOME (Pretty.mark_str (Isabelle_Markup.bound, x))
-      | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.bad, x))
+      | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.bad "", x))
       | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
       | token_trans "_numeral" x = SOME (Pretty.mark_str (Isabelle_Markup.numeral, x))
       | token_trans "_inner_string" x = SOME (Pretty.mark_str (Isabelle_Markup.inner_string, x))

--- a/src/Pure/Thy/thy_syntax.ML	Fri Aug 10 15:14:45 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Fri Aug 10 15:57:22 2012 +0200
@@ -54,7 +54,7 @@
   | Token.Space         => Markup.empty
   | Token.Comment       => Isabelle_Markup.comment
   | Token.InternalValue => Markup.empty
-  | Token.Error _       => Isabelle_Markup.bad
+  | Token.Error msg     => Isabelle_Markup.bad msg
   | Token.Sync          => Isabelle_Markup.control
   | Token.EOF           => Isabelle_Markup.control;
 
@@ -74,7 +74,8 @@
     val malformed_symbols =
       Symbol_Pos.explode (Token.source_position_of tok)
       |> map_filter (fn (sym, pos) =>
-          if Symbol.is_malformed sym then SOME (pos, Isabelle_Markup.bad) else NONE);
+          if Symbol.is_malformed sym
+          then SOME (pos, Isabelle_Markup.bad "Malformed symbol") else NONE);
     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
     val reports = (Token.position_of tok, token_markup tok) :: malformed_symbols;
   in (is_malformed, reports) end;

--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Aug 10 15:14:45 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Aug 10 15:57:22 2012 +0200
@@ -104,18 +104,25 @@
   }
 
 
+  private def tooltip_text(msg: XML.Body): String =
+    Pretty.string_of(msg, margin = Isabelle.Int_Property("tooltip-margin"))
+
   def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
   {
     val msgs =
       snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
-        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
+        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR,
+          Isabelle_Markup.BAD)),
         {
-          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
+          case (msgs, Text.Info(_, msg @
+              XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
           if markup == Isabelle_Markup.WRITELN ||
               markup == Isabelle_Markup.WARNING ||
               markup == Isabelle_Markup.ERROR =>
-            msgs + (serial ->
-              Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
+            msgs + (serial -> tooltip_text(List(msg)))
+          case (msgs, Text.Info(_,
+              XML.Elem(Markup(Isabelle_Markup.BAD, Isabelle_Markup.Message(msg)), _))) =>
+            msgs + (0L -> tooltip_text(YXML.parse_body(msg)))
         }).toList.flatMap(_.info)
     if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
   }