# HG changeset patch # User wenzelm # Date 1344698661 -7200 # Node ID abc45de5bb22838b7d7b4a5b0b7e3d1765cae2ac # Parent 7f0c469cc796da3a99400a7d1309498f21a1bb85 clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards); diff -r 7f0c469cc796 -r abc45de5bb22 src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Sat Aug 11 17:23:09 2012 +0200 +++ b/src/Pure/General/antiquote.ML Sat Aug 11 17:24:21 2012 +0200 @@ -12,7 +12,8 @@ Open of Position.T | Close of Position.T val is_text: 'a antiquote -> bool - val reports_of: ('a -> Position.report list) -> 'a antiquote list -> Position.report list + val reports_of: ('a -> Position.report_text list) -> + 'a antiquote list -> Position.report_text list val check_nesting: 'a antiquote list -> unit val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list @@ -40,9 +41,9 @@ fun reports_of text = maps (fn Text x => text x - | Antiq (_, (pos, _)) => [(pos, Isabelle_Markup.antiq)] - | Open pos => [(pos, Isabelle_Markup.antiq)] - | Close pos => [(pos, Isabelle_Markup.antiq)]); + | Antiq (_, (pos, _)) => [((pos, Isabelle_Markup.antiq), "")] + | Open pos => [((pos, Isabelle_Markup.antiq), "")] + | Close pos => [((pos, Isabelle_Markup.antiq), "")]); (* check_nesting *) @@ -99,7 +100,7 @@ fun read (syms, pos) = (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of - SOME xs => (Position.reports (reports_of (K []) xs); check_nesting xs; xs) + SOME xs => (Position.reports_text (reports_of (K []) xs); check_nesting xs; xs) | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos)); end; diff -r 7f0c469cc796 -r abc45de5bb22 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Sat Aug 11 17:23:09 2012 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Sat Aug 11 17:24:21 2012 +0200 @@ -284,12 +284,12 @@ let val name = Token.content_of tok in (case commands name of NONE => [] - | SOME cmd => [(Token.position_of tok, command_markup false (name, cmd))]) + | SOME cmd => [((Token.position_of tok, command_markup false (name, cmd)), "")]) end else []; val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks; - val _ = Position.reports (token_reports @ maps command_reports toks); + val _ = Position.reports_text (token_reports @ maps command_reports toks); in if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true) else diff -r 7f0c469cc796 -r abc45de5bb22 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Sat Aug 11 17:23:09 2012 +0200 +++ b/src/Pure/ML/ml_lex.ML Sat Aug 11 17:24:21 2012 +0200 @@ -104,28 +104,30 @@ local val token_kind_markup = - fn Keyword => Isabelle_Markup.ML_keyword - | Ident => Markup.empty - | LongIdent => Markup.empty - | TypeVar => Isabelle_Markup.ML_tvar - | Word => Isabelle_Markup.ML_numeral - | Int => Isabelle_Markup.ML_numeral - | Real => Isabelle_Markup.ML_numeral - | Char => Isabelle_Markup.ML_char - | String => Isabelle_Markup.ML_string - | Space => Markup.empty - | Comment => Isabelle_Markup.ML_comment - | Error msg => Isabelle_Markup.bad msg - | EOF => Markup.empty; + fn Keyword => (Isabelle_Markup.ML_keyword, "") + | Ident => (Markup.empty, "") + | LongIdent => (Markup.empty, "") + | TypeVar => (Isabelle_Markup.ML_tvar, "") + | Word => (Isabelle_Markup.ML_numeral, "") + | Int => (Isabelle_Markup.ML_numeral, "") + | Real => (Isabelle_Markup.ML_numeral, "") + | Char => (Isabelle_Markup.ML_char, "") + | String => (Isabelle_Markup.ML_string, "") + | Space => (Markup.empty, "") + | Comment => (Isabelle_Markup.ML_comment, "") + | Error msg => (Isabelle_Markup.bad, msg) + | EOF => (Markup.empty, ""); fun token_markup kind x = if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x - then Isabelle_Markup.ML_delimiter + then (Isabelle_Markup.ML_delimiter, "") else token_kind_markup kind; in -fun report_of_token (Token ((pos, _), (kind, x))) = (pos, token_markup kind x); +fun report_of_token (Token ((pos, _), (kind, x))) = + let val (markup, txt) = token_markup kind x + in ((pos, markup), txt) end; end; @@ -301,7 +303,7 @@ |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq)) (SOME (false, fn msg => recover msg >> map Antiquote.Text)) |> Source.exhaust - |> tap (Position.reports o Antiquote.reports_of (single o report_of_token)) + |> tap (Position.reports_text o Antiquote.reports_of (single o report_of_token)) |> tap Antiquote.check_nesting |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ()))) handle ERROR msg => diff -r 7f0c469cc796 -r abc45de5bb22 src/Pure/PIDE/isabelle_markup.ML --- a/src/Pure/PIDE/isabelle_markup.ML Sat Aug 11 17:23:09 2012 +0200 +++ b/src/Pure/PIDE/isabelle_markup.ML Sat Aug 11 17:24:21 2012 +0200 @@ -95,8 +95,7 @@ val promptN: string val prompt: Markup.T val reportN: string val report: Markup.T val no_reportN: string val no_report: Markup.T - val messageN: string - val badN: string val bad: string -> Markup.T + val badN: string val bad: Markup.T val functionN: string val assign_execs: Properties.T val removed_versions: Properties.T @@ -287,11 +286,7 @@ val (reportN, report) = markup_elem "report"; val (no_reportN, no_report) = markup_elem "no_report"; -val messageN = "message" -val badN = "bad" - -fun bad "" = (badN, []) - | bad msg = (badN, [(messageN, msg)]); +val (badN, bad) = markup_elem "bad"; (* protocol message functions *) diff -r 7f0c469cc796 -r abc45de5bb22 src/Pure/PIDE/isabelle_markup.scala --- a/src/Pure/PIDE/isabelle_markup.scala Sat Aug 11 17:23:09 2012 +0200 +++ b/src/Pure/PIDE/isabelle_markup.scala Sat Aug 11 17:24:21 2012 +0200 @@ -236,7 +236,6 @@ val NO_REPORT = "no_report" - val Message = new Properties.String("message") val BAD = "bad" diff -r 7f0c469cc796 -r abc45de5bb22 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Sat Aug 11 17:23:09 2012 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Sat Aug 11 17:24:21 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)) diff -r 7f0c469cc796 -r abc45de5bb22 src/Pure/Thy/thy_syntax.ML --- a/src/Pure/Thy/thy_syntax.ML Sat Aug 11 17:23:09 2012 +0200 +++ b/src/Pure/Thy/thy_syntax.ML Sat Aug 11 17:24:21 2012 +0200 @@ -7,7 +7,7 @@ signature THY_SYNTAX = sig val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list - val reports_of_tokens: Token.T list -> bool * Position.report list + val reports_of_tokens: Token.T list -> bool * (Position.report * string) list val present_token: Token.T -> Output.output datatype span_kind = Command of string | Ignored | Malformed type span @@ -38,28 +38,29 @@ local val token_kind_markup = - fn Token.Command => Isabelle_Markup.command - | Token.Keyword => Isabelle_Markup.keyword - | Token.Ident => Markup.empty - | Token.LongIdent => Markup.empty - | Token.SymIdent => Markup.empty - | Token.Var => Isabelle_Markup.var - | Token.TypeIdent => Isabelle_Markup.tfree - | Token.TypeVar => Isabelle_Markup.tvar - | Token.Nat => Markup.empty - | Token.Float => Markup.empty - | Token.String => Isabelle_Markup.string - | Token.AltString => Isabelle_Markup.altstring - | Token.Verbatim => Isabelle_Markup.verbatim - | Token.Space => Markup.empty - | Token.Comment => Isabelle_Markup.comment - | Token.InternalValue => Markup.empty - | Token.Error msg => Isabelle_Markup.bad msg - | Token.Sync => Isabelle_Markup.control - | Token.EOF => Isabelle_Markup.control; + fn Token.Command => (Isabelle_Markup.command, "") + | Token.Keyword => (Isabelle_Markup.keyword, "") + | Token.Ident => (Markup.empty, "") + | Token.LongIdent => (Markup.empty, "") + | Token.SymIdent => (Markup.empty, "") + | Token.Var => (Isabelle_Markup.var, "") + | Token.TypeIdent => (Isabelle_Markup.tfree, "") + | Token.TypeVar => (Isabelle_Markup.tvar, "") + | Token.Nat => (Markup.empty, "") + | Token.Float => (Markup.empty, "") + | Token.String => (Isabelle_Markup.string, "") + | Token.AltString => (Isabelle_Markup.altstring, "") + | Token.Verbatim => (Isabelle_Markup.verbatim, "") + | Token.Space => (Markup.empty, "") + | Token.Comment => (Isabelle_Markup.comment, "") + | Token.InternalValue => (Markup.empty, "") + | Token.Error msg => (Isabelle_Markup.bad, msg) + | Token.Sync => (Isabelle_Markup.control, "") + | Token.EOF => (Isabelle_Markup.control, ""); fun token_markup tok = - if Token.keyword_with (not o Lexicon.is_ascii_identifier) tok then Isabelle_Markup.operator + if Token.keyword_with (not o Lexicon.is_ascii_identifier) tok + then (Isabelle_Markup.operator, "") else let val kind = Token.kind_of tok; @@ -67,7 +68,8 @@ if kind = Token.Command then Markup.properties [(Markup.nameN, Token.content_of tok)] else I; - in props (token_kind_markup kind) end; + val (markup, txt) = token_kind_markup kind; + in (props markup, txt) end; fun reports_of_token tok = let @@ -75,9 +77,10 @@ Symbol_Pos.explode (Token.source_position_of tok) |> map_filter (fn (sym, pos) => if Symbol.is_malformed sym - then SOME (pos, Isabelle_Markup.bad "Malformed symbol") else NONE); + 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; + val (markup, txt) = token_markup tok; + val reports = ((Token.position_of tok, markup), txt) :: malformed_symbols; in (is_malformed, reports) end; in @@ -87,7 +90,7 @@ in (exists fst results, maps snd results) end; fun present_token tok = - Markup.enclose (token_markup tok) (Output.output (Token.unparse tok)); + Markup.enclose (fst (token_markup tok)) (Output.output (Token.unparse tok)); end; diff -r 7f0c469cc796 -r abc45de5bb22 src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Sat Aug 11 17:23:09 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Sat Aug 11 17:24:21 2012 +0200 @@ -104,8 +104,8 @@ } - private def tooltip_text(msg: XML.Body): String = - Pretty.string_of(msg, margin = Isabelle.Int_Property("tooltip-margin")) + private def tooltip_text(msg: XML.Tree): String = + Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")) def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] = { @@ -119,10 +119,9 @@ if markup == Isabelle_Markup.WRITELN || markup == Isabelle_Markup.WARNING || markup == Isabelle_Markup.ERROR => - 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))) + msgs + (serial -> tooltip_text(msg)) + case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) => + msgs + (Document.new_id() -> tooltip_text(msg)) }).toList.flatMap(_.info) if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2))) }