# HG changeset patch
# User wenzelm
# Date 1584111867 -3600
# Node ID b0b16088ccf2f1b5843056cc15fccf498755dc88
# Parent  317e9ebbc3e1ef90c8fb992ec4d488a9f97ea623
allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);

diff -r 317e9ebbc3e1 -r b0b16088ccf2 NEWS
--- a/NEWS	Thu Mar 12 23:05:11 2020 +0100
+++ b/NEWS	Fri Mar 13 16:04:27 2020 +0100
@@ -39,6 +39,10 @@
 * The inference kernel is now confined to one main module: structure
 Thm, without the former circular dependency on structure Axclass.
 
+* Mixfix annotations may use "' " (single quote followed by space) to
+separate delimiters (as documented in the isar-ref manual), without
+requiring an auxiliary empty block.
+
 
 *** Isar ***
 
diff -r 317e9ebbc3e1 -r b0b16088ccf2 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Thu Mar 12 23:05:11 2020 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Mar 13 16:04:27 2020 +0100
@@ -243,7 +243,7 @@
 val read_block_indent =
   Bg o block_indent o #1 o Library.read_int o map Symbol_Pos.symbol;
 
-val is_meta = member (op =) ["(", ")", "/", "_", "\<index>", Symbol.open_, Symbol.close];
+val is_meta = member (op =) ["'", "(", ")", "/", "_", "\<index>", Symbol.open_, Symbol.close];
 
 val scan_delim =
   scan_one Symbol.is_control ::: Symbol_Pos.scan_cartouche "Mixfix error: " ||