more position information, e.g. for warning about fn-pattern;
authorwenzelm
Mon, 25 Sep 2023 17:37:12 +0200
changeset 78703 55b1664b564b
parent 78702 5c40df5f0ce9
child 78704 b54aee45cabe
more position information, e.g. for warning about fn-pattern;
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;