# HG changeset patch
# User wenzelm
# Date 1729619165 -7200
# Node ID 0199acc01aa88832a7f808e7699b74b91a5046fd
# Parent  9867b5cf3f7affe94f6d2ba3a090bcd5eeb12181
more parser markup, based on position constraints for logical mixfix syntax;

diff -r 9867b5cf3f7a -r 0199acc01aa8 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Oct 22 19:26:40 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Oct 22 19:46:05 2024 +0200
@@ -152,6 +152,13 @@
 
 (* parsetree_to_ast *)
 
+fun parsetree_literals (Parser.Markup (_, ts)) = maps parsetree_literals ts
+  | parsetree_literals (Parser.Node _) = []
+  | 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 [];
+
 fun parsetree_to_ast ctxt trf parsetree =
   let
     val reports = Unsynchronized.ref ([]: Position.report_text list);
@@ -222,7 +229,19 @@
           let val args = maps asts_of pts
           in [Ast.Appl (Ast.Constant "_constrain" :: ast_of_position' "_idtdummy" tok :: args)] end
       | asts_of (Parser.Node ({const = a, ...}, pts)) =
-          (report_literals a pts; [trans a (maps asts_of pts)])
+          let
+            val ps = maps parsetree_literals pts;
+            val args = maps asts_of pts;
+            fun head () =
+              if Lexicon.is_fixed a orelse Lexicon.is_const a
+              then Ast.constrain (Ast.Constant a) (ast_of_pos ps)
+              else Ast.Constant a;
+            val _ = List.app (fn pos => report pos markup_cache a) ps;
+          in
+            [case trf a of
+              SOME f => f ctxt args
+            | NONE => Ast.mk_appl (head ()) args]
+          end
       | asts_of (Parser.Tip tok) = asts_of_token tok
 
     and ast_of pt =
@@ -303,15 +322,13 @@
               | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
               | decode ps _ _ (Const (a, T)) =
                   (case try Lexicon.unmark_fixed a of
-                    SOME x => (report ps markup_free_cache x; Free (x, T))
+                    SOME x => Free (x, T)
                   | NONE =>
-                      let
-                        val c =
-                          (case try Lexicon.unmark_const a of
-                            SOME c => c
-                          | NONE => #1 (decode_const ctxt (a, [])));
-                        val _ = report ps markup_const_cache c;
-                      in Const (c, T) end)
+                      (case try Lexicon.unmark_const a of
+                        SOME c => Const (c, T)
+                      | NONE =>
+                          let val c = #1 (decode_const ctxt (a, []))
+                          in report ps markup_const_cache c; Const (c, T) end))
               | decode ps _ _ (Free (a, T)) =
                   ((Name.reject_internal (a, ps) handle ERROR msg =>
                       error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));