equal
deleted
inserted
replaced
595 \begin{figure}[t] |
595 \begin{figure}[t] |
596 \begin{graybox}\small |
596 \begin{graybox}\small |
597 \isacommand{theory}~@{text Command}\\ |
597 \isacommand{theory}~@{text Command}\\ |
598 \isacommand{imports}~@{text Main}\\ |
598 \isacommand{imports}~@{text Main}\\ |
599 \isacommand{begin}\\ |
599 \isacommand{begin}\\ |
600 \isacommand{ML}~\isa{\isacharverbatimopen}\\ |
600 \isacommand{ML}~@{text "\<verbopen>"}\\ |
601 @{ML |
601 @{ML |
602 "let |
602 "let |
603 val do_nothing = Scan.succeed (Toplevel.theory I) |
603 val do_nothing = Scan.succeed (Toplevel.theory I) |
604 val kind = OuterKeyword.thy_decl |
604 val kind = OuterKeyword.thy_decl |
605 in |
605 in |
606 OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing |
606 OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing |
607 end"}\\ |
607 end"}\\ |
608 \isa{\isacharverbatimclose}\\ |
608 @{text "\<verbclose>"}\\ |
609 \isacommand{end} |
609 \isacommand{end} |
610 \end{graybox} |
610 \end{graybox} |
611 \caption{\small The file @{text "Command.thy"} is necessary for generating a log |
611 \caption{\small The file @{text "Command.thy"} is necessary for generating a log |
612 file. This log file enables Isabelle to generate a keyword file containing |
612 file. This log file enables Isabelle to generate a keyword file containing |
613 the command \isacommand{foobar}.\label{fig:commandtheory}} |
613 the command \isacommand{foobar}.\label{fig:commandtheory}} |