more uniform treatment of "bad" like other messages (with serial number);
authorwenzelm
Wed Dec 28 10:39:50 2016 +0100 (2016-12-28)
changeset 646778dc24130e8fe
parent 64676 fd2df1ea3bb4
child 64678 914dffe59cc5
more uniform treatment of "bad" like other messages (with serial number);
src/Pure/Isar/token.ML
src/Pure/ML/ml_lex.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/execution.ML
src/Pure/PIDE/markup.ML
src/Pure/Pure.thy
src/Pure/Syntax/syntax_ext.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Tools/print_operation.ML
src/Pure/skip_proof.ML
src/Tools/jEdit/src/jedit_rendering.scala
     1.1 --- a/src/Pure/Isar/token.ML	Tue Dec 27 17:33:57 2016 +0100
     1.2 +++ b/src/Pure/Isar/token.ML	Wed Dec 28 10:39:50 2016 +0100
     1.3 @@ -275,7 +275,7 @@
     1.4    | Verbatim => (Markup.verbatim, "")
     1.5    | Cartouche => (Markup.cartouche, "")
     1.6    | Comment => (Markup.comment, "")
     1.7 -  | Error msg => (Markup.bad, msg)
     1.8 +  | Error msg => (Markup.bad (), msg)
     1.9    | _ => (Markup.empty, "");
    1.10  
    1.11  fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), ""));
     2.1 --- a/src/Pure/ML/ml_lex.ML	Tue Dec 27 17:33:57 2016 +0100
     2.2 +++ b/src/Pure/ML/ml_lex.ML	Wed Dec 28 10:39:50 2016 +0100
     2.3 @@ -147,7 +147,7 @@
     2.4    | Char => (Markup.ML_char, "")
     2.5    | String => (if SML then Markup.SML_string else Markup.ML_string, "")
     2.6    | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
     2.7 -  | Error msg => (Markup.bad, msg)
     2.8 +  | Error msg => (Markup.bad (), msg)
     2.9    | _ => (Markup.empty, "");
    2.10  
    2.11  in
     3.1 --- a/src/Pure/PIDE/command.ML	Tue Dec 27 17:33:57 2016 +0100
     3.2 +++ b/src/Pure/PIDE/command.ML	Wed Dec 28 10:39:50 2016 +0100
     3.3 @@ -116,7 +116,7 @@
     3.4        Input.source_explode (Token.input_of tok)
     3.5        |> map_filter (fn (sym, pos) =>
     3.6            if Symbol.is_malformed sym
     3.7 -          then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
     3.8 +          then SOME ((pos, Markup.bad ()), "Malformed symbolic character") else NONE);
     3.9      val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
    3.10      val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
    3.11    in (is_malformed, reports) end;
    3.12 @@ -242,7 +242,7 @@
    3.13          let
    3.14            val _ = status tr Markup.failed;
    3.15            val _ = status tr Markup.finished;
    3.16 -          val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else ();
    3.17 +          val _ = if null errs then (report tr (Markup.bad ()); Exn.interrupt ()) else ();
    3.18          in {failed = true, command = tr, state = st} end
    3.19      | SOME st' =>
    3.20          let
     4.1 --- a/src/Pure/PIDE/execution.ML	Tue Dec 27 17:33:57 2016 +0100
     4.2 +++ b/src/Pure/PIDE/execution.ML	Wed Dec 28 10:39:50 2016 +0100
     4.3 @@ -116,7 +116,7 @@
     4.4                    Exn.Exn exn =>
     4.5                     (status task [Markup.failed];
     4.6                      status task [Markup.finished];
     4.7 -                    Output.report [Markup.markup_only Markup.bad];
     4.8 +                    Output.report [Markup.markup_only (Markup.bad ())];
     4.9                      if exec_id = 0 then ()
    4.10                      else List.app (Future.error_message pos) (Runtime.exn_messages_ids exn))
    4.11                  | Exn.Res _ =>
     5.1 --- a/src/Pure/PIDE/markup.ML	Tue Dec 27 17:33:57 2016 +0100
     5.2 +++ b/src/Pure/PIDE/markup.ML	Wed Dec 28 10:39:50 2016 +0100
     5.3 @@ -173,7 +173,7 @@
     5.4    val protocolN: string
     5.5    val reportN: string val report: T
     5.6    val no_reportN: string val no_report: T
     5.7 -  val badN: string val bad: T
     5.8 +  val badN: string val bad: unit -> T
     5.9    val intensifyN: string val intensify: T
    5.10    val browserN: string
    5.11    val graphviewN: string
    5.12 @@ -573,7 +573,8 @@
    5.13  val (reportN, report) = markup_elem "report";
    5.14  val (no_reportN, no_report) = markup_elem "no_report";
    5.15  
    5.16 -val (badN, bad) = markup_elem "bad";
    5.17 +val badN = "bad";
    5.18 +fun bad () = (badN, serial_properties (serial ()));
    5.19  
    5.20  val (intensifyN, intensify) = markup_elem "intensify";
    5.21  
     6.1 --- a/src/Pure/Pure.thy	Tue Dec 27 17:33:57 2016 +0100
     6.2 +++ b/src/Pure/Pure.thy	Wed Dec 28 10:39:50 2016 +0100
     6.3 @@ -991,7 +991,7 @@
     6.4  local
     6.5  
     6.6  fun report_back () =
     6.7 -  Output.report [Markup.markup Markup.bad "Explicit backtracking"];
     6.8 +  Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"];
     6.9  
    6.10  val _ =
    6.11    Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"
     7.1 --- a/src/Pure/Syntax/syntax_ext.ML	Tue Dec 27 17:33:57 2016 +0100
     7.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Wed Dec 28 10:39:50 2016 +0100
     7.3 @@ -217,7 +217,7 @@
     7.4    (case xsym of
     7.5      Delim s =>
     7.6        if Position.is_reported pos andalso exists Symbol.is_utf8 (Symbol.explode s) then
     7.7 -        [((pos, Markup.bad),
     7.8 +        [((pos, Markup.bad ()),
     7.9            "Mixfix delimiter contains raw Unicode -- this is non-portable and unreliable")]
    7.10        else []
    7.11    | _ => []);
     8.1 --- a/src/Pure/Syntax/syntax_phases.ML	Tue Dec 27 17:33:57 2016 +0100
     8.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Wed Dec 28 10:39:50 2016 +0100
     8.3 @@ -375,7 +375,7 @@
     8.4  
     8.5  fun parse_failed ctxt pos msg kind =
     8.6    cat_error msg ("Failed to parse " ^ kind ^
     8.7 -    Markup.markup_report (Context_Position.reported_text ctxt pos Markup.bad ""));
     8.8 +    Markup.markup_report (Context_Position.reported_text ctxt pos (Markup.bad ()) ""));
     8.9  
    8.10  fun parse_sort ctxt =
    8.11    Syntax.parse_input ctxt Term_XML.Decode.sort Markup.language_sort
    8.12 @@ -746,7 +746,7 @@
    8.13        | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
    8.14        | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
    8.15        | token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
    8.16 -      | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad, x))
    8.17 +      | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad (), x))
    8.18        | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
    8.19        | token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
    8.20        | token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
     9.1 --- a/src/Pure/Tools/print_operation.ML	Tue Dec 27 17:33:57 2016 +0100
     9.2 +++ b/src/Pure/Tools/print_operation.ML	Wed Dec 28 10:39:50 2016 +0100
     9.3 @@ -49,7 +49,7 @@
     9.4      (fn {state, args, writeln_result, ...} =>
     9.5        let
     9.6          val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
     9.7 -        fun err s = Pretty.mark_str (Markup.bad, s);
     9.8 +        fun err s = Pretty.mark_str (Markup.bad (), s);
     9.9          fun print name =
    9.10            (case AList.lookup (op =) (Synchronized.value print_operations) name of
    9.11              SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
    10.1 --- a/src/Pure/skip_proof.ML	Tue Dec 27 17:33:57 2016 +0100
    10.2 +++ b/src/Pure/skip_proof.ML	Wed Dec 28 10:39:50 2016 +0100
    10.3 @@ -19,7 +19,7 @@
    10.4  
    10.5  fun report ctxt =
    10.6    if Context_Position.is_visible ctxt then
    10.7 -    Output.report [Markup.markup Markup.bad "Skipped proof"]
    10.8 +    Output.report [Markup.markup (Markup.bad ()) "Skipped proof"]
    10.9    else ();
   10.10  
   10.11  
    11.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Dec 27 17:33:57 2016 +0100
    11.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Wed Dec 28 10:39:50 2016 +0100
    11.3 @@ -502,13 +502,9 @@
    11.4        snapshot.cumulate[List[Text.Info[Command.Results.Entry]]](
    11.5          range, Nil, JEdit_Rendering.tooltip_message_elements, _ =>
    11.6          {
    11.7 -          case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
    11.8 +          case (msgs, Text.Info(info_range,
    11.9 +            XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
   11.10            if body.nonEmpty =>
   11.11 -            val entry: Command.Results.Entry = (Document_ID.make(), msg)
   11.12 -            Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
   11.13 -
   11.14 -          case (msgs, Text.Info(info_range,
   11.15 -            XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) =>
   11.16              val entry: Command.Results.Entry =
   11.17                serial -> XML.Elem(Markup(Markup.message(name), props), body)
   11.18              Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)