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)))
}