# HG changeset patch
# User wenzelm
# Date 1535224543 -7200
# Node ID f6c88cb715db09ce3e14f804cc1dd4905538e4bd
# Parent  5467858e9419482a8453c7e1e70497f93becae4c
more uniform cartouche syntax;
more documentation;

diff -r 5467858e9419 -r f6c88cb715db src/Doc/Isar_Ref/Document_Preparation.thy
--- 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.
 
diff -r 5467858e9419 -r f6c88cb715db src/Pure/Thy/document_antiquotations.ML
--- 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 #>