text antiquotation for locales (similar to classes)

--- a/NEWS	Wed Jul 27 10:44:22 2016 +0200
+++ b/NEWS	Sun Jul 24 16:48:39 2016 +0200
@@ -824,6 +824,9 @@
 
 *** Document preparation ***
 
+* Text and ML antiquotation @{locale} for locales, similar to existing
+antiquotations for classes.
+
 * Commands 'paragraph' and 'subparagraph' provide additional section
 headings. Thus there are 6 levels of standard headings, as in HTML.
 

--- a/src/Pure/ML/ml_antiquotations.ML	Wed Jul 27 10:44:22 2016 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Sun Jul 24 16:48:39 2016 +0200
@@ -89,6 +89,15 @@
       ML_Syntax.print_string (Method.check_name ctxt (name, pos)))));
 
 
+(* locales *)
+
+val _ = Theory.setup
+ (ML_Antiquotation.inline @{binding locale}
+   (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
+      Locale.check (Proof_Context.theory_of ctxt) (name, pos)
+      |> ML_Syntax.print_string)));
+
+
 (* type classes *)
 
 fun class syn = Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>

--- a/src/Pure/Thy/thy_output.ML	Wed Jul 27 10:44:22 2016 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sun Jul 24 16:48:39 2016 +0200
@@ -572,6 +572,11 @@
     val ctxt' = Variable.auto_fixes eq ctxt;
   in Proof_Context.pretty_term_abbrev ctxt' eq end;
 
+fun pretty_locale ctxt (name, pos) =
+  let
+    val thy = Proof_Context.theory_of ctxt
+  in (Pretty.str o Locale.extern thy o Locale.check thy) (name, pos) end;
+
 fun pretty_class ctxt =
   Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
 
@@ -647,6 +652,7 @@
   basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
   basic_entity @{binding abbrev} (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
   basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
+  basic_entity @{binding locale} (Scan.lift (Parse.position Args.name)) pretty_locale #>
   basic_entity @{binding class} (Scan.lift Args.embedded_inner_syntax) pretty_class #>
   basic_entity @{binding type} (Scan.lift Args.embedded) pretty_type #>
   basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>