# HG changeset patch
# User wenzelm
# Date 1674141444 -3600
# Node ID 05219e08c3e9702daf5451e8173aa5c6522449ff
# Parent  a19ea85409cdc770f700cefe4564470ac853487d
uniform keywords for embedded syntax;

diff -r a19ea85409cd -r 05219e08c3e9 src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Thu Jan 19 15:51:09 2023 +0100
+++ b/src/Pure/Thy/bibtex.ML	Thu Jan 19 16:17:24 2023 +0100
@@ -83,13 +83,16 @@
       else ();
   in cite_command ctxt get_kind (args, "") end;
 
+val cite_keywords =
+  Thy_Header.bootstrap_keywords
+  |> Keyword.add_keywords (map (fn a => ((a, Position.none), Keyword.no_spec)) ["in", "using"]);
+
 fun cite_command_embedded ctxt get_kind input =
   let
-    val keywords = Thy_Header.get_keywords' ctxt;
     val parser =
       Scan.option (Parse.embedded_input --| Parse.$$$ "in") -- parse_citations --
-        Scan.optional (Parse.command_name "using" |-- Parse.!!! Parse.name) "";
-    val args = Parse.read_embedded ctxt keywords parser input;
+        Scan.optional (Parse.$$$ "using" |-- Parse.!!! Parse.name) "";
+    val args = Parse.read_embedded ctxt cite_keywords parser input;
   in cite_command ctxt get_kind args end;
 
 fun cite_command_parser get_kind =
diff -r a19ea85409cd -r 05219e08c3e9 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Thu Jan 19 15:51:09 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Thu Jan 19 16:17:24 2023 +0100
@@ -822,7 +822,7 @@
     }
 
     object Parsers extends Parse.Parsers {
-      val keywords: Keyword.Keywords = Thy_Header.bootstrap_keywords + "in" + "and" + "using"
+      val keywords: Keyword.Keywords = Thy_Header.bootstrap_keywords + "in" + "using"
 
       val location: Parser[String] = embedded ~ $$$("in") ^^ { case x ~ _ => x } | success("")
       val citations: Parser[String] = rep1sep(name, $$$("and")) ^^ (x => x.mkString(","))