avoid overlapping PIDE markup (amending bb25ea271b15);
authorwenzelm
Tue, 28 Sep 2021 23:25:13 +0200
changeset 74387 6edb71482de6
parent 74386 40804452ab6b
child 74390 23db3493478f
avoid overlapping PIDE markup (amending bb25ea271b15);
src/Pure/ML/ml_antiquotations1.ML
--- a/src/Pure/ML/ml_antiquotations1.ML	Tue Sep 28 22:50:22 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations1.ML	Tue Sep 28 23:25:13 2021 +0200
@@ -262,7 +262,7 @@
 val ml = ML_Lex.tokenize_no_range;
 val ml_range = ML_Lex.tokenize_range;
 val ml_dummy = ml "_";
-fun ml_enclose range x = ml_range range "(" @ x @ ml_range range ")";
+fun ml_enclose range x = ml "(" @ x @ ml_range range ")";
 fun ml_parens x = ml "(" @ x @ ml ")";
 fun ml_bracks x = ml "[" @ x @ ml "]";
 fun ml_commas xs = flat (separate (ml ", ") xs);