proper position for semantic completion: avoid duplicate quotes;
authorwenzelm
Fri, 20 Jan 2023 21:35:49 +0100
changeset 77033 e75e2f86a6d3
parent 77032 c066335efd2e
child 77034 abd4a0f48e49
proper position for semantic completion: avoid duplicate quotes;
src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Fri Jan 20 21:28:47 2023 +0100
+++ b/src/Pure/Thy/bibtex.ML	Fri Jan 20 21:35:49 2023 +0100
@@ -76,7 +76,7 @@
 
 local
 
-val parse_citations = Parse.and_list1 Args.name_position;
+val parse_citations = Parse.and_list1 (Parse.position Parse.name);
 
 fun cite_command ctxt get_kind ((opt_loc, citations), macro_name) =
   let