# HG changeset patch # User wenzelm # Date 1482917990 -3600 # Node ID 8dc24130e8fe41084bbb619d6539f9e9184a1860 # Parent fd2df1ea3bb45747b7ed3b00bd0f6393f308bb25 more uniform treatment of "bad" like other messages (with serial number); diff -r fd2df1ea3bb4 -r 8dc24130e8fe src/Pure/Isar/token.ML --- 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), "")); diff -r fd2df1ea3bb4 -r 8dc24130e8fe src/Pure/ML/ml_lex.ML --- 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 diff -r fd2df1ea3bb4 -r 8dc24130e8fe src/Pure/PIDE/command.ML --- 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 diff -r fd2df1ea3bb4 -r 8dc24130e8fe src/Pure/PIDE/execution.ML --- 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 _ => diff -r fd2df1ea3bb4 -r 8dc24130e8fe src/Pure/PIDE/markup.ML --- 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"; diff -r fd2df1ea3bb4 -r 8dc24130e8fe src/Pure/Pure.thy --- 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" diff -r fd2df1ea3bb4 -r 8dc24130e8fe src/Pure/Syntax/syntax_ext.ML --- 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 [] | _ => []); diff -r fd2df1ea3bb4 -r 8dc24130e8fe src/Pure/Syntax/syntax_phases.ML --- 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)) diff -r fd2df1ea3bb4 -r 8dc24130e8fe src/Pure/Tools/print_operation.ML --- 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"]) diff -r fd2df1ea3bb4 -r 8dc24130e8fe src/Pure/skip_proof.ML --- 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 (); diff -r fd2df1ea3bb4 -r 8dc24130e8fe src/Tools/jEdit/src/jedit_rendering.scala --- 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)