# HG changeset patch
# User ballarin
# Date 1448143327 -3600
# Node ID cb142691ef442ed83966f74d172b3730a246ec1b
# Parent  2b775b88889714b65714337ed35d3045e313e4dc
Clarify locale qualifiers: output and tutorial.

diff -r 2b775b888897 -r cb142691ef44 src/Doc/Locales/Examples3.thy
--- a/src/Doc/Locales/Examples3.thy	Sat Nov 21 20:57:24 2015 +0100
+++ b/src/Doc/Locales/Examples3.thy	Sat Nov 21 23:02:07 2015 +0100
@@ -132,18 +132,16 @@
   outputs the following:
 \begin{small}
 \begin{alltt}
-  int! : partial_order "op \(\le\)"
+  int : partial_order "op \(\le\)"
 \end{alltt}
 \end{small}
   Of course, there is only one interpretation.
-  The interpretation qualifier on the left is decorated with an
-  exclamation point.  This means that it is mandatory.  Qualifiers
-  can either be \emph{mandatory} or \emph{optional}, designated by
-  ``!'' or ``?'' respectively.  Mandatory qualifiers must occur in a
-  name reference while optional ones need not.  Mandatory qualifiers
+  The interpretation qualifier on the left is mandatory.  Qualifiers
+  can either be \emph{mandatory} or \emph{optional}.  Optional qualifiers
+  are designated by ``?''.  Mandatory qualifiers must occur in
+  name references while optional ones need not.  Mandatory qualifiers
   prevent accidental hiding of names, while optional qualifiers can be
-  more convenient to use.  For \isakeyword{interpretation}, the
-  default is ``!''.
+  more convenient to use.  The default is mandatory.
 \<close>
 
 
@@ -178,10 +176,8 @@
   We have already seen locale instances as arguments to
   \isakeyword{interpretation} in Section~\ref{sec:interpretation}.
   As before, the qualifier serves to disambiguate names from
-  different instances of the same locale.  While in
-  \isakeyword{interpretation} qualifiers default to mandatory, in
-  import and in the \isakeyword{sublocale} command, they default to
-  optional.
+  different instances of the same locale, and unless designated with a
+  ``?'' it must occur in name references.
 
   Since the parameters~@{text le} and~@{text le'} are to be partial
   orders, our locale for order preserving maps will import the these
@@ -544,7 +540,7 @@
   & \textit{name} $|$ \textit{attribute} $|$
     \textit{name} \textit{attribute} \\
   \textit{qualifier} & ::=
-  & \textit{name} [``\textbf{?}'' $|$ ``\textbf{!}''] \\[2ex]
+  & \textit{name} [``\textbf{?}''] \\[2ex]
 
   \multicolumn{3}{l}{Context Elements} \\
 
diff -r 2b775b888897 -r cb142691ef44 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Nov 21 20:57:24 2015 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Nov 21 23:02:07 2015 +0100
@@ -232,7 +232,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val morph' = morph $> export;
-    fun print_qual (qual, mandatory) = qual ^ (if mandatory then "!" else "?");
+    fun print_qual (qual, mandatory) = qual ^ (if mandatory then "" else "?");
     fun prt_quals qs = Pretty.str (space_implode "." (map print_qual qs));
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     fun prt_term' t =