# HG changeset patch
# User wenzelm
# Date 1673621831 -3600
# Node ID c044306db39fcdd8c204db5f047a5a506576f547
# Parent  a8566127d43b7dee4e7ca23684b5246e0d54d732
support embedded syntax, for use with control symbols;

diff -r a8566127d43b -r c044306db39f etc/symbols
--- a/etc/symbols	Fri Jan 13 14:38:19 2023 +0100
+++ b/etc/symbols	Fri Jan 13 15:57:11 2023 +0100
@@ -506,3 +506,7 @@
 \<^if_macos>            argument: cartouche
 \<^if_windows>          argument: cartouche
 \<^if_unix>             argument: cartouche
+\<^cite>                argument: cartouche
+\<^nocite>              argument: cartouche
+\<^citet>               argument: cartouche
+\<^citep>               argument: cartouche
diff -r a8566127d43b -r c044306db39f src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Fri Jan 13 14:38:19 2023 +0100
+++ b/src/Pure/Thy/bibtex.ML	Fri Jan 13 15:57:11 2023 +0100
@@ -43,29 +43,52 @@
 val _ =
   Theory.setup (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro));
 
-fun cite_antiquotation binding get_kind =
-  Document_Output.antiquotation_raw binding
-    (Scan.lift (Scan.option Args.cartouche_input -- Parse.and_list1 Args.name_position))
-    (fn ctxt => fn (opt_loc, citations) =>
-      let
-        val loc = the_default Input.empty opt_loc;
-        val _ =
-          Context_Position.reports ctxt
-            (Document_Output.document_reports loc @
-              map (fn (name, pos) => (pos, Markup.citation name)) citations);
+
+local
+
+val parse_citations = Parse.and_list1 Args.name_position;
+
+fun cite_command ctxt get_kind (opt_loc, citations) =
+  let
+    val loc = the_default Input.empty opt_loc;
+    val _ =
+      Context_Position.reports ctxt
+        (Document_Output.document_reports loc @
+          map (fn (name, pos) => (pos, Markup.citation name)) citations);
+
+    val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt);
+    val bibtex_entries = Resources.theory_bibtex_entries thy_name;
+    val _ =
+      if null bibtex_entries andalso thy_name <> Context.PureN then ()
+      else
+        citations |> List.app (fn (name, pos) =>
+          if member (op =) bibtex_entries name orelse name = "*" then ()
+          else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
 
-        val thy_name = Context.theory_long_name (Proof_Context.theory_of ctxt);
-        val bibtex_entries = Resources.theory_bibtex_entries thy_name;
-        val _ =
-          if null bibtex_entries andalso thy_name <> Context.PureN then ()
-          else
-            citations |> List.app (fn (name, pos) =>
-              if member (op =) bibtex_entries name orelse name = "*" then ()
-              else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos));
+    val kind = get_kind ctxt;
+    val location = Document_Output.output_document ctxt {markdown = false} loc;
+  in Latex.cite {kind = kind, citations = citations, location = location} end;
+
+fun cite_command_embedded ctxt get_kind input =
+  let
+    val keywords = Keyword.no_major_keywords (Thy_Header.get_keywords' ctxt);
+    val parser = Scan.option (Parse.embedded_input --| Parse.$$$ "in") -- parse_citations;
+    val args = Parse.read_embedded ctxt keywords parser input;
+  in cite_command ctxt get_kind args end;
 
-        val kind = get_kind ctxt;
-        val location = Document_Output.output_document ctxt {markdown = false} loc;
-      in Latex.cite {kind = kind, citations = citations, location = location} end);
+fun cite_command_parser get_kind =
+  Scan.option Args.cartouche_input -- parse_citations
+    >> (fn args => fn ctxt => cite_command ctxt get_kind args) ||
+  Parse.embedded_input
+    >> (fn arg => fn ctxt => cite_command_embedded ctxt get_kind arg);
+
+in
+
+fun cite_antiquotation binding get_kind =
+  Document_Output.antiquotation_raw binding (Scan.lift (cite_command_parser get_kind))
+    (fn ctxt => fn cmd => cmd ctxt);
+
+end;
 
 val _ =
   Theory.setup