# HG changeset patch
# User wenzelm
# Date 1695656232 -7200
# Node ID 55b1664b564be497f86c51184496acd46595267d
# Parent  5c40df5f0ce9338e94423f35f5d12e11e884935f
more position information, e.g. for warning about fn-pattern;

diff -r 5c40df5f0ce9 -r 55b1664b564b src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Mon Sep 25 16:55:11 2023 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Mon Sep 25 17:37:12 2023 +0200
@@ -345,14 +345,15 @@
 local
 
 val tokenize_text = map Antiquote.Text o ML_Lex.tokenize_no_range;
+val tokenize_range_text = map Antiquote.Text oo ML_Lex.tokenize_range;
 
 val bg_expr = tokenize_text "(fn () =>";
 val en_expr = tokenize_text ")";
 fun make_expr a = bg_expr @ a @ en_expr;
 
-val bg_handler = tokenize_text "(fn";
-val en_handler = tokenize_text "| exn => Exn.reraise exn)";
-fun make_handler a = bg_handler @ a @ en_handler;
+fun make_handler range a =
+  tokenize_range_text range "(fn" @ a @
+  tokenize_range_text range "| exn => Exn.reraise exn)";
 
 fun report_special tok = (ML_Lex.pos_of tok, Markup.keyword3);
 
@@ -378,7 +379,7 @@
         let val (a, b) = ants |> chop_prefix (not o is_special_text) ||> tl in
           if is_finally s
           then ("Isabelle_Thread.try_finally", [make_expr a, make_expr b])
-          else ("Isabelle_Thread.try_catch", [make_expr a, make_handler b])
+          else ("Isabelle_Thread.try_catch", [make_expr a, make_handler (ML_Lex.range_of s) b])
         end
     | _ => error ("Too many special keywords: " ^ commas (map print_special specials)))
   end;