clarified term positions and markup: syntax = true means this is via concrete syntax;
clarified text color rendering;

--- a/src/HOL/ex/Cartouche_Examples.thy	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Sat Dec 07 23:50:18 2024 +0100
@@ -71,7 +71,7 @@
         (case args of
           [(c as Const (\<^syntax_const>\<open>_constrain\<close>, _)) $ Free (s, _) $ p] =>
             (case Term_Position.decode_position1 p of
-              SOME pos => c $ mk_string (content (s, pos)) $ p
+              SOME {pos, ...} => c $ mk_string (content (s, pos)) $ p
             | NONE => err ())
         | _ => err ())
       end;

--- a/src/Pure/Build/browser_info.scala	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Pure/Build/browser_info.scala	Sat Dec 07 23:50:18 2024 +0100
@@ -522,7 +522,7 @@
                 case _ =>
                   body1
               }
-            Rendering.foreground.get(name) orElse Rendering.get_text_color(name) match {
+            Rendering.foreground.get(name) orElse Rendering.get_text_color(markup) match {
               case Some(c) => (html_class(c.toString, html), offset)
               case None => (html_class(name, html), offset)
             }

--- a/src/Pure/General/position.ML	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Pure/General/position.ML	Sat Dec 07 23:50:18 2024 +0100
@@ -54,8 +54,6 @@
   type report_text = report * string
   val reports_text: report_text list -> unit
   val reports: report list -> unit
-  val store_reports: report_text list Unsynchronized.ref ->
-    T list -> ('a -> Markup.T list) -> 'a -> unit
   val append_reports: report_text list Unsynchronized.ref -> report list -> unit
   val here_strs: T -> string * string
   val here: T -> string
@@ -271,11 +269,6 @@
 
 val reports = map (rpair "") #> reports_text;
 
-fun store_reports _ [] _ _ = ()
-  | store_reports (r: report_text list Unsynchronized.ref) ps markup x =
-      let val ms = markup x
-      in Unsynchronized.change r (fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps) end;
-
 fun append_reports (r: report_text list Unsynchronized.ref) reports =
   Unsynchronized.change r (append (map (rpair "") reports));
 

--- a/src/Pure/Isar/proof_context.ML	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Dec 07 23:50:18 2024 +0100
@@ -790,7 +790,7 @@
           Vartab.insert (op =) (xi, Type.minimize_sort tsig S) env
             handle Vartab.DUP _ =>
               error ("Inconsistent sort constraints for type variable " ^
-                quote (Term.string_of_vname' xi) ^ Position.here_list ps)
+                quote (Term.string_of_vname' xi) ^ Position.here_list (map #pos ps))
       end;
 
     val env =
@@ -821,7 +821,7 @@
 
     fun get_sort_reports xi raw_S =
       let
-        val ps = #1 (Term_Position.decode_positionS raw_S);
+        val ps = map #pos (#1 (Term_Position.decode_positionS raw_S));
         val S = get_sort xi raw_S handle ERROR msg => error (msg ^ Position.here_list ps);
       in fold (add_report S) ps end;
 

--- a/src/Pure/Isar/specification.ML	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Dec 07 23:50:18 2024 +0100
@@ -100,7 +100,7 @@
       | get _ (t $ u) = get [] t @ get [] u
       | get _ (Abs (_, _, t)) = get [] t
       | get _ _ = [];
-  in get [] end;
+  in map #pos o get [] end;
 
 local
 

--- a/src/Pure/PIDE/markup.ML	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Dec 07 23:50:18 2024 +0100
@@ -196,6 +196,8 @@
   val comment1N: string val comment1: T
   val comment2N: string val comment2: T
   val comment3N: string val comment3: T
+  val syntaxN: string val syntax_properties: bool -> T -> T
+  val has_syntax: Properties.T -> bool
   val elapsedN: string
   val cpuN: string
   val gcN: string
@@ -675,6 +677,19 @@
 val (comment3N, comment3) = markup_elem "comment3";
 
 
+(* concrete syntax (notably mixfix notation) *)
+
+val syntaxN = "syntax";
+
+val syntax_elements = [improperN, freeN, skolemN];
+
+fun syntax_properties syntax (m as (elem, props): T) =
+  if syntax andalso member (op =) syntax_elements elem
+  then (elem, Properties.put (syntaxN, "true") props) else m;
+
+fun has_syntax props = Properties.get_bool props syntaxN;
+
+
 (* timing *)
 
 val elapsedN = "elapsed";

--- a/src/Pure/PIDE/markup.scala	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Dec 07 23:50:18 2024 +0100
@@ -479,6 +479,13 @@
   val COMMENT3 = "comment3"
 
 
+  /* concrete syntax (notably mixfix notation) */
+
+  val Syntax = new Properties.Boolean("syntax")
+
+  def has_syntax(props: Properties.T): Boolean = Syntax.get(props)
+
+
   /* timing */
 
   val Elapsed = new Properties.Double("elapsed")

--- a/src/Pure/PIDE/rendering.scala	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sat Dec 07 23:50:18 2024 +0100
@@ -105,14 +105,20 @@
 
   /* text color */
 
-  def get_text_color(name: String): Option[Color.Value] = text_colors.get(name)
+  def get_text_color(markup: Markup): Option[Color.Value] =
+    if (Markup.has_syntax(markup.properties)) text_color2.get(markup.name)
+    else text_color1.get(markup.name) orElse text_color2.get(markup.name)
 
-  private val text_colors = Map(
+  private val text_color1 = Map(
+    Markup.IMPROPER -> Color.improper,
+    Markup.FREE -> Color.free,
+    Markup.SKOLEM -> Color.skolem)
+
+  private val text_color2 = Map(
     Markup.KEYWORD1 -> Color.keyword1,
     Markup.KEYWORD2 -> Color.keyword2,
     Markup.KEYWORD3 -> Color.keyword3,
     Markup.QUASI_KEYWORD -> Color.quasi_keyword,
-    Markup.IMPROPER -> Color.improper,
     Markup.OPERATOR -> Color.operator,
     Markup.STRING -> Color.main,
     Markup.ALT_STRING -> Color.main,
@@ -121,8 +127,6 @@
     Markup.DELIMITER -> Color.main,
     Markup.TFREE -> Color.tfree,
     Markup.TVAR -> Color.tvar,
-    Markup.FREE -> Color.free,
-    Markup.SKOLEM -> Color.skolem,
     Markup.BOUND -> Color.bound,
     Markup.VAR -> Color.`var`,
     Markup.INNER_STRING -> Color.inner_quoted,
@@ -222,7 +226,7 @@
 
   val foreground_elements = Markup.Elements(foreground.keySet)
 
-  val text_color_elements = Markup.Elements(text_colors.keySet)
+  val text_color_elements = Markup.Elements(text_color1.keySet ++ text_color2.keySet)
 
   val structure_elements =
     Markup.Elements(Markup.NOTATION, Markup.EXPRESSION, Markup.LANGUAGE, Markup.ML_TYPING,

--- a/src/Pure/Syntax/ast.ML	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Pure/Syntax/ast.ML	Sat Dec 07 23:50:18 2024 +0100
@@ -89,7 +89,7 @@
 fun pretty_var x =
   (case Term_Position.decode x of
     [] => Pretty.str x
-  | ps => Term_Position.pretty ps);
+  | ps => Term_Position.pretty (map #pos ps));
 
 fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
   | pretty_ast (Variable x) = pretty_var x

--- a/src/Pure/Syntax/syntax_phases.ML	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Dec 07 23:50:18 2024 +0100
@@ -61,8 +61,9 @@
 
 fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
 
-fun markup_bound def ps (name, id) =
-  Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps;
+fun markup_bound def (ps: Term_Position.T list) (name, id) =
+  Markup.bound ::
+    map (fn {pos, ...} => Position.make_entity_markup def id Markup.boundN (name, pos)) ps;
 
 fun markup_entity ctxt c =
   Syntax.get_consts (Proof_Context.syntax_of ctxt) c
@@ -158,7 +159,7 @@
 fun parsetree_to_ast ctxt trf parsetree =
   let
     val reports = Unsynchronized.ref ([]: Position.report_text list);
-    fun report pos = Position.store_reports reports [pos];
+    fun report pos = Term_Position.store_reports reports [pos];
     val append_reports = Position.append_reports reports;
 
     fun report_pos tok =
@@ -168,8 +169,11 @@
     val markup_cache = Symtab.apply_unsynchronized_cache (markup_entity ctxt);
 
     val ast_of_pos = Ast.Variable o Term_Position.encode;
-    val ast_of_position = ast_of_pos o single o report_pos;
-    fun ast_of_position' a = Ast.constrain (Ast.Constant a) o ast_of_position;
+    val ast_of_position = Ast.Variable o Term_Position.encode_no_syntax o single o report_pos;
+
+    val syntax_ast_of_pos = Ast.Variable o Term_Position.encode_syntax;
+    val syntax_ast_of_position = syntax_ast_of_pos o single o report_pos;
+    fun syntax_ast_of_position' a = Ast.constrain (Ast.Constant a) o syntax_ast_of_position;
 
     fun asts_of_token tok =
       if Lexicon.valued_token tok
@@ -201,21 +205,21 @@
             val _ = append_reports rs;
           in [Ast.Constant (Lexicon.mark_type c)] end
       | asts_of (Parser.Node ({const = "_DDDOT", ...}, [Parser.Tip tok])) =
-          [Ast.constrain (Ast.Variable Auto_Bind.dddot_vname) (ast_of_position tok)]
+          [Ast.constrain (Ast.Variable Auto_Bind.dddot_vname) (syntax_ast_of_position tok)]
       | asts_of (Parser.Node ({const = "_position", ...}, [Parser.Tip tok])) =
           asts_of_position "_constrain" tok
       | asts_of (Parser.Node ({const = "_position_sort", ...}, [Parser.Tip tok])) =
           asts_of_position "_ofsort" tok
       | asts_of (Parser.Node ({const = a as "\<^const>Pure.dummy_pattern", ...}, [Parser.Tip tok])) =
-          [ast_of_position' a tok]
+          [syntax_ast_of_position' a tok]
       | asts_of (Parser.Node ({const = a as "_idtdummy", ...}, [Parser.Tip tok])) =
-          [ast_of_position' a tok]
+          [syntax_ast_of_position' a tok]
       | asts_of (Parser.Node ({const = "_idtypdummy", ...}, pts as [Parser.Tip tok, _, _])) =
           let val args = maps asts_of pts
-          in [Ast.Appl (Ast.Constant "_constrain" :: ast_of_position' "_idtdummy" tok :: args)] end
+          in [Ast.Appl (Ast.Constant "_constrain" :: syntax_ast_of_position' "_idtdummy" tok :: args)] end
       | asts_of (Parser.Node ({const = a, ...}, pts)) =
           let
-            val ps = maps parsetree_literals pts;
+            val ps = map Term_Position.syntax (maps parsetree_literals pts);
             val args = maps asts_of pts;
             fun head () =
               if not (null ps) andalso (Lexicon.is_fixed a orelse Lexicon.is_const a)
@@ -272,7 +276,7 @@
       | decode (reports0, Exn.Res tm) =
           let
             val reports = Unsynchronized.ref reports0;
-            fun report ps = Position.store_reports reports ps;
+            fun report ps = Term_Position.store_reports reports ps;
             val append_reports = Position.append_reports reports;
 
             fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
@@ -299,13 +303,13 @@
                           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)));
+                  ((Name.reject_internal (a, map #pos ps) handle ERROR msg =>
+                      error (msg ^ Proof_Context.consts_completion_message ctxt (a, map #pos ps)));
                     (case Proof_Context.lookup_free ctxt a of
                       SOME x => (report ps markup_free_cache x; Free (x, T))
                     | NONE =>
                         let
-                          val (c, rs) = decode_const ctxt (a, ps);
+                          val (c, rs) = decode_const ctxt (a, map #pos ps);
                           val _ = append_reports rs;
                         in Const (c, T) end))
               | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
@@ -462,7 +466,7 @@
     val syn = Proof_Context.syntax_of ctxt;
 
     val reports = Unsynchronized.ref ([]: Position.report_text list);
-    fun report ps = Position.store_reports reports ps;
+    fun report ps = Term_Position.store_reports reports ps;
 
     val markup_cache = Symtab.apply_unsynchronized_cache (markup_entity ctxt);
 
@@ -765,11 +769,12 @@
     val pretty_free_cache = Symtab.apply_unsynchronized_cache (pretty_free ctxt);
     val pretty_var_cache = Symtab.apply_unsynchronized_cache pretty_var;
 
-    val markup_syntax_cache = Symtab.apply_unsynchronized_cache (markup_entity ctxt);
+    val markup_syntax_cache =
+      Symtab.apply_unsynchronized_cache (markup_entity ctxt #> map (Markup.syntax_properties true));
 
     val pretty_entity_cache =
       Symtab.apply_unsynchronized_cache (fn a =>
-        Pretty.marks_str (markup_syntax_cache a, extern ctxt a));
+        Pretty.marks_str (markup_entity ctxt a, extern ctxt a));
 
     val cache1 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table);
     val cache2 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table);
@@ -872,7 +877,7 @@
   (case asts of
     [Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] =>
       let
-        val (c', _) = decode_const ctxt (c, Term_Position.decode p);
+        val (c', _) = decode_const ctxt (c, map #pos (Term_Position.decode p));
         val d = if intern then Lexicon.mark_const c' else c;
       in Ast.constrain (Ast.Constant d) T end
   | _ => raise Ast.AST ("const_ast_tr", asts));
@@ -995,7 +1000,7 @@
       |> apply_term_check ctxt
       |> chop (length ts);
     val typing_report =
-      fold2 (fn (pos, _) => fn ty =>
+      fold2 (fn ({pos, ...}, _) => fn ty =>
         if Position.is_reported pos then
           cons (Position.reported_text pos Markup.typing
             (Syntax.string_of_typ ctxt (Logic.dest_type ty)))

--- a/src/Pure/Syntax/term_position.ML	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Pure/Syntax/term_position.ML	Sat Dec 07 23:50:18 2024 +0100
@@ -6,16 +6,23 @@
 
 signature TERM_POSITION =
 sig
+  type T = {syntax: bool, pos: Position.T}
+  val syntax: Position.T -> T
+  val no_syntax: Position.T -> T
+  val store_reports: Position.report_text list Unsynchronized.ref ->
+    T list -> ('a -> Markup.T list) -> 'a -> unit
   val pretty: Position.T list -> Pretty.T
-  val encode: Position.T list -> string
+  val encode: T list -> string
+  val encode_syntax: Position.T list -> string
+  val encode_no_syntax: Position.T list -> string
   val detect: string -> bool
-  val decode: string -> Position.T list
+  val decode: string -> T list
   val detect_position: term -> bool
-  val decode_position: term -> (Position.T list * typ) option
-  val decode_position1: term -> Position.T option
+  val decode_position: term -> (T list * typ) option
+  val decode_position1: term -> T option
   val detect_positionT: typ -> bool
-  val decode_positionT: typ -> Position.T list
-  val decode_positionS: sort -> Position.T list * sort
+  val decode_positionT: typ -> T list
+  val decode_positionS: sort -> T list * sort
   val markers: string list
   val strip_positions: term -> term
 end;
@@ -23,6 +30,22 @@
 structure Term_Position: TERM_POSITION =
 struct
 
+(* type T *)
+
+type T = {syntax: bool, pos: Position.T};
+
+fun syntax pos : T = {syntax = true, pos = pos};
+fun no_syntax pos : T = {syntax = false, pos = pos};
+
+fun store_reports _ [] _ _ = ()
+  | store_reports (r: Position.report_text list Unsynchronized.ref) ps markup x =
+      let
+        val ms = markup x;
+        fun store {syntax, pos} =
+          fold (fn m => cons ((pos, Markup.syntax_properties syntax m), "")) ms;
+      in Unsynchronized.change r (fold store ps) end;
+
+
 (* markup *)
 
 val position_dummy = "<position>";
@@ -30,24 +53,28 @@
 
 fun pretty ps = Pretty.marks_str (map Position.markup ps, position_dummy);
 
-fun encode_pos pos = XML.Elem (Position.markup pos, [position_text]);
+fun encode_pos {syntax, pos} =
+  XML.Elem (Position.markup pos |> Markup.syntax_properties syntax, [position_text]);
 
 fun decode_pos (XML.Elem ((name, props), [arg])) =
       if name = Markup.positionN andalso arg = position_text
-      then SOME (Position.of_properties props)
+      then SOME {syntax = Markup.has_syntax props, pos = Position.of_properties props}
       else NONE
   | decode_pos _ = NONE;
 
 
 (* encode *)
 
-val encode_none = YXML.string_of (encode_pos Position.none);
+val encode_none = YXML.string_of (encode_pos (no_syntax Position.none));
 
 fun encode ps =
-  (case filter Position.is_reported ps of
+  (case filter (Position.is_reported o #pos) ps of
     [] => encode_none
   | ps' => YXML.string_of_body (map encode_pos ps'));
 
+val encode_syntax = encode o map syntax;
+val encode_no_syntax = encode o map no_syntax;
+
 val encode_prefix = YXML.XY ^ Markup.positionN;
 
 
@@ -56,7 +83,7 @@
 val detect = String.isPrefix encode_prefix;
 
 fun decode str =
-  if str = encode_none then [Position.none]
+  if str = encode_none then [no_syntax Position.none]
   else if detect str then
     let
       val xml = YXML.parse_body str handle Fail msg => error msg;

--- a/src/Pure/type_infer_context.ML	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Pure/type_infer_context.ML	Sat Dec 07 23:50:18 2024 +0100
@@ -8,7 +8,7 @@
 sig
   val const_sorts: bool Config.T
   val const_type: Proof.context -> string -> typ option
-  val prepare_positions: Proof.context -> term list -> term list * (Position.T * typ) list
+  val prepare_positions: Proof.context -> term list -> term list * (Term_Position.T * typ) list
   val prepare: Proof.context -> term list -> int * term list
   val infer_types: Proof.context -> term list -> term list
   val infer_types_finished: Proof.context -> term list -> term list

--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Sat Dec 07 23:50:18 2024 +0100
@@ -75,13 +75,13 @@
 
       val document = Line.Document(text)
       val decorations =
-        tree.cumulate[Option[String]](Text.Range.full, None, Rendering.text_color_elements,
-          { case (_, m) => Some(Some(m.info.name)) }
+        tree.cumulate[Option[Markup]](Text.Range.full, None, Rendering.text_color_elements,
+          { case (_, m) => Some(Some(m.info.markup)) }
         ).flatMap(info =>
             info.info match {
-              case Some(name) =>
+              case Some(markup) =>
                 val range = document.range(info.range)
-                Some((range, "text_" + Rendering.get_text_color(name).get.toString))
+                Some((range, "text_" + Rendering.get_text_color(markup).get.toString))
               case None => None
             }
         ).groupMap(_._2)(e => LSP.Decoration_Options(e._1, Nil)).toList

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sat Dec 07 23:50:18 2024 +0100
@@ -167,7 +167,7 @@
   def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = {
     snapshot.select(range, Rendering.text_color_elements, _ =>
       {
-        case Text.Info(_, elem) => Rendering.get_text_color(elem.name)
+        case Text.Info(_, elem) => Rendering.get_text_color(elem.markup)
       })
   }
 

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sat Dec 07 23:50:18 2024 +0100
@@ -375,7 +375,7 @@
     else
       snapshot.cumulate(range, current_color, Rendering.text_color_elements, _ =>
         {
-          case (_, Text.Info(_, elem)) => Rendering.get_text_color(elem.name).map(color)
+          case (_, Text.Info(_, elem)) => Rendering.get_text_color(elem.markup).map(color)
         })
   }