src/Pure/Syntax/term_position.ML

--- 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;