# HG changeset patch
# User wenzelm
# Date 1610111146 -3600
# Node ID 84cde7fc4b86cf84be810f815d21ddece9486279
# Parent  d08cbc36a99af0a92fc6523a682401c58803e6dc
more uniform core_range (amending def3ec9cdb7e);

diff -r d08cbc36a99a -r 84cde7fc4b86 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Jan 07 13:28:13 2021 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Jan 08 14:05:46 2021 +0100
@@ -144,13 +144,6 @@
 fun read keywords thy master_dir init blobs_info span =
   let
     val command_reports = Outer_Syntax.command_reports thy;
-
-    val core_range = Token.range_of (drop_suffix Token.is_ignored span);
-    val pos =
-      (case find_first Token.is_command span of
-        SOME tok => Token.pos_of tok
-      | NONE => #1 core_range);
-
     val token_reports = map (reports_of_token keywords) span;
     val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span);
 
@@ -162,7 +155,8 @@
       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 pos "Malformed command syntax"
+    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;