# HG changeset patch
# User wenzelm
# Date 1726562828 -7200
# Node ID 5a75dc44623ad5371496e4c8092b189015a40a2e
# Parent  5de9c4af07134a3281635f6b2776e87f03d66e0c
tuned;

diff -r 5de9c4af0713 -r 5a75dc44623a src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Mon Sep 16 20:44:46 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Tue Sep 17 10:47:08 2024 +0200
@@ -160,7 +160,8 @@
   (case AList.lookup (op =) props name of
     NONE => default
   | SOME (s, pos) =>
-      (parse s handle Fail msg => error (msg ^ " for property " ^ quote name ^ Position.here pos)));
+      (parse s handle Fail msg =>
+        error (msg ^ " for property " ^ quote name ^ Position.here pos)));
 
 in
 
@@ -214,14 +215,12 @@
   | Brk _ => [(pos, markup_break), (pos, Markup.keyword3)]
   | En => [(pos, markup_block_end), (pos, Markup.keyword3)]);
 
-fun reports_text_of (xsym, pos) =
-  (case xsym of
-    Delim s =>
+fun reports_text_of (Delim s, pos) =
       if Position.is_reported pos andalso exists Symbol.is_utf8 (Symbol.explode s) then
         [((pos, Markup.bad ()),
           "Mixfix delimiter contains raw Unicode -- this is non-portable and unreliable")]
       else []
-  | _ => []);
+  | reports_text_of _ = [];
 
 fun read_block_properties ss =
   let