1.1 --- a/doc-src/IsarRef/Thy/document/syntax.tex	Mon Apr 28 14:41:32 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/syntax.tex	Mon Apr 28 14:42:13 2008 +0200
     1.3 @@ -294,8 +294,8 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
     1.7 -  types and terms.  Some commands such as \isa{types} (see
     1.8 -  \S\ref{sec:types-pure}) admit infixes only, while \isa{consts} (see \S\ref{sec:consts}) and \isa{syntax} (see
     1.9 +  types and terms.  Some commands such as \isa{\isacommand{types}} (see
    1.10 +  \S\ref{sec:types-pure}) admit infixes only, while \isa{\isacommand{consts}} (see \S\ref{sec:consts}) and \isa{\isacommand{syntax}} (see
    1.11    \S\ref{sec:syn-trans}) support the full range of general mixfixes
    1.12    and binders.
    1.13  
    1.14 @@ -426,7 +426,7 @@
    1.15    involving an internal dummy fact, which will be ignored later on.
    1.16    So only the effect of the attribute on the background context will
    1.17    persist.  This form of in-place declarations is particularly useful
    1.18 -  with commands like \isa{declare} and \isa{using}.
    1.19 +  with commands like \isa{\isacommand{declare}} and \isa{\isacommand{using}}.
    1.20  
    1.21    \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
    1.22    \indexouternonterm{thmdef}\indexouternonterm{thmref}
    1.23 @@ -490,8 +490,8 @@
    1.24    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.
    1.25    Isar language elements that refer to \railnonterm{vars} or
    1.26    \railnonterm{props} typically admit separate typings or namings via
    1.27 -  another level of iteration, with explicit \indexref{}{keyword}{and}\isa{and}
    1.28 -  separators; e.g.\ see \isa{fix} and \isa{assume} in
    1.29 +  another level of iteration, with explicit \indexref{}{keyword}{and}\isa{\isakeyword{and}}
    1.30 +  separators; e.g.\ see \isa{\isacommand{fix}} and \isa{\isacommand{assume}} in
    1.31    \S\ref{sec:proof-context}.%
    1.32  \end{isamarkuptext}%
    1.33  \isamarkuptrue%
    1.34 @@ -751,14 +751,14 @@
    1.35    specifically, e.g.\ to fold proof texts, or drop parts of the text
    1.36    completely.
    1.37  
    1.38 -  For example ``\isa{by}~\isa{{\isacharpercent}invisible\ auto}'' would
    1.39 +  For example ``\isa{\isacommand{by}}~\isa{{\isacharpercent}invisible\ auto}'' would
    1.40    cause that piece of proof to be treated as \isa{invisible} instead
    1.41    of \isa{proof} (the default), which may be either show or hidden
    1.42 -  depending on the document setup.  In contrast, ``\isa{by}~\isa{{\isacharpercent}visible\ auto}'' would force this text to be shown
    1.43 +  depending on the document setup.  In contrast, ``\isa{\isacommand{by}}~\isa{{\isacharpercent}visible\ auto}'' would force this text to be shown
    1.44    invariably.
    1.45  
    1.46    Explicit tag specifications within a proof apply to all subsequent
    1.47 -  commands of the same level of nesting.  For example, ``\isa{proof}~\isa{{\isacharpercent}visible\ {\isasymdots}}~\isa{qed}'' would force the
    1.48 +  commands of the same level of nesting.  For example, ``\isa{\isacommand{proof}}~\isa{{\isacharpercent}visible\ {\isasymdots}}~\isa{\isacommand{qed}}'' would force the
    1.49    whole sub-proof to be typeset as \isa{visible} (unless some of its
    1.50    parts are tagged differently).%
    1.51  \end{isamarkuptext}%

     2.1 --- a/doc-src/antiquote_setup.ML	Mon Apr 28 14:41:32 2008 +0200
     2.2 +++ b/doc-src/antiquote_setup.ML	Mon Apr 28 14:42:13 2008 +0200
     2.3 @@ -135,39 +135,40 @@
     2.4  
     2.5  val arg = enclose "{" "}" o clean_string;
     2.6  
     2.7 -fun output_entity index kind src ctxt (logic, name) =
     2.8 +fun output_entity markup index kind src ctxt (logic, name) =
     2.9    (case index of
    2.10      NONE => ""
    2.11    | SOME is_def =>
    2.12        "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name)
    2.13    ^
    2.14    (Output.output (if ! O.source then str_of_source src else name)
    2.15 +    |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
    2.16      |> (if ! O.quotes then quote else I)
    2.17      |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    2.18          else enclose "\\isa{" "}"));
    2.19  
    2.20 -fun entity index kind =
    2.21 +fun entity markup index kind =
    2.22    O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
    2.23 -    (output_entity index kind);
    2.24 +    (output_entity markup index kind);
    2.25      
    2.26 -fun entity_antiqs kind =
    2.27 - [(kind, entity NONE kind),
    2.28 -  (kind ^ "_def", entity (SOME true) kind), 
    2.29 -  (kind ^ "_ref", entity (SOME false) kind)];
    2.30 +fun entity_antiqs markup kind =
    2.31 + [(kind, entity markup NONE kind),
    2.32 +  (kind ^ "_def", entity markup (SOME true) kind), 
    2.33 +  (kind ^ "_ref", entity markup (SOME false) kind)];
    2.34  
    2.35  in
    2.36  
    2.37  val _ = O.add_commands
    2.38 - (entity_antiqs "syntax" @
    2.39 -  entity_antiqs "command" @
    2.40 -  entity_antiqs "keyword" @
    2.41 -  entity_antiqs "element" @
    2.42 -  entity_antiqs "method" @
    2.43 -  entity_antiqs "attribute" @
    2.44 -  entity_antiqs "fact" @
    2.45 -  entity_antiqs "term" @
    2.46 -  entity_antiqs "case" @
    2.47 -  entity_antiqs "antiquotation");
    2.48 + (entity_antiqs "" "syntax" @
    2.49 +  entity_antiqs "isacommand" "command" @
    2.50 +  entity_antiqs "isakeyword" "keyword" @
    2.51 +  entity_antiqs "" "element" @
    2.52 +  entity_antiqs "" "method" @
    2.53 +  entity_antiqs "" "attribute" @
    2.54 +  entity_antiqs "" "fact" @
    2.55 +  entity_antiqs "" "variable" @
    2.56 +  entity_antiqs "" "case" @
    2.57 +  entity_antiqs "" "antiquotation");
    2.58  
    2.59  end;
    2.60