# HG changeset patch
# User wenzelm
# Date 1635953000 -3600
# Node ID eae5fa0055bdd5a43a392f0ad20c07f4e61762d5
# Parent  1a8fd26fedb636e30d001ab89ad87f314c5bd2f6
more PIDE markup;

diff -r 1a8fd26fedb6 -r eae5fa0055bd src/Pure/PIDE/command.ML
--- 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;
 
diff -r 1a8fd26fedb6 -r eae5fa0055bd src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Nov 03 16:19:49 2021 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Nov 03 16:23:20 2021 +0100
@@ -158,6 +158,7 @@
   val descriptionN: string
   val inputN: string val input: bool -> Properties.T -> T
   val command_keywordN: string val command_keyword: T
+  val command_spanN: string val command_span: string -> T
   val commandN: string val command_properties: T -> T
   val keywordN: string val keyword_properties: T -> T
   val stringN: string val string: T
@@ -592,6 +593,7 @@
 (* outer syntax *)
 
 val (command_keywordN, command_keyword) = markup_elem "command_keyword";
+val (command_spanN, command_span) = markup_string "command_span" nameN;
 
 val commandN = "command"; val command_properties = properties [(kindN, commandN)];
 val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)];
diff -r 1a8fd26fedb6 -r eae5fa0055bd src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed Nov 03 16:19:49 2021 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Nov 03 16:23:20 2021 +0100
@@ -414,6 +414,9 @@
 
   /* outer syntax */
 
+  val COMMAND_SPAN = "command_span"
+  val Command_Span = new Markup_String(COMMAND_SPAN, NAME)
+
   val COMMAND = "command"
   val KEYWORD = "keyword"
   val KEYWORD1 = "keyword1"