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