# HG changeset patch # User wenzelm # Date 1632864313 -7200 # Node ID 6edb71482de6bb40e05bc1920e25bb019aee72b0 # Parent 40804452ab6bcee50ea86ad1270ed1855448b9a3 avoid overlapping PIDE markup (amending bb25ea271b15); diff -r 40804452ab6b -r 6edb71482de6 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);