--- a/src/Pure/PIDE/command.ML Wed Nov 03 16:19:49 2021 +0100
+++ b/src/Pure/PIDE/command.ML Wed Nov 03 16:23:20 2021 +0100
@@ -154,11 +154,16 @@
if null verbatim then ()
else legacy_feature ("Old-style {* verbatim *} token -- use \<open>cartouche\<close> instead" ^
Position.here_list verbatim);
- in
- if exists #1 token_reports
- then Toplevel.malformed (#1 (Token.core_range_of span)) "Malformed command syntax"
- else Outer_Syntax.parse_span thy init (resolve_files master_dir blobs_info span)
- end;
+
+ val core_range = Token.core_range_of span;
+ val tr =
+ if exists #1 token_reports
+ then Toplevel.malformed (#1 core_range) "Malformed command syntax"
+ else Outer_Syntax.parse_span thy init (resolve_files master_dir blobs_info span);
+ val _ =
+ if Toplevel.is_ignored tr orelse Toplevel.is_malformed tr then ()
+ else Position.report (#1 core_range) (Markup.command_span (Toplevel.name_of tr));
+ in tr end;
end;