proper command/keyword markup;

--- a/doc-src/IsarRef/Thy/document/syntax.tex	Mon Apr 28 14:41:32 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/syntax.tex	Mon Apr 28 14:42:13 2008 +0200
@@ -294,8 +294,8 @@
 %
 \begin{isamarkuptext}%
 Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
-  types and terms.  Some commands such as \isa{types} (see
-  \S\ref{sec:types-pure}) admit infixes only, while \isa{consts} (see \S\ref{sec:consts}) and \isa{syntax} (see
+  types and terms.  Some commands such as \isa{\isacommand{types}} (see
+  \S\ref{sec:types-pure}) admit infixes only, while \isa{\isacommand{consts}} (see \S\ref{sec:consts}) and \isa{\isacommand{syntax}} (see
   \S\ref{sec:syn-trans}) support the full range of general mixfixes
   and binders.
 
@@ -426,7 +426,7 @@
   involving an internal dummy fact, which will be ignored later on.
   So only the effect of the attribute on the background context will
   persist.  This form of in-place declarations is particularly useful
-  with commands like \isa{declare} and \isa{using}.
+  with commands like \isa{\isacommand{declare}} and \isa{\isacommand{using}}.
 
   \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
   \indexouternonterm{thmdef}\indexouternonterm{thmref}
@@ -490,8 +490,8 @@
   the typing refers to all variables, while in \isa{a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n} the naming refers to all propositions collectively.
   Isar language elements that refer to \railnonterm{vars} or
   \railnonterm{props} typically admit separate typings or namings via
-  another level of iteration, with explicit \indexref{}{keyword}{and}\isa{and}
-  separators; e.g.\ see \isa{fix} and \isa{assume} in
+  another level of iteration, with explicit \indexref{}{keyword}{and}\isa{\isakeyword{and}}
+  separators; e.g.\ see \isa{\isacommand{fix}} and \isa{\isacommand{assume}} in
   \S\ref{sec:proof-context}.%
 \end{isamarkuptext}%
 \isamarkuptrue%
@@ -751,14 +751,14 @@
   specifically, e.g.\ to fold proof texts, or drop parts of the text
   completely.
 
-  For example ``\isa{by}~\isa{{\isacharpercent}invisible\ auto}'' would
+  For example ``\isa{\isacommand{by}}~\isa{{\isacharpercent}invisible\ auto}'' would
   cause that piece of proof to be treated as \isa{invisible} instead
   of \isa{proof} (the default), which may be either show or hidden
-  depending on the document setup.  In contrast, ``\isa{by}~\isa{{\isacharpercent}visible\ auto}'' would force this text to be shown
+  depending on the document setup.  In contrast, ``\isa{\isacommand{by}}~\isa{{\isacharpercent}visible\ auto}'' would force this text to be shown
   invariably.
 
   Explicit tag specifications within a proof apply to all subsequent
-  commands of the same level of nesting.  For example, ``\isa{proof}~\isa{{\isacharpercent}visible\ {\isasymdots}}~\isa{qed}'' would force the
+  commands of the same level of nesting.  For example, ``\isa{\isacommand{proof}}~\isa{{\isacharpercent}visible\ {\isasymdots}}~\isa{\isacommand{qed}}'' would force the
   whole sub-proof to be typeset as \isa{visible} (unless some of its
   parts are tagged differently).%
 \end{isamarkuptext}%

--- a/doc-src/antiquote_setup.ML	Mon Apr 28 14:41:32 2008 +0200
+++ b/doc-src/antiquote_setup.ML	Mon Apr 28 14:42:13 2008 +0200
@@ -135,39 +135,40 @@
 
 val arg = enclose "{" "}" o clean_string;
 
-fun output_entity index kind src ctxt (logic, name) =
+fun output_entity markup index kind src ctxt (logic, name) =
   (case index of
     NONE => ""
   | SOME is_def =>
       "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name)
   ^
   (Output.output (if ! O.source then str_of_source src else name)
+    |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
     |> (if ! O.quotes then quote else I)
     |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
         else enclose "\\isa{" "}"));
 
-fun entity index kind =
+fun entity markup index kind =
   O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
-    (output_entity index kind);
+    (output_entity markup index kind);
     
-fun entity_antiqs kind =
- [(kind, entity NONE kind),
-  (kind ^ "_def", entity (SOME true) kind), 
-  (kind ^ "_ref", entity (SOME false) kind)];
+fun entity_antiqs markup kind =
+ [(kind, entity markup NONE kind),
+  (kind ^ "_def", entity markup (SOME true) kind), 
+  (kind ^ "_ref", entity markup (SOME false) kind)];
 
 in
 
 val _ = O.add_commands
- (entity_antiqs "syntax" @
-  entity_antiqs "command" @
-  entity_antiqs "keyword" @
-  entity_antiqs "element" @
-  entity_antiqs "method" @
-  entity_antiqs "attribute" @
-  entity_antiqs "fact" @
-  entity_antiqs "term" @
-  entity_antiqs "case" @
-  entity_antiqs "antiquotation");
+ (entity_antiqs "" "syntax" @
+  entity_antiqs "isacommand" "command" @
+  entity_antiqs "isakeyword" "keyword" @
+  entity_antiqs "" "element" @
+  entity_antiqs "" "method" @
+  entity_antiqs "" "attribute" @
+  entity_antiqs "" "fact" @
+  entity_antiqs "" "variable" @
+  entity_antiqs "" "case" @
+  entity_antiqs "" "antiquotation");
 
 end;