more uniform syntax;
authorwenzelm
Thu, 21 Jun 2018 14:29:44 +0200
changeset 68481 fb6afa538b04
parent 68480 27be5b4cb80d
child 68482 cb84beb84ca9
more uniform syntax;
src/Doc/Isar_Ref/Document_Preparation.thy
src/Pure/Thy/document_antiquotations.ML
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Jun 21 14:17:57 2018 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Thu Jun 21 14:29:44 2018 +0200
@@ -167,7 +167,7 @@
     @{syntax_def antiquotation_body}:
       (@@{antiquotation text} | @@{antiquotation cartouche} | @@{antiquotation theory_text})
         options @{syntax text} |
-      @@{antiquotation theory} options @{syntax name} |
+      @@{antiquotation theory} options @{syntax embedded} |
       @@{antiquotation thm} options styles @{syntax thms} |
       @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
       @@{antiquotation prop} options styles @{syntax prop} |
--- a/src/Pure/Thy/document_antiquotations.ML	Thu Jun 21 14:17:57 2018 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Thu Jun 21 14:29:44 2018 +0200
@@ -82,7 +82,7 @@
   basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.name)) pretty_locale #>
   basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #>
   basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded) pretty_type #>
-  basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.name)) pretty_theory #>
+  basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.embedded)) pretty_theory #>
   basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #>
   basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
   Document_Antiquotation.setup \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms)