# HG changeset patch
# User wenzelm
# Date 1729504551 -7200
# Node ID 94bace5078ba6fe81d308fa99c62e7d66ceee402
# Parent  6a33337eb08d895e7d63b02f449584806a1e0edf
support multiple positions (non-empty list);

diff -r 6a33337eb08d -r 94bace5078ba src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Sun Oct 20 22:40:18 2024 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy	Mon Oct 21 11:55:51 2024 +0200
@@ -70,8 +70,8 @@
       let fun err () = raise TERM ("string_tr", args) in
         (case args of
           [(c as Const (\<^syntax_const>\<open>_constrain\<close>, _)) $ Free (s, _) $ p] =>
-            (case Term_Position.decode_position p of
-              SOME (pos, _) => c $ mk_string (content (s, pos)) $ p
+            (case Term_Position.decode_position1 p of
+              SOME pos => c $ mk_string (content (s, pos)) $ p
             | NONE => err ())
         | _ => err ())
       end;
diff -r 6a33337eb08d -r 94bace5078ba src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Oct 20 22:40:18 2024 +0200
+++ b/src/Pure/Isar/specification.ML	Mon Oct 21 11:55:51 2024 +0200
@@ -94,7 +94,7 @@
     fun get Cs (Const ("_type_constraint_", C) $ t) = get (C :: Cs) t
       | get Cs (Free (y, T)) =
           if x = y then
-            map_filter Term_Position.decode_positionT
+            maps Term_Position.decode_positionT
               (T :: map (Type.constraint_type ctxt) Cs)
           else []
       | get _ (t $ u) = get [] t @ get [] u
diff -r 6a33337eb08d -r 94bace5078ba src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Sun Oct 20 22:40:18 2024 +0200
+++ b/src/Pure/Syntax/ast.ML	Mon Oct 21 11:55:51 2024 +0200
@@ -88,8 +88,8 @@
 
 fun pretty_var x =
   (case Term_Position.decode x of
-    SOME pos => Term_Position.pretty pos
-  | NONE => Pretty.str x);
+    [] => Pretty.str x
+  | ps => Term_Position.pretty ps);
 
 fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
   | pretty_ast (Variable x) = pretty_var x
@@ -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 is_some (Term_Position.decode x)
+      if member (op =) Term_Position.markers c andalso not (null (Term_Position.decode 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 6a33337eb08d -r 94bace5078ba src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Oct 20 22:40:18 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon Oct 21 11:55:51 2024 +0200
@@ -118,7 +118,7 @@
 (* decode_typ *)
 
 fun decode_pos (Free (s, _)) =
-      if is_some (Term_Position.decode s) then SOME s else NONE
+      if not (null (Term_Position.decode s)) then SOME s else NONE
   | decode_pos _ = NONE;
 
 fun decode_typ tm =
@@ -174,7 +174,7 @@
           if Lexicon.is_literal tok then report (report_pos tok) markup_cache a else ());
 
     val ast_of_pos = Ast.Variable o Term_Position.encode;
-    val ast_of_position = ast_of_pos o report_pos;
+    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;
 
     fun trans a args =
@@ -290,11 +290,11 @@
 
             fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
                   (case Term_Position.decode_position typ of
-                    SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t)
+                    SOME (ps', T) => Type.constraint T (decode (ps' @ ps) qs bs t)
                   | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t))
               | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
                   (case Term_Position.decode_position typ of
-                    SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t)
+                    SOME (qs', T) => Type.constraint (T --> dummyT) (decode ps (qs' @ qs) bs t)
                   | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t))
               | decode _ qs bs (Abs (x, T, t)) =
                   let
@@ -494,8 +494,8 @@
       | decode ps (Ast.Appl (asts as (Ast.Constant c :: ast :: Ast.Variable x :: args))) =
           if member (op =) Term_Position.markers c then
             (case Term_Position.decode x of
-              SOME p => Ast.mk_appl (decode (p :: ps) ast) (map (decode ps) args)
-            | NONE => decode_appl ps asts)
+              [] => decode_appl ps asts
+            | ps' => Ast.mk_appl (decode (ps' @ ps) ast) (map (decode ps) args))
           else decode_appl ps asts
       | decode ps (Ast.Appl asts) = decode_appl ps asts;
 
@@ -546,7 +546,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 is_some (Term_Position.decode x) then Syntax.free x
+          if not (null (Term_Position.decode 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;
@@ -877,8 +877,7 @@
   (case asts of
     [Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] =>
       let
-        val pos = the_default Position.none (Term_Position.decode p);
-        val (c', _) = decode_const ctxt (c, [pos]);
+        val (c', _) = decode_const ctxt (c, 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));
diff -r 6a33337eb08d -r 94bace5078ba src/Pure/Syntax/term_position.ML
--- a/src/Pure/Syntax/term_position.ML	Sun Oct 20 22:40:18 2024 +0200
+++ b/src/Pure/Syntax/term_position.ML	Mon Oct 21 11:55:51 2024 +0200
@@ -1,16 +1,17 @@
 (*  Title:      Pure/Syntax/term_position.ML
     Author:     Makarius
 
-Encoded position within term syntax trees.
+Positions within term syntax trees (non-empty list).
 *)
 
 signature TERM_POSITION =
 sig
-  val pretty: Position.T -> Pretty.T
-  val encode: Position.T -> string
-  val decode: string -> Position.T option
-  val decode_position: term -> (Position.T * typ) option
-  val decode_positionT: typ -> Position.T option
+  val pretty: Position.T list -> Pretty.T
+  val encode: Position.T list -> string
+  val decode: string -> Position.T list
+  val decode_position: term -> (Position.T list * typ) option
+  val decode_position1: term -> Position.T option
+  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
@@ -26,37 +27,53 @@
 val position_dummy = "<position>";
 val position_text = XML.Text position_dummy;
 
-fun pretty pos = Pretty.mark_str_position (pos, position_dummy);
+fun pretty ps = Pretty.marks_str (map Position.markup ps, position_dummy);
 
-fun encode pos =
-  YXML.string_of (XML.Elem (Position.markup pos, [position_text]));
+fun encode_pos pos = XML.Elem (Position.markup pos, [position_text]);
 
-fun decode str =
-  (case YXML.parse_body str handle Fail msg => error msg of
-    [XML.Elem ((name, props), [arg])] =>
+fun decode_pos (XML.Elem ((name, props), [arg])) =
       if name = Markup.positionN andalso arg = position_text
       then SOME (Position.of_properties props)
       else NONE
-  | _ => NONE);
+  | decode_pos _ = NONE;
+
+fun encode ps =
+  YXML.string_of_body (map encode_pos (if null ps then [Position.none] else ps));
+
+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;
 
 
 (* positions within parse trees *)
 
 fun decode_position (Free (x, _)) =
       (case decode x of
-        SOME pos => SOME (pos, TFree (x, dummyS))
-      | NONE => NONE)
+        [] => NONE
+      | ps => SOME (ps, TFree (x, dummyS)))
   | decode_position _ = NONE;
 
+fun decode_position1 (Free (x, _)) =
+      (case decode x of
+        [] => NONE
+      | pos :: _ => SOME pos)
+  | decode_position1 _ = NONE;
+
 fun decode_positionT (TFree (x, _)) = decode x
-  | decode_positionT _ = NONE;
+  | decode_positionT _ = [];
 
 fun decode_positionS cs =
-  let val (ps, sort) = List.partition (is_some o decode) cs
-  in (map (the o decode) ps, sort) end;
+  let val (ps, sort) = List.partition (not o null o decode) cs
+  in (maps decode ps, sort) end;
 
 val is_position = is_some o decode_position;
-val is_positionT = is_some o decode_positionT;
+val is_positionT = not o null o decode_positionT;
 
 val markers = ["_constrain", "_constrainAbs", "_ofsort"];
 
diff -r 6a33337eb08d -r 94bace5078ba src/Pure/type_infer_context.ML
--- a/src/Pure/type_infer_context.ML	Sun Oct 20 22:40:18 2024 +0200
+++ b/src/Pure/type_infer_context.ML	Mon Oct 21 11:55:51 2024 +0200
@@ -125,10 +125,12 @@
           in (Type (a, Ts'), ps_idx') end
       | prepareT T (ps, idx) =
           (case Term_Position.decode_positionT T of
-            SOME pos =>
-              let val U = Type_Infer.mk_param idx []
-              in (U, ((pos, U) :: ps, idx + 1)) end
-          | NONE => (T, (ps, idx)));
+            [] => (T, (ps, idx))
+          | pos =>
+              let
+                val U = Type_Infer.mk_param idx [];
+                val ps' = map (rpair U) pos;
+              in (U, (ps' @ ps, idx + 1)) end);
 
     fun prepare (Const ("_type_constraint_", T)) ps_idx =
           let