--- a/src/Pure/PIDE/command.ML Sun Jul 09 16:29:13 2023 +0200
+++ b/src/Pure/PIDE/command.ML Sun Jul 09 17:39:46 2023 +0200
@@ -123,7 +123,12 @@
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));
+ else
+ let
+ val name = Toplevel.name_of tr;
+ val kind = the_default "" (Keyword.command_kind (Thy_Header.get_keywords thy) name);
+ val markup = Markup.command_span {name = name, kind = kind};
+ in Position.report (#1 core_range) markup end;
in tr end;
end;