# HG changeset patch
# User wenzelm
# Date 1729766561 -7200
# Node ID 89ea66c2045b6e75c75132295d8d19ad6dd618aa
# Parent  08e0d3f248f95b589db2e0fa38e3c647ed48d38e
clarified position constraints: omit redundant information, e.g. for implicit object-logic judgment;

diff -r 08e0d3f248f9 -r 89ea66c2045b src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Oct 24 11:50:20 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Oct 24 12:42:41 2024 +0200
@@ -160,7 +160,7 @@
   | parsetree_literals (Parser.Tip tok) =
       if Lexicon.is_literal tok andalso
         not (null (Lexicon.literal_markup (Lexicon.str_of_token tok)))
-      then [Lexicon.pos_of_token tok] else [];
+      then filter Position.is_reported [Lexicon.pos_of_token tok] else [];
 
 fun parsetree_to_ast ctxt trf parsetree =
   let
@@ -223,7 +223,7 @@
             val ps = maps parsetree_literals pts;
             val args = maps asts_of pts;
             fun head () =
-              if (Lexicon.is_fixed a orelse Lexicon.is_const a)
+              if not (null ps) andalso (Lexicon.is_fixed a orelse Lexicon.is_const a)
                 andalso not (Config.get ctxt const_syntax_legacy)
               then Ast.constrain (Ast.Constant a) (ast_of_pos ps)
               else Ast.Constant a;
diff -r 08e0d3f248f9 -r 89ea66c2045b src/Pure/Syntax/term_position.ML
--- a/src/Pure/Syntax/term_position.ML	Thu Oct 24 11:50:20 2024 +0200
+++ b/src/Pure/Syntax/term_position.ML	Thu Oct 24 12:42:41 2024 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Syntax/term_position.ML
     Author:     Makarius
 
-Positions within term syntax trees (non-empty list).
+Reported positions within term syntax trees (non-empty list).
 *)
 
 signature TERM_POSITION =
@@ -44,9 +44,9 @@
 val encode_none = YXML.string_of (encode_pos Position.none);
 
 fun encode ps =
-  (case remove (op =) Position.none ps of
+  (case filter Position.is_reported ps of
     [] => encode_none
-  | ps' => YXML.string_of_body (map encode_pos (distinct (op =) ps')));
+  | ps' => YXML.string_of_body (map encode_pos ps'));
 
 val encode_prefix = YXML.XY ^ Markup.positionN;