# HG changeset patch
# User wenzelm
# Date 1726740536 -7200
# Node ID 51c33810397593a1ef78e45d4ec9b928c8e4763b
# Parent  71756d95b7df9da74716f0c51ebbdeca42aabfda
proper Context_Position.report, following 5328d67ec647;

diff -r 71756d95b7df -r 51c338103975 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Tue Sep 17 18:49:46 2024 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Thu Sep 19 12:08:56 2024 +0200
@@ -180,7 +180,7 @@
               Position.here (pos_of mx))
       | check_args _ NONE = ();
 
-    val _ = Position.reports_text (maps (mixfix_template_reports o #3) type_decls);
+    val _ = Context_Position.reports_text ctxt (maps (mixfix_template_reports o #3) type_decls);
 
     val mfix = map mfix_of type_decls;
     val _ = map2 check_args type_decls mfix;
@@ -227,7 +227,7 @@
     fun binder (c, _, Binder _) = SOME (binder_name c, c)
       | binder _ = NONE;
 
-    val _ = Position.reports_text (maps (mixfix_template_reports o #3) const_decls);
+    val _ = Context_Position.reports_text ctxt (maps (mixfix_template_reports o #3) const_decls);
 
     val mfix = maps mfix_of const_decls;
     val binders = map_filter binder const_decls;
diff -r 71756d95b7df -r 51c338103975 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Tue Sep 17 18:49:46 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Thu Sep 19 12:08:56 2024 +0200
@@ -291,7 +291,7 @@
     val nonterm_for_lhs = the_default "logic" o try dest_Type_name;
     val nonterm_for_rhs = the_default "any" o try dest_Type_name;
 
-    val _ = Position.report pos Markup.language_mixfix;
+    val _ = Context_Position.report ctxt pos Markup.language_mixfix;
     val symbs0 = read_mfix ctxt sy;
 
     fun err_in_mixfix msg = error (msg ^ " in mixfix annotation" ^ Position.here pos);