1.1 --- a/doc-src/IsarAdvanced/Codegen/style.sty	Thu Feb 26 20:41:28 2009 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/style.sty	Thu Feb 26 20:44:07 2009 +0100
     1.3 @@ -6,12 +6,6 @@
     1.4  %% references
     1.5  \newcommand{\secref}[1]{\S\ref{#1}}
     1.6  
     1.7 -%% index
     1.8 -\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
     1.9 -\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
    1.10 -\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
    1.11 -\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
    1.12 -
    1.13  %% logical markup
    1.14  \newcommand{\strong}[1]{{\bfseries {#1}}}
    1.15  \newcommand{\qn}[1]{\emph{#1}}

     2.1 --- a/doc-src/IsarAdvanced/Functions/style.sty	Thu Feb 26 20:41:28 2009 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Functions/style.sty	Thu Feb 26 20:44:07 2009 +0100
     2.3 @@ -7,12 +7,6 @@
     2.4  \newcommand{\chref}[1]{chapter~\ref{#1}}
     2.5  \newcommand{\figref}[1]{figure~\ref{#1}}
     2.6  
     2.7 -%% index
     2.8 -\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
     2.9 -\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
    2.10 -\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
    2.11 -\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
    2.12 -
    2.13  %% math
    2.14  \newcommand{\text}[1]{\mbox{#1}}
    2.15  \newcommand{\isasymvartheta}{\isamath{\theta}}

     3.1 --- a/doc-src/IsarImplementation/style.sty	Thu Feb 26 20:41:28 2009 +0100
     3.2 +++ b/doc-src/IsarImplementation/style.sty	Thu Feb 26 20:44:07 2009 +0100
     3.3 @@ -7,13 +7,6 @@
     3.4  \newcommand{\chref}[1]{chapter~\ref{#1}}
     3.5  \newcommand{\figref}[1]{figure~\ref{#1}}
     3.6  
     3.7 -%% index
     3.8 -\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
     3.9 -\newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}}
    3.10 -\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
    3.11 -\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
    3.12 -\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
    3.13 -
    3.14  %% math
    3.15  \newcommand{\text}[1]{\mbox{#1}}
    3.16  \newcommand{\isasymvartheta}{\isamath{\theta}}

     4.1 --- a/doc-src/IsarRef/style.sty	Thu Feb 26 20:41:28 2009 +0100
     4.2 +++ b/doc-src/IsarRef/style.sty	Thu Feb 26 20:44:07 2009 +0100
     4.3 @@ -15,7 +15,6 @@
     4.4  
     4.5  %% ML
     4.6  \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
     4.7 -\newcommand{\indexml}[1]{\index{#1 (ML value)|bold}}
     4.8  
     4.9  %% Isar
    4.10  \newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}

     5.1 --- a/doc-src/antiquote_setup.ML	Thu Feb 26 20:41:28 2009 +0100
     5.2 +++ b/doc-src/antiquote_setup.ML	Thu Feb 26 20:44:07 2009 +0100
     5.3 @@ -16,10 +16,11 @@
     5.4  
     5.5  val clean_string = translate
     5.6    (fn "_" => "\\_"
     5.7 +    | "#" => "\\#"
     5.8      | "<" => "$<$"
     5.9      | ">" => "$>$"
    5.10 -    | "#" => "\\#"
    5.11      | "{" => "\\{"
    5.12 +    | "|" => "$\\mid$"
    5.13      | "}" => "\\}"
    5.14      | "\\<dash>" => "-"
    5.15      | c => c);
    5.16 @@ -68,8 +69,9 @@
    5.17      val txt' = if kind = "" then txt else kind ^ " " ^ txt;
    5.18      val _ = writeln (ml (txt1, txt2));
    5.19      val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
    5.20 +    val kind' = if kind = "" then "ML" else "ML " ^ kind;
    5.21    in
    5.22 -    "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
    5.23 +    "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
    5.24      (txt'
    5.25      |> (if ! O.quotes then quote else I)
    5.26      |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"