diff --git a/src/Doc/Isar_Ref/Document_Preparation.thy b/src/Doc/Isar_Ref/Document_Preparation.thy --- a/src/Doc/Isar_Ref/Document_Preparation.thy +++ b/src/Doc/Isar_Ref/Document_Preparation.thy @@ -1,724 +1,728 @@ (*:maxLineLen=78:*) theory Document_Preparation imports Main Base begin chapter \Document preparation \label{ch:document-prep}\ text \ Isabelle/Isar provides a simple document preparation system based on {PDF-\LaTeX}, with support for hyperlinks and bookmarks within that format. This allows to produce papers, books, theses etc.\ from Isabelle theory sources. {\LaTeX} output is generated while processing a \<^emph>\session\ in batch mode, as explained in the \<^emph>\The Isabelle System Manual\ @{cite "isabelle-system"}. The main Isabelle tools to get started with document preparation are @{tool_ref mkroot} and @{tool_ref build}. The classic Isabelle/HOL tutorial @{cite "isabelle-hol-book"} also explains some aspects of theory presentation. \ section \Markup commands \label{sec:markup}\ text \ \begin{matharray}{rcl} @{command_def "chapter"} & : & \any \ any\ \\ @{command_def "section"} & : & \any \ any\ \\ @{command_def "subsection"} & : & \any \ any\ \\ @{command_def "subsubsection"} & : & \any \ any\ \\ @{command_def "paragraph"} & : & \any \ any\ \\ @{command_def "subparagraph"} & : & \any \ any\ \\ @{command_def "text"} & : & \any \ any\ \\ @{command_def "txt"} & : & \any \ any\ \\ @{command_def "text_raw"} & : & \any \ any\ \\ \end{matharray} Markup commands provide a structured way to insert text into the document generated from a theory. Each markup command takes a single @{syntax text} argument, which is passed as argument to a corresponding {\LaTeX} macro. The default macros provided by \<^file>\~~/lib/texinputs/isabelle.sty\ can be redefined according to the needs of the underlying document and {\LaTeX} styles. Note that formal comments (\secref{sec:comments}) are similar to markup commands, but have a different status within Isabelle/Isar syntax. \<^rail>\ (@@{command chapter} | @@{command section} | @@{command subsection} | @@{command subsubsection} | @@{command paragraph} | @@{command subparagraph}) @{syntax text} ';'? | (@@{command text} | @@{command txt} | @@{command text_raw}) @{syntax text} \ \<^descr> @{command chapter}, @{command section}, @{command subsection} etc.\ mark section headings within the theory source. This works in any context, even before the initial @{command theory} command. The corresponding {\LaTeX} macros are \<^verbatim>\\isamarkupchapter\, \<^verbatim>\\isamarkupsection\, \<^verbatim>\\isamarkupsubsection\ etc.\ \<^descr> @{command text} and @{command txt} specify paragraphs of plain text. This corresponds to a {\LaTeX} environment \<^verbatim>\\begin{isamarkuptext}\ \\\ \<^verbatim>\\end{isamarkuptext}\ etc. \<^descr> @{command text_raw} is similar to @{command text}, but without any surrounding markup environment. This allows to inject arbitrary {\LaTeX} source into the generated document. All text passed to any of the above markup commands may refer to formal entities via \<^emph>\document antiquotations\, see also \secref{sec:antiq}. These are interpreted in the present theory or proof context. \<^medskip> The proof markup commands closely resemble those for theory specifications, but have a different formal status and produce different {\LaTeX} macros. \ section \Document antiquotations \label{sec:antiq}\ text \ \begin{matharray}{rcl} @{antiquotation_def "theory"} & : & \antiquotation\ \\ @{antiquotation_def "thm"} & : & \antiquotation\ \\ @{antiquotation_def "lemma"} & : & \antiquotation\ \\ @{antiquotation_def "prop"} & : & \antiquotation\ \\ @{antiquotation_def "term"} & : & \antiquotation\ \\ @{antiquotation_def term_type} & : & \antiquotation\ \\ @{antiquotation_def typeof} & : & \antiquotation\ \\ @{antiquotation_def const} & : & \antiquotation\ \\ @{antiquotation_def abbrev} & : & \antiquotation\ \\ @{antiquotation_def typ} & : & \antiquotation\ \\ @{antiquotation_def type} & : & \antiquotation\ \\ @{antiquotation_def class} & : & \antiquotation\ \\ @{antiquotation_def locale} & : & \antiquotation\ \\ + @{antiquotation_def bundle} & : & \antiquotation\ \\ @{antiquotation_def "text"} & : & \antiquotation\ \\ @{antiquotation_def goals} & : & \antiquotation\ \\ @{antiquotation_def subgoals} & : & \antiquotation\ \\ @{antiquotation_def prf} & : & \antiquotation\ \\ @{antiquotation_def full_prf} & : & \antiquotation\ \\ @{antiquotation_def ML_text} & : & \antiquotation\ \\ @{antiquotation_def ML} & : & \antiquotation\ \\ @{antiquotation_def ML_def} & : & \antiquotation\ \\ @{antiquotation_def ML_ref} & : & \antiquotation\ \\ @{antiquotation_def ML_infix} & : & \antiquotation\ \\ @{antiquotation_def ML_infix_def} & : & \antiquotation\ \\ @{antiquotation_def ML_infix_ref} & : & \antiquotation\ \\ @{antiquotation_def ML_type} & : & \antiquotation\ \\ @{antiquotation_def ML_type_def} & : & \antiquotation\ \\ @{antiquotation_def ML_type_ref} & : & \antiquotation\ \\ @{antiquotation_def ML_structure} & : & \antiquotation\ \\ @{antiquotation_def ML_structure_def} & : & \antiquotation\ \\ @{antiquotation_def ML_structure_ref} & : & \antiquotation\ \\ @{antiquotation_def ML_functor} & : & \antiquotation\ \\ @{antiquotation_def ML_functor_def} & : & \antiquotation\ \\ @{antiquotation_def ML_functor_ref} & : & \antiquotation\ \\ @{antiquotation_def emph} & : & \antiquotation\ \\ @{antiquotation_def bold} & : & \antiquotation\ \\ @{antiquotation_def verbatim} & : & \antiquotation\ \\ @{antiquotation_def bash_function} & : & \antiquotation\ \\ @{antiquotation_def system_option} & : & \antiquotation\ \\ @{antiquotation_def session} & : & \antiquotation\ \\ @{antiquotation_def "file"} & : & \antiquotation\ \\ @{antiquotation_def "url"} & : & \antiquotation\ \\ @{antiquotation_def "cite"} & : & \antiquotation\ \\ @{command_def "print_antiquotations"}\\<^sup>*\ & : & \context \\ \\ \end{matharray} The overall content of an Isabelle/Isar theory may alternate between formal and informal text. The main body consists of formal specification and proof commands, interspersed with markup commands (\secref{sec:markup}) or document comments (\secref{sec:comments}). The argument of markup commands quotes informal text to be printed in the resulting document, but may again refer to formal entities via \<^emph>\document antiquotations\. For example, embedding \<^verbatim>\@{term [show_types] "f x = a + x"}\ within a text block makes \isa{{\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharplus}\ x} appear in the final {\LaTeX} document. Antiquotations usually spare the author tedious typing of logical entities in full detail. Even more importantly, some degree of consistency-checking between the main body of formal text and its informal explanation is achieved, since terms and types appearing in antiquotations are checked within the current theory or proof context. \<^medskip> Antiquotations are in general written as \<^verbatim>\@{\\name\~\<^verbatim>\[\\options\\<^verbatim>\]\~\arguments\\<^verbatim>\}\. The short form \<^verbatim>\\\\<^verbatim>\<^\\name\\<^verbatim>\>\\\argument_content\\ (without surrounding \<^verbatim>\@{\\\\\<^verbatim>\}\) works for a single argument that is a cartouche. A cartouche without special decoration is equivalent to \<^verbatim>\\<^cartouche>\\\argument_content\\, which is equivalent to \<^verbatim>\@{cartouche\~\\argument_content\\\<^verbatim>\}\. The special name @{antiquotation_def cartouche} is defined in the context: Isabelle/Pure introduces that as an alias to @{antiquotation_ref text} (see below). Consequently, \\foo_bar + baz \ bazar\\ prints literal quasi-formal text (unchecked). A control symbol \<^verbatim>\\\\<^verbatim>\<^\\name\\<^verbatim>\>\ within the body text, but without a subsequent cartouche, is equivalent to \<^verbatim>\@{\\name\\<^verbatim>\}\. \begingroup \def\isasymcontrolstart{\isatt{\isacharbackslash\isacharless\isacharcircum}} \<^rail>\ @{syntax_def antiquotation}: '@{' antiquotation_body '}' | '\' @{syntax_ref name} '>' @{syntax_ref cartouche} | @{syntax_ref cartouche} ; options: '[' (option * ',') ']' ; option: @{syntax name} | @{syntax name} '=' @{syntax name} ; \ \endgroup Note that the syntax of antiquotations may \<^emph>\not\ include source comments \<^verbatim>\(*\~\\\~\<^verbatim>\*)\ nor verbatim text \<^verbatim>\{*\~\\\~\<^verbatim>\*}\. %% FIXME less monolithic presentation, move to individual sections!? \<^rail>\ @{syntax_def antiquotation_body}: (@@{antiquotation text} | @@{antiquotation cartouche} | @@{antiquotation theory_text}) options @{syntax text} | @@{antiquotation theory} options @{syntax embedded} | @@{antiquotation thm} options styles @{syntax thms} | @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? | @@{antiquotation prop} options styles @{syntax prop} | @@{antiquotation term} options styles @{syntax term} | @@{antiquotation (HOL) value} options styles @{syntax term} | @@{antiquotation term_type} options styles @{syntax term} | @@{antiquotation typeof} options styles @{syntax term} | @@{antiquotation const} options @{syntax term} | @@{antiquotation abbrev} options @{syntax term} | @@{antiquotation typ} options @{syntax type} | @@{antiquotation type} options @{syntax embedded} | @@{antiquotation class} options @{syntax embedded} | @@{antiquotation locale} options @{syntax embedded} | + @@{antiquotation bundle} options @{syntax embedded} | (@@{antiquotation command} | @@{antiquotation method} | @@{antiquotation attribute}) options @{syntax name} ; @{syntax antiquotation}: @@{antiquotation goals} options | @@{antiquotation subgoals} options | @@{antiquotation prf} options @{syntax thms} | @@{antiquotation full_prf} options @{syntax thms} | @@{antiquotation ML_text} options @{syntax text} | @@{antiquotation ML} options @{syntax text} | @@{antiquotation ML_infix} options @{syntax text} | @@{antiquotation ML_type} options @{syntax typeargs} @{syntax text} | @@{antiquotation ML_structure} options @{syntax text} | @@{antiquotation ML_functor} options @{syntax text} | @@{antiquotation emph} options @{syntax text} | @@{antiquotation bold} options @{syntax text} | @@{antiquotation verbatim} options @{syntax text} | @@{antiquotation bash_function} options @{syntax embedded} | @@{antiquotation system_option} options @{syntax embedded} | @@{antiquotation session} options @{syntax embedded} | @@{antiquotation path} options @{syntax embedded} | @@{antiquotation "file"} options @{syntax name} | @@{antiquotation dir} options @{syntax name} | @@{antiquotation url} options @{syntax embedded} | @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and') ; styles: '(' (style + ',') ')' ; style: (@{syntax name} +) ; @@{command print_antiquotations} ('!'?) \ \<^descr> \@{text s}\ prints uninterpreted source text \s\, i.e.\ inner syntax. This is particularly useful to print portions of text according to the Isabelle document style, without demanding well-formedness, e.g.\ small pieces of terms that should not be parsed or type-checked yet. It is also possible to write this in the short form \\s\\ without any further decoration. \<^descr> \@{theory_text s}\ prints uninterpreted theory source text \s\, i.e.\ outer syntax with command keywords and other tokens. \<^descr> \@{theory A}\ prints the session-qualified theory name \A\, which is guaranteed to refer to a valid ancestor theory in the current context. \<^descr> \@{thm a\<^sub>1 \ a\<^sub>n}\ prints theorems \a\<^sub>1 \ a\<^sub>n\. Full fact expressions are allowed here, including attributes (\secref{sec:syn-att}). \<^descr> \@{prop \}\ prints a well-typed proposition \\\. \<^descr> \@{lemma \ by m}\ proves a well-typed proposition \\\ by method \m\ and prints the original \\\. \<^descr> \@{term t}\ prints a well-typed term \t\. \<^descr> \@{value t}\ evaluates a term \t\ and prints its result, see also @{command_ref (HOL) value}. \<^descr> \@{term_type t}\ prints a well-typed term \t\ annotated with its type. \<^descr> \@{typeof t}\ prints the type of a well-typed term \t\. \<^descr> \@{const c}\ prints a logical or syntactic constant \c\. \<^descr> \@{abbrev c x\<^sub>1 \ x\<^sub>n}\ prints a constant abbreviation \c x\<^sub>1 \ x\<^sub>n \ rhs\ as defined in the current context. \<^descr> \@{typ \}\ prints a well-formed type \\\. \<^descr> \@{type \}\ prints a (logical or syntactic) type constructor \\\. \<^descr> \@{class c}\ prints a class \c\. \<^descr> \@{locale c}\ prints a locale \c\. + \<^descr> \@{bundle c}\ prints a bundle \c\. + \<^descr> \@{command name}\, \@{method name}\, \@{attribute name}\ print checked entities of the Isar language. \<^descr> \@{goals}\ prints the current \<^emph>\dynamic\ goal state. This is mainly for support of tactic-emulation scripts within Isar. Presentation of goal states does not conform to the idea of human-readable proof documents! When explaining proofs in detail it is usually better to spell out the reasoning via proper Isar proof commands, instead of peeking at the internal machine configuration. \<^descr> \@{subgoals}\ is similar to \@{goals}\, but does not print the main goal. \<^descr> \@{prf a\<^sub>1 \ a\<^sub>n}\ prints the (compact) proof terms corresponding to the theorems \a\<^sub>1 \ a\<^sub>n\. Note that this requires proof terms to be switched on for the current logic session. \<^descr> \@{full_prf a\<^sub>1 \ a\<^sub>n}\ is like \@{prf a\<^sub>1 \ a\<^sub>n}\, but prints the full proof terms, i.e.\ also displays information omitted in the compact proof term, which is denoted by ``\_\'' placeholders there. \<^descr> \@{ML_text s}\ prints ML text verbatim: only the token language is checked. \<^descr> \@{ML s}\, \@{ML_infix s}\, \@{ML_type s}\, \@{ML_structure s}\, and \@{ML_functor s}\ check text \s\ as ML value, infix operator, type, exception, structure, and functor respectively. The source is printed verbatim. The variants \@{ML_def s}\ and \@{ML_ref s}\ etc. maintain the document index: ``def'' means to make a bold entry, ``ref'' means to make a regular entry. There are two forms for type constructors, with or without separate type arguments: this impacts only the index entry. For example, \@{ML_type_ref \'a list\}\ makes an entry literally for ``\'a list\'' (sorted under the letter ``a''), but \@{ML_type_ref 'a \list\}\ makes an entry for the constructor name ``\list\''. \<^descr> \@{emph s}\ prints document source recursively, with {\LaTeX} markup \<^verbatim>\\emph{\\\\\<^verbatim>\}\. \<^descr> \@{bold s}\ prints document source recursively, with {\LaTeX} markup \<^verbatim>\\textbf{\\\\\<^verbatim>\}\. \<^descr> \@{verbatim s}\ prints uninterpreted source text literally as ASCII characters, using some type-writer font style. \<^descr> \@{bash_function name}\ prints the given GNU bash function verbatim. The name is checked wrt.\ the Isabelle system environment @{cite "isabelle-system"}. \<^descr> \@{system_option name}\ prints the given system option verbatim. The name is checked wrt.\ cumulative \<^verbatim>\etc/options\ of all Isabelle components, notably \<^file>\~~/etc/options\. \<^descr> \@{session name}\ prints given session name verbatim. The name is checked wrt.\ the dependencies of the current session. \<^descr> \@{path name}\ prints the file-system path name verbatim. \<^descr> \@{file name}\ is like \@{path name}\, but ensures that \name\ refers to a plain file. \<^descr> \@{dir name}\ is like \@{path name}\, but ensures that \name\ refers to a directory. \<^descr> \@{url name}\ produces markup for the given URL, which results in an active hyperlink within the text. \<^descr> \@{cite name}\ produces a citation \<^verbatim>\\cite{name}\ in {\LaTeX}, where the name refers to some Bib{\TeX} database entry. This is only checked in batch-mode session builds. The variant \@{cite \opt\ name}\ produces \<^verbatim>\\cite[opt]{name}\ with some free-form optional argument. Multiple names are output with commas, e.g. \@{cite foo \ bar}\ becomes \<^verbatim>\\cite{foo,bar}\. The {\LaTeX} macro name is determined by the antiquotation option @{antiquotation_option_def cite_macro}, or the configuration option @{attribute cite_macro} in the context. For example, \@{cite [cite_macro = nocite] foobar}\ produces \<^verbatim>\\nocite{foobar}\. \<^descr> @{command "print_antiquotations"} prints all document antiquotations that are defined in the current context; the ``\!\'' option indicates extra verbosity. \ subsection \Styled antiquotations\ text \ The antiquotations \thm\, \prop\ and \term\ admit an extra \<^emph>\style\ specification to modify the printed result. A style is specified by a name with a possibly empty number of arguments; multiple styles can be sequenced with commas. The following standard styles are available: \<^descr> \lhs\ extracts the first argument of any application form with at least two arguments --- typically meta-level or object-level equality, or any other binary relation. \<^descr> \rhs\ is like \lhs\, but extracts the second argument. \<^descr> \concl\ extracts the conclusion \C\ from a rule in Horn-clause normal form \A\<^sub>1 \ \ A\<^sub>n \ C\. \<^descr> \prem\ \n\ extract premise number \n\ from from a rule in Horn-clause normal form \A\<^sub>1 \ \ A\<^sub>n \ C\. \ subsection \General options\ text \ The following options are available to tune the printed output of antiquotations. Note that many of these coincide with system and configuration options of the same names. \<^descr> @{antiquotation_option_def show_types}~\= bool\ and @{antiquotation_option_def show_sorts}~\= bool\ control printing of explicit type and sort constraints. \<^descr> @{antiquotation_option_def show_structs}~\= bool\ controls printing of implicit structures. \<^descr> @{antiquotation_option_def show_abbrevs}~\= bool\ controls folding of abbreviations. \<^descr> @{antiquotation_option_def names_long}~\= bool\ forces names of types and constants etc.\ to be printed in their fully qualified internal form. \<^descr> @{antiquotation_option_def names_short}~\= bool\ forces names of types and constants etc.\ to be printed unqualified. Note that internalizing the output again in the current context may well yield a different result. \<^descr> @{antiquotation_option_def names_unique}~\= bool\ determines whether the printed version of qualified names should be made sufficiently long to avoid overlap with names declared further back. Set to \false\ for more concise output. \<^descr> @{antiquotation_option_def eta_contract}~\= bool\ prints terms in \\\-contracted form. \<^descr> @{antiquotation_option_def display}~\= bool\ indicates if the text is to be output as multi-line ``display material'', rather than a small piece of text without line breaks (which is the default). In this mode the embedded entities are printed in the same style as the main theory text. \<^descr> @{antiquotation_option_def break}~\= bool\ controls line breaks in non-display material. \<^descr> @{antiquotation_option_def cartouche}~\= bool\ indicates if the output should be delimited as cartouche. \<^descr> @{antiquotation_option_def quotes}~\= bool\ indicates if the output should be delimited via double quotes (option @{antiquotation_option cartouche} takes precedence). Note that the Isabelle {\LaTeX} styles may suppress quotes on their own account. \<^descr> @{antiquotation_option_def mode}~\= name\ adds \name\ to the print mode to be used for presentation. Note that the standard setup for {\LaTeX} output is already present by default, with mode ``\latex\''. \<^descr> @{antiquotation_option_def margin}~\= nat\ and @{antiquotation_option_def indent}~\= nat\ change the margin or indentation for pretty printing of display material. \<^descr> @{antiquotation_option_def goals_limit}~\= nat\ determines the maximum number of subgoals to be printed (for goal-based antiquotation). \<^descr> @{antiquotation_option_def source}~\= bool\ prints the original source text of the antiquotation arguments, rather than its internal representation. Note that formal checking of @{antiquotation "thm"}, @{antiquotation "term"}, etc. is still enabled; use the @{antiquotation "text"} antiquotation for unchecked output. Regular \term\ and \typ\ antiquotations with \source = false\ involve a full round-trip from the original source to an internalized logical entity back to a source form, according to the syntax of the current context. Thus the printed output is not under direct control of the author, it may even fluctuate a bit as the underlying theory is changed later on. In contrast, @{antiquotation_option source}~\= true\ admits direct printing of the given source text, with the desirable well-formedness check in the background, but without modification of the printed text. Cartouche delimiters of the argument are stripped for antiquotations that are internally categorized as ``embedded''. \<^descr> @{antiquotation_option_def source_cartouche} is like @{antiquotation_option source}, but cartouche delimiters are always preserved in the output. For Boolean flags, ``\name = true\'' may be abbreviated as ``\name\''. All of the above flags are disabled by default, unless changed specifically for a logic session in the corresponding \<^verbatim>\ROOT\ file. \ section \Markdown-like text structure\ text \ The markup commands @{command_ref text}, @{command_ref txt}, @{command_ref text_raw} (\secref{sec:markup}) consist of plain text. Its internal structure consists of paragraphs and (nested) lists, using special Isabelle symbols and some rules for indentation and blank lines. This quasi-visual format resembles \<^emph>\Markdown\\<^footnote>\\<^url>\http://commonmark.org\\, but the full complexity of that notation is avoided. This is a summary of the main principles of minimal Markdown in Isabelle: \<^item> List items start with the following markers \<^descr>[itemize:] \<^verbatim>\\<^item>\ \<^descr>[enumerate:] \<^verbatim>\\<^enum>\ \<^descr>[description:] \<^verbatim>\\<^descr>\ \<^item> Adjacent list items with same indentation and same marker are grouped into a single list. \<^item> Singleton blank lines separate paragraphs. \<^item> Multiple blank lines escape from the current list hierarchy. Notable differences to official Markdown: \<^item> Indentation of list items needs to match exactly. \<^item> Indentation is unlimited (official Markdown interprets four spaces as block quote). \<^item> List items always consist of paragraphs --- there is no notion of ``tight'' list. \<^item> Section headings are expressed via Isar document markup commands (\secref{sec:markup}). \<^item> URLs, font styles, other special content is expressed via antiquotations (\secref{sec:antiq}), usually with proper nesting of sub-languages via text cartouches. \ section \Document markers and command tags \label{sec:document-markers}\ text \ \emph{Document markers} are formal comments of the form \\<^marker>\marker_body\\ (using the control symbol \<^verbatim>\\<^marker>\) and may occur anywhere within the outer syntax of a command: the inner syntax of a marker body resembles that for attributes (\secref{sec:syn-att}). In contrast, \emph{Command tags} may only occur after a command keyword and are treated as special markers as explained below. \<^rail>\ @{syntax_def marker}: '\<^marker>' @{syntax cartouche} ; @{syntax_def marker_body}: (@{syntax name} @{syntax args} * ',') ; @{syntax_def tags}: tag* ; tag: '%' (@{syntax short_ident} | @{syntax string}) \ Document markers are stripped from the document output, but surrounding white-space is preserved: e.g.\ a marker at the end of a line does not affect the subsequent line break. Markers operate within the semantic presentation context of a command, and may modify it to change the overall appearance of a command span (e.g.\ by adding tags). Each document marker has its own syntax defined in the theory context; the following markers are predefined in Isabelle/Pure: \<^rail>\ (@@{document_marker_def title} | @@{document_marker_def creator} | @@{document_marker_def contributor} | @@{document_marker_def date} | @@{document_marker_def license} | @@{document_marker_def description}) @{syntax embedded} ; @@{document_marker_def tag} (scope?) @{syntax name} ; scope: '(' ('proof' | 'command') ')' \ \<^descr> \\<^marker>\title arg\\, \\<^marker>\creator arg\\, \\<^marker>\contributor arg\\, \\<^marker>\date arg\\, \\<^marker>\license arg\\, and \\<^marker>\description arg\\ produce markup in the PIDE document, without any immediate effect on typesetting. This vocabulary is taken from the Dublin Core Metadata Initiative\<^footnote>\\<^url>\https://www.dublincore.org/specifications/dublin-core/dcmi-terms\\. The argument is an uninterpreted string, except for @{document_marker description}, which consists of words that are subject to spell-checking. \<^descr> \\<^marker>\tag name\\ updates the list of command tags in the presentation context: later declarations take precedence, so \\<^marker>\tag a, tag b, tag c\\ produces a reversed list. The default tags are given by the original \<^theory_text>\keywords\ declaration of a command, and the system option @{system_option_ref document_tags}. The optional \scope\ tells how far the tagging is applied to subsequent proof structure: ``\<^theory_text>\("proof")\'' means it applies to the following proof text, and ``\<^theory_text>\(command)\'' means it only applies to the current command. The default within a proof body is ``\<^theory_text>\("proof")\'', but for toplevel goal statements it is ``\<^theory_text>\(command)\''. Thus a \tag\ marker for \<^theory_text>\theorem\, \<^theory_text>\lemma\ etc. does \emph{not} affect its proof by default. An old-style command tag \<^verbatim>\%\\name\ is treated like a document marker \\<^marker>\tag (proof) name\\: the list of command tags precedes the list of document markers. The head of the resulting tags in the presentation context is turned into {\LaTeX} environments to modify the type-setting. The following tags are pre-declared for certain classes of commands, and serve as default markup for certain kinds of commands: \<^medskip> \begin{tabular}{ll} \document\ & document markup commands \\ \theory\ & theory begin/end \\ \proof\ & all proof commands \\ \ML\ & all commands involving ML code \\ \end{tabular} \<^medskip> The Isabelle document preparation system @{cite "isabelle-system"} allows tagged command regions to be presented specifically, e.g.\ to fold proof texts, or drop parts of the text completely. For example ``\<^theory_text>\by auto\~\\<^marker>\tag invisible\\'' causes that piece of proof to be treated as \invisible\ instead of \proof\ (the default), which may be shown or hidden depending on the document setup. In contrast, ``\<^theory_text>\by auto\~\\<^marker>\tag visible\\'' forces 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, ``\<^theory_text>\proof\~\\<^marker>\tag invisible\ \\~\<^theory_text>\qed\'' forces the whole sub-proof to be typeset as \visible\ (unless some of its parts are tagged differently). \<^medskip> Command tags merely produce certain markup environments for type-setting. The meaning of these is determined by {\LaTeX} macros, as defined in \<^file>\~~/lib/texinputs/isabelle.sty\ or by the document author. The Isabelle document preparation tools also provide some high-level options to specify the meaning of arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding parts of the text. Logic sessions may also specify ``document versions'', where given tags are interpreted in some particular way. Again see @{cite "isabelle-system"} for further details. \ section \Railroad diagrams\ text \ \begin{matharray}{rcl} @{antiquotation_def "rail"} & : & \antiquotation\ \\ \end{matharray} \<^rail>\ 'rail' @{syntax text} \ The @{antiquotation rail} antiquotation allows to include syntax diagrams into Isabelle documents. {\LaTeX} requires the style file \<^file>\~~/lib/texinputs/railsetup.sty\, which can be used via \<^verbatim>\\usepackage{railsetup}\ in \<^verbatim>\root.tex\, for example. The rail specification language is quoted here as Isabelle @{syntax string} or text @{syntax "cartouche"}; it has its own grammar given below. \begingroup \def\isasymnewline{\isatt{\isacharbackslash\isacharless newline\isachargreater}} \<^rail>\ rule? + ';' ; rule: ((identifier | @{syntax antiquotation}) ':')? body ; body: concatenation + '|' ; concatenation: ((atom '?'?) +) (('*' | '+') atom?)? ; atom: '(' body? ')' | identifier | '@'? (string | @{syntax antiquotation}) | '\' \ \endgroup The lexical syntax of \identifier\ coincides with that of @{syntax short_ident} in regular Isabelle syntax, but \string\ uses single quotes instead of double quotes of the standard @{syntax string} category. Each \rule\ defines a formal language (with optional name), using a notation that is similar to EBNF or regular expressions with recursion. The meaning and visual appearance of these rail language elements is illustrated by the following representative examples. \<^item> Empty \<^verbatim>\()\ \<^rail>\()\ \<^item> Nonterminal \<^verbatim>\A\ \<^rail>\A\ \<^item> Nonterminal via Isabelle antiquotation \<^verbatim>\@{syntax method}\ \<^rail>\@{syntax method}\ \<^item> Terminal \<^verbatim>\'xyz'\ \<^rail>\'xyz'\ \<^item> Terminal in keyword style \<^verbatim>\@'xyz'\ \<^rail>\@'xyz'\ \<^item> Terminal via Isabelle antiquotation \<^verbatim>\@@{method rule}\ \<^rail>\@@{method rule}\ \<^item> Concatenation \<^verbatim>\A B C\ \<^rail>\A B C\ \<^item> Newline inside concatenation \<^verbatim>\A B C \ D E F\ \<^rail>\A B C \ D E F\ \<^item> Variants \<^verbatim>\A | B | C\ \<^rail>\A | B | C\ \<^item> Option \<^verbatim>\A ?\ \<^rail>\A ?\ \<^item> Repetition \<^verbatim>\A *\ \<^rail>\A *\ \<^item> Repetition with separator \<^verbatim>\A * sep\ \<^rail>\A * sep\ \<^item> Strict repetition \<^verbatim>\A +\ \<^rail>\A +\ \<^item> Strict repetition with separator \<^verbatim>\A + sep\ \<^rail>\A + sep\ \ end diff --git a/src/Pure/Isar/bundle.ML b/src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML +++ b/src/Pure/Isar/bundle.ML @@ -1,232 +1,235 @@ (* Title: Pure/Isar/bundle.ML Author: Makarius Bundled declarations (notes etc.). *) signature BUNDLE = sig type name = string val check: Proof.context -> xstring * Position.T -> string val get: Proof.context -> name -> Attrib.thms val read: Proof.context -> xstring * Position.T -> Attrib.thms + val extern: Proof.context -> string -> xstring val print_bundles: bool -> Proof.context -> unit val bundle: binding * Attrib.thms -> (binding * typ option * mixfix) list -> local_theory -> local_theory val bundle_cmd: binding * (Facts.ref * Token.src list) list -> (binding * string option * mixfix) list -> local_theory -> local_theory val init: binding -> theory -> local_theory val unbundle: name list -> local_theory -> local_theory val unbundle_cmd: (xstring * Position.T) list -> local_theory -> local_theory val includes: name list -> Proof.context -> Proof.context val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context val include_: name list -> Proof.state -> Proof.state val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state val including: name list -> Proof.state -> Proof.state val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state end; structure Bundle: BUNDLE = struct (** context data **) structure Data = Generic_Data ( type T = Attrib.thms Name_Space.table * Attrib.thms option; val empty : T = (Name_Space.empty_table "bundle", NONE); val extend = I; fun merge ((tab1, target1), (tab2, target2)) = (Name_Space.merge_tables (tab1, tab2), merge_options (target1, target2)); ); (* bundles *) type name = string val get_all_generic = #1 o Data.get; val get_all = get_all_generic o Context.Proof; fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_all ctxt); val get = Name_Space.get o get_all_generic o Context.Proof; fun read ctxt = get ctxt o check ctxt; +fun extern ctxt = Name_Space.extern ctxt (Name_Space.space_of_table (get_all ctxt)); + fun define_bundle (b, bundle) context = let val bundle' = Attrib.trim_context_thms bundle; val (name, bundles') = Name_Space.define context true (b, bundle') (get_all_generic context); val context' = (Data.map o apfst o K) bundles' context; in (name, context') end; (* target -- bundle under construction *) fun the_target thy = (case #2 (Data.get (Context.Theory thy)) of SOME thms => thms | NONE => error "Missing bundle target"); val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE; val set_target = Context.theory_map o Data.map o apsnd o K o SOME o Attrib.trim_context_thms; fun augment_target thms = Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy); (* print bundles *) fun pretty_bundle ctxt (markup_name, bundle) = let val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt; fun prt_thm_attribs atts th = Pretty.block (Pretty.breaks (prt_thm th :: Attrib.pretty_attribs ctxt atts)); fun prt_thms (ths, []) = map prt_thm ths | prt_thms (ths, atts) = map (prt_thm_attribs atts) ths; in Pretty.block ([Pretty.keyword1 "bundle", Pretty.str " ", Pretty.mark_str markup_name] @ (if null bundle then [] else Pretty.fbreaks (Pretty.str " =" :: maps prt_thms bundle))) end; fun print_bundles verbose ctxt = Pretty.writeln_chunks (map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_all ctxt))); (** define bundle **) fun transform_bundle phi = map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts)); (* command *) local fun gen_bundle prep_fact prep_att add_fixes (binding, raw_bundle) raw_fixes lthy = let val (_, ctxt') = add_fixes raw_fixes lthy; val bundle0 = raw_bundle |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts)); val bundle = Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)] |> map snd |> flat |> transform_bundle (Proof_Context.export_morphism ctxt' lthy); in lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => #2 o define_bundle (Morphism.binding phi binding, transform_bundle phi bundle)) end; in val bundle = gen_bundle (K I) (K I) Proof_Context.add_fixes; val bundle_cmd = gen_bundle Proof_Context.get_fact Attrib.check_src Proof_Context.add_fixes_cmd; end; (* target *) local fun bad_operation _ = error "Not possible in bundle target"; fun conclude invisible binding = Local_Theory.background_theory_result (fn thy => thy |> invisible ? Context_Position.set_visible_global false |> Context.Theory |> define_bundle (binding, the_target thy) ||> (Context.the_theory #> invisible ? Context_Position.restore_visible_global thy #> reset_target)); fun pretty binding lthy = let val bundle = the_target (Proof_Context.theory_of lthy); val (name, lthy') = lthy |> Local_Theory.raw_theory (Context_Position.set_visible_global false) |> conclude true binding; val thy_ctxt' = Proof_Context.init_global (Proof_Context.theory_of lthy'); val markup_name = Name_Space.markup_extern thy_ctxt' (Name_Space.space_of_table (get_all thy_ctxt')) name; in [pretty_bundle lthy' (markup_name, bundle)] end; fun bundle_notes kind facts lthy = let val bundle = facts |> maps (fn ((_, more_atts), thms) => map (fn (ths, atts) => (ths, atts @ more_atts)) thms); in lthy |> augment_target (transform_bundle (Local_Theory.standard_morphism_theory lthy) bundle) |> Generic_Target.standard_notes (op <>) kind facts |> Attrib.local_notes kind facts end; fun bundle_declaration decl lthy = lthy |> (augment_target o Attrib.internal_declaration) (Morphism.transform (Local_Theory.standard_morphism_theory lthy) decl) |> Generic_Target.standard_declaration (K true) decl; in fun init binding thy = thy |> Local_Theory.init {background_naming = Sign.naming_of thy, setup = set_target [] #> Proof_Context.init_global, conclude = conclude false binding #> #2} {define = bad_operation, notes = bundle_notes, abbrev = bad_operation, declaration = K bundle_declaration, theory_registration = bad_operation, locale_dependency = bad_operation, pretty = pretty binding} end; (** activate bundles **) local fun gen_activate notes prep_bundle args ctxt = let val decls = maps (prep_bundle ctxt) args in ctxt |> Context_Position.set_visible false |> notes [(Binding.empty_atts, decls)] |> #2 |> Context_Position.restore_visible ctxt end; fun gen_unbundle prep_bundle = gen_activate Local_Theory.notes prep_bundle; fun gen_includes prep_bundle = gen_activate (Attrib.local_notes "") prep_bundle; fun gen_include prep_bundle bs = Proof.assert_forward #> Proof.map_context (gen_includes prep_bundle bs) #> Proof.reset_facts; fun gen_including prep_bundle bs = Proof.assert_backward #> Proof.map_context (gen_includes prep_bundle bs) in val unbundle = gen_unbundle get; val unbundle_cmd = gen_unbundle read; val includes = gen_includes get; val includes_cmd = gen_includes read; val include_ = gen_include get; val include_cmd = gen_include read; val including = gen_including get; val including_cmd = gen_including read; end; end; diff --git a/src/Pure/Thy/document_antiquotations.ML b/src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML +++ b/src/Pure/Thy/document_antiquotations.ML @@ -1,447 +1,451 @@ (* Title: Pure/Thy/document_antiquotations.ML Author: Makarius Miscellaneous document antiquotations. *) structure Document_Antiquotations: sig end = struct (* basic entities *) local type style = term -> term; fun pretty_term_style ctxt (style: style, t) = Document_Output.pretty_term ctxt (style t); fun pretty_thms_style ctxt (style: style, ths) = map (fn th => Document_Output.pretty_term ctxt (style (Thm.full_prop_of th))) ths; fun pretty_term_typ ctxt (style: style, t) = let val t' = style t in Document_Output.pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end; fun pretty_term_typeof ctxt (style: style, t) = Syntax.pretty_typ ctxt (Term.fastype_of (style t)); fun pretty_const ctxt c = let val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c) handle TYPE (msg, _, _) => error msg; val (t', _) = yield_singleton (Variable.import_terms true) t ctxt; in Document_Output.pretty_term ctxt t' end; fun pretty_abbrev ctxt s = let val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s; fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t); val (head, args) = Term.strip_comb t; val (c, T) = Term.dest_Const head handle TERM _ => err (); val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c handle TYPE _ => err (); val t' = Term.betapplys (Envir.expand_atom T (U, u), args); val eq = Logic.mk_equals (t, t'); val ctxt' = Proof_Context.augment eq ctxt; in Proof_Context.pretty_term_abbrev ctxt' eq end; fun pretty_locale ctxt (name, pos) = let val thy = Proof_Context.theory_of ctxt in Pretty.str (Locale.extern thy (Locale.check thy (name, pos))) end; +fun pretty_bundle ctxt (name, pos) = + Pretty.str (Bundle.extern ctxt (Bundle.check ctxt (name, pos))); + fun pretty_class ctxt s = Pretty.str (Proof_Context.extern_class ctxt (Proof_Context.read_class ctxt s)); fun pretty_type ctxt s = let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s in Pretty.str (Proof_Context.extern_type ctxt name) end; fun pretty_prf full ctxt = Proof_Syntax.pretty_standard_proof_of ctxt full; fun pretty_theory ctxt (name, pos) = (Theory.check {long = true} ctxt (name, pos); Pretty.str name); val basic_entity = Document_Output.antiquotation_pretty_source_embedded; fun basic_entities name scan pretty = Document_Antiquotation.setup name scan (fn {context = ctxt, source = src, argument = xs} => Document_Output.pretty_items_source ctxt {embedded = false} src (map (pretty ctxt) xs)); val _ = Theory.setup (basic_entity \<^binding>\prop\ (Term_Style.parse -- Args.prop) pretty_term_style #> basic_entity \<^binding>\term\ (Term_Style.parse -- Args.term) pretty_term_style #> basic_entity \<^binding>\term_type\ (Term_Style.parse -- Args.term) pretty_term_typ #> basic_entity \<^binding>\typeof\ (Term_Style.parse -- Args.term) pretty_term_typeof #> basic_entity \<^binding>\const\ (Args.const {proper = true, strict = false}) pretty_const #> basic_entity \<^binding>\abbrev\ (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #> basic_entity \<^binding>\typ\ Args.typ_abbrev Syntax.pretty_typ #> basic_entity \<^binding>\locale\ (Scan.lift Args.embedded_position) pretty_locale #> + basic_entity \<^binding>\bundle\ (Scan.lift Args.embedded_position) pretty_bundle #> basic_entity \<^binding>\class\ (Scan.lift Args.embedded_inner_syntax) pretty_class #> basic_entity \<^binding>\type\ (Scan.lift Args.embedded_inner_syntax) pretty_type #> basic_entity \<^binding>\theory\ (Scan.lift Args.embedded_position) pretty_theory #> basic_entities \<^binding>\prf\ Attrib.thms (pretty_prf false) #> basic_entities \<^binding>\full_prf\ Attrib.thms (pretty_prf true) #> Document_Antiquotation.setup \<^binding>\thm\ (Term_Style.parse -- Attrib.thms) (fn {context = ctxt, source = src, argument = arg} => Document_Output.pretty_items_source ctxt {embedded = false} src (pretty_thms_style ctxt arg))); in end; (* Markdown errors *) local fun markdown_error binding = Document_Antiquotation.setup binding (Scan.succeed ()) (fn {source = src, ...} => error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^ Position.here (Position.no_range_position (#1 (Token.range_of src))))) val _ = Theory.setup (markdown_error \<^binding>\item\ #> markdown_error \<^binding>\enum\ #> markdown_error \<^binding>\descr\); in end; (* control spacing *) val _ = Theory.setup (Document_Output.antiquotation_raw \<^binding>\noindent\ (Scan.succeed ()) (fn _ => fn () => Latex.string "\\noindent") #> Document_Output.antiquotation_raw \<^binding>\smallskip\ (Scan.succeed ()) (fn _ => fn () => Latex.string "\\smallskip") #> Document_Output.antiquotation_raw \<^binding>\medskip\ (Scan.succeed ()) (fn _ => fn () => Latex.string "\\medskip") #> Document_Output.antiquotation_raw \<^binding>\bigskip\ (Scan.succeed ()) (fn _ => fn () => Latex.string "\\bigskip")); (* nested document text *) local fun nested_antiquotation name s1 s2 = Document_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input) (fn ctxt => fn txt => (Context_Position.reports ctxt (Document_Output.document_reports txt); Latex.enclose_text s1 s2 (Document_Output.output_document ctxt {markdown = false} txt))); val _ = Theory.setup (nested_antiquotation \<^binding>\footnote\ "\\footnote{" "}" #> nested_antiquotation \<^binding>\emph\ "\\emph{" "}" #> nested_antiquotation \<^binding>\bold\ "\\textbf{" "}"); in end; (* index entries *) local val index_like = Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "is" |-- Args.name --| Parse.$$$ ")"); val index_args = Parse.enum1 "!" (Args.embedded_input -- Scan.option index_like); fun output_text ctxt = Document_Output.output_document ctxt {markdown = false}; fun index binding def = Document_Output.antiquotation_raw binding (Scan.lift index_args) (fn ctxt => fn args => let val _ = Context_Position.reports ctxt (maps (Document_Output.document_reports o #1) args); fun make_item (txt, opt_like) = let val text = output_text ctxt txt; val like = (case opt_like of SOME s => s | NONE => Document_Antiquotation.approx_content ctxt (Input.string_of txt)); val _ = if is_none opt_like andalso Context_Position.is_visible ctxt then writeln ("(" ^ Markup.markup Markup.keyword2 "is" ^ " " ^ quote like ^ ")" ^ Position.here (Input.pos_of txt)) else (); in {text = text, like = like} end; in Latex.index_entry {items = map make_item args, def = def} end); val _ = Theory.setup (index \<^binding>\index_ref\ false #> index \<^binding>\index_def\ true); in end; (* quasi-formal text (unchecked) *) local fun report_text ctxt text = let val pos = Input.pos_of text in Context_Position.reports ctxt [(pos, Markup.language_text (Input.is_delimited text)), (pos, Markup.raw_text)] end; fun prepare_text ctxt = Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt; fun text_antiquotation name = Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) (fn ctxt => fn text => let val _ = report_text ctxt text; in prepare_text ctxt text |> Document_Output.output_source ctxt |> Document_Output.isabelle ctxt end); val theory_text_antiquotation = Document_Output.antiquotation_raw_embedded \<^binding>\theory_text\ (Scan.lift Args.text_input) (fn ctxt => fn text => let val keywords = Thy_Header.get_keywords' ctxt; val _ = report_text ctxt text; val _ = Input.source_explode text |> Token.tokenize keywords {strict = true} |> maps (Token.reports keywords) |> Context_Position.reports_text ctxt; in prepare_text ctxt text |> Token.explode0 keywords |> maps (Document_Output.output_token ctxt) |> Document_Output.isabelle ctxt end); val _ = Theory.setup (text_antiquotation \<^binding>\text\ #> text_antiquotation \<^binding>\cartouche\ #> theory_text_antiquotation); in end; (* goal state *) local fun goal_state name main = Document_Output.antiquotation_pretty name (Scan.succeed ()) (fn ctxt => fn () => Goal_Display.pretty_goal (Config.put Goal_Display.show_main_goal main ctxt) (#goal (Proof.goal (Toplevel.proof_of (Toplevel.presentation_state ctxt))))); val _ = Theory.setup (goal_state \<^binding>\goals\ true #> goal_state \<^binding>\subgoals\ false); in end; (* embedded lemma *) val _ = Theory.setup (Document_Antiquotation.setup \<^binding>\lemma\ (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop -- Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse)) (fn {context = ctxt, source = src, argument = ((prop_tok, prop), (((_, by_pos), m1), m2))} => let val reports = (by_pos, Markup.keyword1 |> Markup.keyword_properties) :: maps Method.reports_of (m1 :: the_list m2); val _ = Context_Position.reports ctxt reports; (* FIXME check proof!? *) val _ = ctxt |> Proof.theorem NONE (K I) [[(prop, [])]] |> Proof.global_terminal_proof (m1, m2); in Document_Output.pretty_source ctxt {embedded = false} [hd src, prop_tok] (Document_Output.pretty_term ctxt prop) end)); (* verbatim text *) val _ = Theory.setup (Document_Output.antiquotation_verbatim_embedded \<^binding>\verbatim\ (Scan.lift Args.text_input) (fn ctxt => fn text => let val pos = Input.pos_of text; val _ = Context_Position.reports ctxt [(pos, Markup.language_verbatim (Input.is_delimited text)), (pos, Markup.raw_text)]; in #1 (Input.source_content text) end)); (* bash functions *) val _ = Theory.setup (Document_Output.antiquotation_verbatim_embedded \<^binding>\bash_function\ (Scan.lift Args.embedded_position) Isabelle_System.check_bash_function); (* system options *) val _ = Theory.setup (Document_Output.antiquotation_verbatim_embedded \<^binding>\system_option\ (Scan.lift Args.embedded_position) (fn ctxt => fn (name, pos) => let val _ = Completion.check_option (Options.default ()) ctxt (name, pos); in name end)); (* ML text *) local fun test_val (ml1, []) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read ");" | test_val (ml1, ml2) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : " @ ml2 @ ML_Lex.read ");"; fun test_op (ml1, ml2) = test_val (ML_Lex.read "op " @ ml1, ml2); fun test_type (ml1, []) = ML_Lex.read "val _ = NONE : (" @ ml1 @ ML_Lex.read ") option;" | test_type (ml1, ml2) = ML_Lex.read "val _ = [NONE : (" @ ml1 @ ML_Lex.read ") option, NONE : (" @ ml2 @ ML_Lex.read ") option];"; fun test_exn (ml1, []) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : exn);" | test_exn (ml1, ml2) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : " @ ml2 @ ML_Lex.read " -> exn);"; fun test_struct (ml, _) = ML_Lex.read "functor XXX() = struct structure XX = " @ ml @ ML_Lex.read " end;"; fun test_functor (Antiquote.Text tok :: _, _) = ML_Lex.read "ML_Env.check_functor " @ ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok)) | test_functor _ = raise Fail "Bad ML functor specification"; val parse_ml0 = Args.text_input >> (fn source => ("", (source, Input.empty))); val parse_ml = Args.text_input -- Scan.optional (Args.colon |-- Args.text_input) Input.empty >> pair ""; val parse_exn = Args.text_input -- Scan.optional (Args.$$$ "of" |-- Args.text_input) Input.empty >> pair ""; val parse_type = (Parse.type_args >> (fn [] => "" | [a] => a ^ " " | bs => enclose "(" ") " (commas bs))) -- (Args.text_input -- Scan.optional (Args.$$$ "=" |-- Args.text_input) Input.empty); fun eval ctxt pos ml = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos ml handle ERROR msg => error (msg ^ Position.here pos); fun make_text sep sources = let val (txt1, txt2) = apply2 (#1 o Input.source_content) sources; val is_ident = (case try List.last (Symbol.explode txt1) of NONE => false | SOME s => Symbol.is_ascii_letdig s); val txt = if txt2 = "" then txt1 else if sep = ":" andalso is_ident then txt1 ^ ": " ^ txt2 else txt1 ^ " " ^ sep ^ " " ^ txt2 in (txt, txt1) end; fun antiquotation_ml parse test kind show_kind binding index = Document_Output.antiquotation_raw binding (Scan.lift parse) (fn ctxt => fn (txt0, sources) => let val (ml1, ml2) = apply2 ML_Lex.read_source sources; val ml0 = ML_Lex.read_source (Input.string txt0); val _ = test (ml0 @ ml1, ml2) |> eval ctxt (Input.pos_of (#1 sources)); val sep = if kind = "type" then "=" else if kind = "exception" then "of" else ":"; val (txt, idx) = make_text sep sources; val main_text = Document_Output.verbatim ctxt ((if kind = "" orelse not show_kind then "" else kind ^ " ") ^ txt0 ^ txt); val index_text = (case index of NONE => [] | SOME def => let val ctxt' = Config.put Document_Antiquotation.thy_output_display false ctxt; val kind' = if kind = "" then " (ML)" else " (ML " ^ kind ^ ")"; val txt' = Document_Output.verbatim ctxt' idx @ Latex.string kind'; val like = Document_Antiquotation.approx_content ctxt' idx; in Latex.index_entry {items = [{text = txt', like = like}], def = def} end); in index_text @ main_text end); fun antiquotation_ml0 test kind = antiquotation_ml parse_ml0 test kind false; fun antiquotation_ml1 parse test kind binding = antiquotation_ml parse test kind true binding (SOME true); in val _ = Theory.setup (Latex.index_variants (antiquotation_ml0 test_val "") \<^binding>\ML\ #> Latex.index_variants (antiquotation_ml0 test_op "infix") \<^binding>\ML_infix\ #> Latex.index_variants (antiquotation_ml0 test_type "type") \<^binding>\ML_type\ #> Latex.index_variants (antiquotation_ml0 test_struct "structure") \<^binding>\ML_structure\ #> Latex.index_variants (antiquotation_ml0 test_functor "functor") \<^binding>\ML_functor\ #> antiquotation_ml0 (K []) "text" \<^binding>\ML_text\ NONE #> antiquotation_ml1 parse_ml test_val "" \<^binding>\define_ML\ #> antiquotation_ml1 parse_ml test_op "infix" \<^binding>\define_ML_infix\ #> antiquotation_ml1 parse_type test_type "type" \<^binding>\define_ML_type\ #> antiquotation_ml1 parse_exn test_exn "exception" \<^binding>\define_ML_exception\ #> antiquotation_ml1 parse_ml0 test_struct "structure" \<^binding>\define_ML_structure\ #> antiquotation_ml1 parse_ml0 test_functor "functor" \<^binding>\define_ML_functor\); end; (* URLs *) val escape_url = translate_string (fn c => if c = "%" orelse c = "#" orelse c = "^" then "\\" ^ c else c); val _ = Theory.setup (Document_Output.antiquotation_raw_embedded \<^binding>\url\ (Scan.lift Args.embedded_input) (fn ctxt => fn source => let val url = Input.string_of source; val pos = Input.pos_of source; val delimited = Input.is_delimited source; val _ = Context_Position.reports ctxt [(pos, Markup.language_url delimited), (pos, Markup.url url)]; in Latex.enclose_text "\\url{" "}" (Latex.string (escape_url url)) end)); (* formal entities *) local fun entity_antiquotation name check bg en = Document_Output.antiquotation_raw name (Scan.lift Args.name_position) (fn ctxt => fn (name, pos) => let val _ = check ctxt (name, pos) in Latex.enclose_text bg en (Latex.string (Output.output name)) end); val _ = Theory.setup (entity_antiquotation \<^binding>\command\ Outer_Syntax.check_command "\\isacommand{" "}" #> entity_antiquotation \<^binding>\method\ Method.check_name "\\isa{" "}" #> entity_antiquotation \<^binding>\attribute\ Attrib.check_name "\\isa{" "}"); in end; end;