documentation of document markers and re-interpreted command tags;
authorwenzelm
Sun Mar 24 13:48:46 2019 +0100 (4 weeks ago)
changeset 6996282e945d472d5
parent 69961 708743578e45
child 69963 396e0120f7b8
documentation of document markers and re-interpreted command tags;
NEWS
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/Isar_Ref/Spec.thy
src/Doc/Isar_Ref/document/root.tex
src/Doc/antiquote_setup.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Thy/document_marker.ML
     1.1 --- a/NEWS	Sat Mar 23 20:27:56 2019 +0100
     1.2 +++ b/NEWS	Sun Mar 24 13:48:46 2019 +0100
     1.3 @@ -85,6 +85,21 @@
     1.4  separated from option "-s".
     1.5  
     1.6  
     1.7 +*** Document preparation ***
     1.8 +
     1.9 +* Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that
    1.10 +are stripped from document output: the effect is to modify the semantic
    1.11 +presentation context or to emit markup to the PIDE document. Some
    1.12 +predefined markers are taken from the Dublin Core Metadata Initiative,
    1.13 +e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that
    1.14 +can retrieved from the document database.
    1.15 +
    1.16 +* Old-style command tags %name are re-interpreted as markers \<^marker>\<open>tag name\<close>
    1.17 +and produce LaTeX environments as before. Potential INCOMPATIBILITY:
    1.18 +multiple markers are composed in canonical order, resulting in a
    1.19 +reversed list of tags in the presentation context.
    1.20 +
    1.21 +
    1.22  *** Isar ***
    1.23  
    1.24  * More robust treatment of structural errors: begin/end blocks take
     2.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Sat Mar 23 20:27:56 2019 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Sun Mar 24 13:48:46 2019 +0100
     2.3 @@ -466,43 +466,89 @@
     2.4  \<close>
     2.5  
     2.6  
     2.7 -section \<open>Markup via command tags \label{sec:tags}\<close>
     2.8 +section \<open>Document markers and command tags \label{sec:document-markers}\<close>
     2.9  
    2.10  text \<open>
    2.11 -  Each Isabelle/Isar command may be decorated by additional presentation tags,
    2.12 -  to indicate some modification in the way it is printed in the document.
    2.13 +  \emph{Document markers} are formal comments of the form \<open>\<^marker>\<open>marker_body\<close>\<close>
    2.14 +  (using the control symbol \<^verbatim>\<open>\<^marker>\<close>) and may occur anywhere within the
    2.15 +  outer syntax of a command: the inner syntax of a marker body resembles that
    2.16 +  for attributes (\secref{sec:syn-att}). In contrast, \emph{Command tags} may
    2.17 +  only occur after a command keyword and are treated as special markers as
    2.18 +  explained below.
    2.19  
    2.20    \<^rail>\<open>
    2.21 -    @{syntax_def tags}: ( tag * )
    2.22 +    @{syntax_def marker}: '\<^marker>' @{syntax cartouche}
    2.23 +    ;
    2.24 +    @{syntax_def marker_body}: (@{syntax name} @{syntax args} * ',')
    2.25 +    ;
    2.26 +    @{syntax_def tags}: tag*
    2.27      ;
    2.28      tag: '%' (@{syntax short_ident} | @{syntax string})
    2.29    \<close>
    2.30  
    2.31 -  Some tags are pre-declared for certain classes of commands, serving as
    2.32 -  default markup if no tags are given in the text:
    2.33 +  Document markers are stripped from the document output, but surrounding
    2.34 +  white-space is preserved: e.g.\ a marker at the end of a line does not
    2.35 +  affect the subsequent line break. Markers operate within the semantic
    2.36 +  presentation context of a command, and may modify it to change the overall
    2.37 +  appearance of a command span (e.g.\ by adding tags).
    2.38 +
    2.39 +  Each document marker has its own syntax defined in the theory context; the
    2.40 +  following markers are predefined in Isabelle/Pure:
    2.41 +
    2.42 +  \<^rail>\<open>
    2.43 +    (@@{document_marker_def title} |
    2.44 +     @@{document_marker_def creator} |
    2.45 +     @@{document_marker_def contributor} |
    2.46 +     @@{document_marker_def date} |
    2.47 +     @@{document_marker_def license} |
    2.48 +     @@{document_marker_def description}) @{syntax embedded}
    2.49 +    ;
    2.50 +    @@{document_marker_def tag} @{syntax name}
    2.51 +  \<close>
    2.52  
    2.53 -  \<^medskip>
    2.54 -  \begin{tabular}{ll}
    2.55 -    \<open>document\<close> & document markup commands \\
    2.56 -    \<open>theory\<close> & theory begin/end \\
    2.57 -    \<open>proof\<close> & all proof commands \\
    2.58 -    \<open>ML\<close> & all commands involving ML code \\
    2.59 -  \end{tabular}
    2.60 -  \<^medskip>
    2.61 +    \<^descr> \<open>\<^marker>\<open>title arg\<close>\<close>, \<open>\<^marker>\<open>creator arg\<close>\<close>, \<open>\<^marker>\<open>contributor arg\<close>\<close>, \<open>\<^marker>\<open>date arg\<close>\<close>,
    2.62 +    \<open>\<^marker>\<open>license arg\<close>\<close>, and \<open>\<^marker>\<open>description arg\<close>\<close> produce markup in the PIDE
    2.63 +    document, without any immediate effect on typesetting. This vocabulary is
    2.64 +    taken from the Dublin Core Metadata
    2.65 +    Initiative\<^footnote>\<open>\<^url>\<open>https://www.dublincore.org/specifications/dublin-core/dcmi-terms\<close>\<close>.
    2.66 +    The argument is an uninterpreted string, except for @{document_marker
    2.67 +    description}, which consists of words that are subject to spell-checking.
    2.68 +
    2.69 +    \<^descr> \<open>\<^marker>\<open>tag name\<close>\<close> updates the list of command tags in the presentation
    2.70 +    context: later declarations take precedence, so \<open>\<^marker>\<open>tag a, tag b, tag c\<close>\<close>
    2.71 +    produces a reversed list. The default tags are given by the original
    2.72 +    \<^theory_text>\<open>keywords\<close> declaration of a command, and the system option
    2.73 +    @{system_option_ref document_tags}.
    2.74 +
    2.75 +    An old-style command tag \<^verbatim>\<open>%\<close>\<open>name\<close> is treated like a document marker
    2.76 +    \<open>\<^marker>\<open>tag name\<close>\<close>: the list of command tags precedes the list of document
    2.77 +    markers. The head of the resulting tags in the presentation context is
    2.78 +    turned into {\LaTeX} environments to modify the type-setting. The
    2.79 +    following tags are pre-declared for certain classes of commands, and serve
    2.80 +    as default markup for certain kinds of commands:
    2.81 +
    2.82 +    \<^medskip>
    2.83 +    \begin{tabular}{ll}
    2.84 +      \<open>document\<close> & document markup commands \\
    2.85 +      \<open>theory\<close> & theory begin/end \\
    2.86 +      \<open>proof\<close> & all proof commands \\
    2.87 +      \<open>ML\<close> & all commands involving ML code \\
    2.88 +    \end{tabular}
    2.89 +    \<^medskip>
    2.90  
    2.91    The Isabelle document preparation system @{cite "isabelle-system"} allows
    2.92    tagged command regions to be presented specifically, e.g.\ to fold proof
    2.93    texts, or drop parts of the text completely.
    2.94  
    2.95 -  For example ``@{command "by"}~\<open>%invisible auto\<close>'' causes that piece of proof
    2.96 -  to be treated as \<open>invisible\<close> instead of \<open>proof\<close> (the default), which may be
    2.97 -  shown or hidden depending on the document setup. In contrast, ``@{command
    2.98 -  "by"}~\<open>%visible auto\<close>'' forces this text to be shown invariably.
    2.99 +  For example ``\<^theory_text>\<open>by auto\<close>~\<open>\<^marker>\<open>tag invisible\<close>\<close>'' causes that piece of proof to
   2.100 +  be treated as \<open>invisible\<close> instead of \<open>proof\<close> (the default), which may be
   2.101 +  shown or hidden depending on the document setup. In contrast, ``\<^theory_text>\<open>by
   2.102 +  auto\<close>~\<open>\<^marker>\<open>tag visible\<close>\<close>'' forces this text to be shown invariably.
   2.103  
   2.104    Explicit tag specifications within a proof apply to all subsequent commands
   2.105 -  of the same level of nesting. For example, ``@{command "proof"}~\<open>%visible
   2.106 -  \<dots>\<close>~@{command "qed"}'' forces the whole sub-proof to be typeset as \<open>visible\<close>
   2.107 -  (unless some of its parts are tagged differently).
   2.108 +  of the same level of nesting. For example, ``\<^theory_text>\<open>proof\<close>~\<open>\<^marker>\<open>tag invisible\<close>
   2.109 +  \<dots>\<close>~\<^theory_text>\<open>qed\<close>'' forces the whole sub-proof to be typeset as \<open>visible\<close> (unless
   2.110 +  some of its parts are tagged differently).
   2.111  
   2.112    \<^medskip>
   2.113    Command tags merely produce certain markup environments for type-setting.
     3.1 --- a/src/Doc/Isar_Ref/Spec.thy	Sat Mar 23 20:27:56 2019 +0100
     3.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sun Mar 24 13:48:46 2019 +0100
     3.3 @@ -96,7 +96,7 @@
     3.4    \<open>:: thy_goal_defn\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_defn\<close> for
     3.5    theory-level definitions with and without proof, respectively. Additional
     3.6    @{syntax tags} provide defaults for document preparation
     3.7 -  (\secref{sec:tags}).
     3.8 +  (\secref{sec:document-markers}).
     3.9  
    3.10    The @{keyword_def "abbrevs"} specification declares additional abbreviations
    3.11    for syntactic completion. The default for a new keyword is just its name,
     4.1 --- a/src/Doc/Isar_Ref/document/root.tex	Sat Mar 23 20:27:56 2019 +0100
     4.2 +++ b/src/Doc/Isar_Ref/document/root.tex	Sun Mar 24 13:48:46 2019 +0100
     4.3 @@ -5,6 +5,7 @@
     4.4  \usepackage{amssymb}
     4.5  \usepackage{wasysym}
     4.6  \usepackage{eurosym}
     4.7 +\usepackage{pifont}
     4.8  \usepackage[english]{babel}
     4.9  \usepackage[only,bigsqcap]{stmaryrd}
    4.10  \usepackage{textcomp}
     5.1 --- a/src/Doc/antiquote_setup.ML	Sat Mar 23 20:27:56 2019 +0100
     5.2 +++ b/src/Doc/antiquote_setup.ML	Sun Mar 24 13:48:46 2019 +0100
     5.3 @@ -196,6 +196,7 @@
     5.4      entity_antiqs no_check "" \<^binding>\<open>case\<close> #>
     5.5      entity_antiqs Document_Antiquotation.check "" \<^binding>\<open>antiquotation\<close> #>
     5.6      entity_antiqs Document_Antiquotation.check_option "" \<^binding>\<open>antiquotation_option\<close> #>
     5.7 +    entity_antiqs Document_Marker.check "" \<^binding>\<open>document_marker\<close> #>
     5.8      entity_antiqs no_check "isasystem" \<^binding>\<open>setting\<close> #>
     5.9      entity_antiqs check_system_option "isasystem" \<^binding>\<open>system_option\<close> #>
    5.10      entity_antiqs no_check "" \<^binding>\<open>inference\<close> #>
     6.1 --- a/src/Pure/PIDE/markup.ML	Sat Mar 23 20:27:56 2019 +0100
     6.2 +++ b/src/Pure/PIDE/markup.ML	Sun Mar 24 13:48:46 2019 +0100
     6.3 @@ -20,8 +20,8 @@
     6.4    val meta_creatorN: string val meta_creator: T
     6.5    val meta_contributorN: string val meta_contributor: T
     6.6    val meta_dateN: string val meta_date: T
     6.7 +  val meta_licenseN: string val meta_license: T
     6.8    val meta_descriptionN: string val meta_description: T
     6.9 -  val meta_licenseN: string val meta_license: T
    6.10    val languageN: string
    6.11    val symbolsN: string
    6.12    val delimitedN: string
    6.13 @@ -289,14 +289,14 @@
    6.14  val instanceN = "instance";
    6.15  
    6.16  
    6.17 -(* meta data -- see http://dublincore.org/documents/dces *)
    6.18 +(* meta data -- see https://www.dublincore.org/specifications/dublin-core/dcmi-terms *)
    6.19  
    6.20  val (meta_titleN, meta_title) = markup_elem "meta_title";
    6.21  val (meta_creatorN, meta_creator) = markup_elem "meta_creator";
    6.22  val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor";
    6.23  val (meta_dateN, meta_date) = markup_elem "meta_date";
    6.24 +val (meta_licenseN, meta_license) = markup_elem "meta_license";
    6.25  val (meta_descriptionN, meta_description) = markup_elem "meta_description";
    6.26 -val (meta_licenseN, meta_license) = markup_elem "meta_license";
    6.27  
    6.28  
    6.29  (* embedded languages *)
     7.1 --- a/src/Pure/PIDE/markup.scala	Sat Mar 23 20:27:56 2019 +0100
     7.2 +++ b/src/Pure/PIDE/markup.scala	Sun Mar 24 13:48:46 2019 +0100
     7.3 @@ -95,8 +95,8 @@
     7.4    val META_CREATOR = "meta_creator"
     7.5    val META_CONTRIBUTOR = "meta_contributor"
     7.6    val META_DATE = "meta_date"
     7.7 +  val META_LICENSE = "meta_license"
     7.8    val META_DESCRIPTION = "meta_description"
     7.9 -  val META_LICENSE = "meta_license"
    7.10  
    7.11  
    7.12    /* formal entities */
     8.1 --- a/src/Pure/Thy/document_marker.ML	Sat Mar 23 20:27:56 2019 +0100
     8.2 +++ b/src/Pure/Thy/document_marker.ML	Sun Mar 24 13:48:46 2019 +0100
     8.3 @@ -7,6 +7,7 @@
     8.4  signature DOCUMENT_MARKER =
     8.5  sig
     8.6    type marker = Proof.context -> Proof.context
     8.7 +  val check: Proof.context -> string * Position.T -> string * (Token.src -> marker)
     8.8    val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory
     8.9    val setup0: binding -> 'a parser -> ('a -> marker) -> theory -> theory
    8.10    val evaluate: Input.source -> marker
    8.11 @@ -71,13 +72,13 @@
    8.12       setup0 (Binding.make ("creator", \<^here>)) Parse.embedded (meta_data Markup.meta_creator) #>
    8.13       setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #>
    8.14       setup0 (Binding.make ("date", \<^here>)) Parse.embedded (meta_data Markup.meta_date) #>
    8.15 +     setup0 (Binding.make ("license", \<^here>)) Parse.embedded (meta_data Markup.meta_license) #>
    8.16       setup0 (Binding.make ("description", \<^here>)) (Parse.input Parse.embedded)
    8.17        (fn source => fn ctxt =>
    8.18          let
    8.19            val (arg, pos) = Input.source_content source;
    8.20            val _ = Context_Position.report ctxt pos Markup.words;
    8.21 -        in meta_data Markup.meta_description arg ctxt end) #>
    8.22 -     setup0 (Binding.make ("license", \<^here>)) Parse.embedded (meta_data Markup.meta_license));
    8.23 +        in meta_data Markup.meta_description arg ctxt end));
    8.24  
    8.25  fun legacy_tag name =
    8.26    Input.string (cartouche ("tag " ^ Symbol_Pos.quote_string_qq name));