--- a/src/Doc/Isar_Ref/Document_Preparation.thy Sat Aug 25 20:48:16 2018 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sat Aug 25 21:15:43 2018 +0200
@@ -94,6 +94,7 @@
@{antiquotation_def typ} & : & \<open>antiquotation\<close> \\
@{antiquotation_def type} & : & \<open>antiquotation\<close> \\
@{antiquotation_def class} & : & \<open>antiquotation\<close> \\
+ @{antiquotation_def locale} & : & \<open>antiquotation\<close> \\
@{antiquotation_def "text"} & : & \<open>antiquotation\<close> \\
@{antiquotation_def goals} & : & \<open>antiquotation\<close> \\
@{antiquotation_def subgoals} & : & \<open>antiquotation\<close> \\
@@ -180,6 +181,7 @@
@@{antiquotation typ} options @{syntax type} |
@@{antiquotation type} options @{syntax embedded} |
@@{antiquotation class} options @{syntax embedded} |
+ @@{antiquotation locale} options @{syntax embedded} |
(@@{antiquotation command} | @@{antiquotation method} | @@{antiquotation attribute})
options @{syntax name}
;
@@ -252,6 +254,8 @@
\<^descr> \<open>@{class c}\<close> prints a class \<open>c\<close>.
+ \<^descr> \<open>@{locale c}\<close> prints a locale \<open>c\<close>.
+
\<^descr> \<open>@{command name}\<close>, \<open>@{method name}\<close>, \<open>@{attribute name}\<close> print checked
entities of the Isar language.
--- a/src/Pure/Thy/document_antiquotations.ML Sat Aug 25 20:48:16 2018 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Sat Aug 25 21:15:43 2018 +0200
@@ -80,7 +80,7 @@
basic_entity \<^binding>\<open>const\<close> (Args.const {proper = true, strict = false}) pretty_const #>
basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #>
- basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.name)) pretty_locale #>
+ basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.embedded)) 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.embedded)) pretty_theory #>