# HG changeset patch
# User wenzelm
# Date 1729618000 -7200
# Node ID 9867b5cf3f7affe94f6d2ba3a090bcd5eeb12181
# Parent  808d940fa83884756463191930e41c3908c4cb3a
more concise representation of term positions;

diff -r 808d940fa838 -r 9867b5cf3f7a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Oct 22 13:39:24 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Oct 22 19:26:40 2024 +0200
@@ -779,7 +779,7 @@
     val reports =
       (fold o fold_atyps)
         (fn T =>
-          if Term_Position.is_positionT T then I
+          if Term_Position.detect_positionT T then I
           else
             (case T of
               TFree (x, raw_S) => get_sort_reports (x, ~1) raw_S
@@ -791,7 +791,7 @@
 fun replace_sortsT_same get_sort =
   Term.map_atyps_same
     (fn T =>
-      if Term_Position.is_positionT T then raise Same.SAME
+      if Term_Position.detect_positionT T then raise Same.SAME
       else
         (case T of
           TFree (x, raw_S) => TFree (x, Same.function_eq (op =) (get_sort (x, ~1)) raw_S)
diff -r 808d940fa838 -r 9867b5cf3f7a src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Tue Oct 22 13:39:24 2024 +0200
+++ b/src/Pure/Syntax/ast.ML	Tue Oct 22 19:26:40 2024 +0200
@@ -104,7 +104,7 @@
 (* strip_positions *)
 
 fun strip_positions (Appl ((t as Constant c) :: u :: (v as Variable x) :: asts)) =
-      if member (op =) Term_Position.markers c andalso not (null (Term_Position.decode x))
+      if member (op =) Term_Position.markers c andalso Term_Position.detect x
       then mk_appl (strip_positions u) (map strip_positions asts)
       else Appl (map strip_positions (t :: u :: v :: asts))
   | strip_positions (Appl asts) = Appl (map strip_positions asts)
diff -r 808d940fa838 -r 9867b5cf3f7a src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Oct 22 13:39:24 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Oct 22 19:26:40 2024 +0200
@@ -117,8 +117,7 @@
 
 (* decode_typ *)
 
-fun decode_pos (Free (s, _)) =
-      if not (null (Term_Position.decode s)) then SOME s else NONE
+fun decode_pos (Free (x, _)) = if Term_Position.detect x then SOME x else NONE
   | decode_pos _ = NONE;
 
 fun decode_typ tm =
@@ -546,7 +545,7 @@
     fun term_of (Type (a, Ts)) =
           Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts)
       | term_of (TFree (x, S)) =
-          if not (null (Term_Position.decode x)) then Syntax.free x
+          if Term_Position.detect x then Syntax.free x
           else ofsort (Syntax.const "_tfree" $ Syntax.free x) S
       | term_of (TVar (xi, S)) = ofsort (Syntax.const "_tvar" $ Syntax.var xi) S;
   in term_of ty end;
diff -r 808d940fa838 -r 9867b5cf3f7a src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Tue Oct 22 13:39:24 2024 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Tue Oct 22 19:26:40 2024 +0200
@@ -205,7 +205,7 @@
 fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
   | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
   | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
-      if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
+      if Term_Position.detect_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
       else
         list_comb (c $ update_name_tr [t] $
           (Lexicon.fun_type $
diff -r 808d940fa838 -r 9867b5cf3f7a src/Pure/Syntax/term_position.ML
--- a/src/Pure/Syntax/term_position.ML	Tue Oct 22 13:39:24 2024 +0200
+++ b/src/Pure/Syntax/term_position.ML	Tue Oct 22 19:26:40 2024 +0200
@@ -8,13 +8,14 @@
 sig
   val pretty: Position.T list -> Pretty.T
   val encode: Position.T list -> string
+  val detect: string -> bool
   val decode: string -> Position.T list
+  val detect_position: term -> bool
   val decode_position: term -> (Position.T list * typ) option
   val decode_position1: term -> Position.T option
+  val detect_positionT: typ -> bool
   val decode_positionT: typ -> Position.T list
   val decode_positionS: sort -> Position.T list * sort
-  val is_position: term -> bool
-  val is_positionT: typ -> bool
   val markers: string list
   val strip_positions: term -> term
 end;
@@ -37,22 +38,42 @@
       else NONE
   | decode_pos _ = NONE;
 
+
+(* encode *)
+
+val encode_none = YXML.string_of (encode_pos Position.none);
+
 fun encode ps =
-  YXML.string_of_body (map encode_pos (if null ps then [Position.none] else ps));
+  (case remove (op =) Position.none ps of
+    [] => encode_none
+  | ps' => YXML.string_of_body (map encode_pos (distinct (op =) ps')));
+
+val encode_prefix = YXML.XY ^ Markup.positionN;
+
+
+(* decode *)
+
+val detect = String.isPrefix encode_prefix;
 
 fun decode str =
-  let
-    val xml = YXML.parse_body str handle Fail msg => error msg;
-    val ps = map decode_pos xml;
-  in
-    if not (null ps) andalso forall is_some ps then map the ps
-    else if forall is_none ps then []
-    else error ("Bad encoded positions: " ^ quote str)
-  end;
+  if str = encode_none then [Position.none]
+  else if detect str then
+    let
+      val xml = YXML.parse_body str handle Fail msg => error msg;
+      val ps = map decode_pos xml;
+    in
+      if not (null ps) andalso forall is_some ps then map the ps
+      else if forall is_none ps then []
+      else error ("Bad encoded positions: " ^ quote str)
+    end
+  else [];
 
 
 (* positions within parse trees *)
 
+fun detect_position (Free (x, _)) = detect x
+  | detect_position _ = false;
+
 fun decode_position (Free (x, _)) =
       (case decode x of
         [] => NONE
@@ -65,20 +86,23 @@
       | pos :: _ => SOME pos)
   | decode_position1 _ = NONE;
 
+fun detect_positionT (TFree (x, _)) = detect x
+  | detect_positionT _ = false;
+
 fun decode_positionT (TFree (x, _)) = decode x
   | decode_positionT _ = [];
 
 fun decode_positionS cs =
-  let val (ps, sort) = List.partition (not o null o decode) cs
+  let val (ps, sort) = List.partition detect cs
   in (maps decode ps, sort) end;
 
-val is_position = is_some o decode_position;
-val is_positionT = not o null o decode_positionT;
+
+(* strip_positions *)
 
 val markers = ["_constrain", "_constrainAbs", "_ofsort"];
 
 fun strip_positions ((t as Const (c, _)) $ u $ v) =
-      if member (op =) markers c andalso is_position v
+      if member (op =) markers c andalso detect_position v
       then strip_positions u
       else t $ strip_positions u $ strip_positions v
   | strip_positions (t $ u) = strip_positions t $ strip_positions u