--- a/NEWS Sat Mar 23 20:27:56 2019 +0100
+++ b/NEWS Sun Mar 24 13:48:46 2019 +0100
@@ -85,6 +85,21 @@
separated from option "-s".
+*** Document preparation ***
+
+* Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that
+are stripped from document output: the effect is to modify the semantic
+presentation context or to emit markup to the PIDE document. Some
+predefined markers are taken from the Dublin Core Metadata Initiative,
+e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that
+can retrieved from the document database.
+
+* Old-style command tags %name are re-interpreted as markers \<^marker>\<open>tag name\<close>
+and produce LaTeX environments as before. Potential INCOMPATIBILITY:
+multiple markers are composed in canonical order, resulting in a
+reversed list of tags in the presentation context.
+
+
*** Isar ***
* More robust treatment of structural errors: begin/end blocks take
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Sat Mar 23 20:27:56 2019 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sun Mar 24 13:48:46 2019 +0100
@@ -466,43 +466,89 @@
\<close>
-section \<open>Markup via command tags \label{sec:tags}\<close>
+section \<open>Document markers and command tags \label{sec:document-markers}\<close>
text \<open>
- Each Isabelle/Isar command may be decorated by additional presentation tags,
- to indicate some modification in the way it is printed in the document.
+ \emph{Document markers} are formal comments of the form \<open>\<^marker>\<open>marker_body\<close>\<close>
+ (using the control symbol \<^verbatim>\<open>\<^marker>\<close>) 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>\<open>
- @{syntax_def tags}: ( tag * )
+ @{syntax_def marker}: '\<^marker>' @{syntax cartouche}
+ ;
+ @{syntax_def marker_body}: (@{syntax name} @{syntax args} * ',')
+ ;
+ @{syntax_def tags}: tag*
;
tag: '%' (@{syntax short_ident} | @{syntax string})
\<close>
- Some tags are pre-declared for certain classes of commands, serving as
- default markup if no tags are given in the text:
+ 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>\<open>
+ (@@{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} @{syntax name}
+ \<close>
- \<^medskip>
- \begin{tabular}{ll}
- \<open>document\<close> & document markup commands \\
- \<open>theory\<close> & theory begin/end \\
- \<open>proof\<close> & all proof commands \\
- \<open>ML\<close> & all commands involving ML code \\
- \end{tabular}
- \<^medskip>
+ \<^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>,
+ \<open>\<^marker>\<open>license arg\<close>\<close>, and \<open>\<^marker>\<open>description arg\<close>\<close> produce markup in the PIDE
+ document, without any immediate effect on typesetting. This vocabulary is
+ taken from the Dublin Core Metadata
+ Initiative\<^footnote>\<open>\<^url>\<open>https://www.dublincore.org/specifications/dublin-core/dcmi-terms\<close>\<close>.
+ The argument is an uninterpreted string, except for @{document_marker
+ description}, which consists of words that are subject to spell-checking.
+
+ \<^descr> \<open>\<^marker>\<open>tag name\<close>\<close> updates the list of command tags in the presentation
+ context: later declarations take precedence, so \<open>\<^marker>\<open>tag a, tag b, tag c\<close>\<close>
+ produces a reversed list. The default tags are given by the original
+ \<^theory_text>\<open>keywords\<close> declaration of a command, and the system option
+ @{system_option_ref document_tags}.
+
+ An old-style command tag \<^verbatim>\<open>%\<close>\<open>name\<close> is treated like a document marker
+ \<open>\<^marker>\<open>tag name\<close>\<close>: 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}
+ \<open>document\<close> & document markup commands \\
+ \<open>theory\<close> & theory begin/end \\
+ \<open>proof\<close> & all proof commands \\
+ \<open>ML\<close> & 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 ``@{command "by"}~\<open>%invisible auto\<close>'' causes that piece of proof
- to be treated as \<open>invisible\<close> instead of \<open>proof\<close> (the default), which may be
- shown or hidden depending on the document setup. In contrast, ``@{command
- "by"}~\<open>%visible auto\<close>'' forces this text to be shown invariably.
+ For example ``\<^theory_text>\<open>by auto\<close>~\<open>\<^marker>\<open>tag invisible\<close>\<close>'' causes that piece of proof to
+ be treated as \<open>invisible\<close> instead of \<open>proof\<close> (the default), which may be
+ shown or hidden depending on the document setup. In contrast, ``\<^theory_text>\<open>by
+ auto\<close>~\<open>\<^marker>\<open>tag visible\<close>\<close>'' 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, ``@{command "proof"}~\<open>%visible
- \<dots>\<close>~@{command "qed"}'' forces the whole sub-proof to be typeset as \<open>visible\<close>
- (unless some of its parts are tagged differently).
+ of the same level of nesting. For example, ``\<^theory_text>\<open>proof\<close>~\<open>\<^marker>\<open>tag invisible\<close>
+ \<dots>\<close>~\<^theory_text>\<open>qed\<close>'' forces the whole sub-proof to be typeset as \<open>visible\<close> (unless
+ some of its parts are tagged differently).
\<^medskip>
Command tags merely produce certain markup environments for type-setting.
--- a/src/Doc/Isar_Ref/Spec.thy Sat Mar 23 20:27:56 2019 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Sun Mar 24 13:48:46 2019 +0100
@@ -96,7 +96,7 @@
\<open>:: thy_goal_defn\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_defn\<close> for
theory-level definitions with and without proof, respectively. Additional
@{syntax tags} provide defaults for document preparation
- (\secref{sec:tags}).
+ (\secref{sec:document-markers}).
The @{keyword_def "abbrevs"} specification declares additional abbreviations
for syntactic completion. The default for a new keyword is just its name,
--- a/src/Doc/Isar_Ref/document/root.tex Sat Mar 23 20:27:56 2019 +0100
+++ b/src/Doc/Isar_Ref/document/root.tex Sun Mar 24 13:48:46 2019 +0100
@@ -5,6 +5,7 @@
\usepackage{amssymb}
\usepackage{wasysym}
\usepackage{eurosym}
+\usepackage{pifont}
\usepackage[english]{babel}
\usepackage[only,bigsqcap]{stmaryrd}
\usepackage{textcomp}
--- a/src/Doc/antiquote_setup.ML Sat Mar 23 20:27:56 2019 +0100
+++ b/src/Doc/antiquote_setup.ML Sun Mar 24 13:48:46 2019 +0100
@@ -196,6 +196,7 @@
entity_antiqs no_check "" \<^binding>\<open>case\<close> #>
entity_antiqs Document_Antiquotation.check "" \<^binding>\<open>antiquotation\<close> #>
entity_antiqs Document_Antiquotation.check_option "" \<^binding>\<open>antiquotation_option\<close> #>
+ entity_antiqs Document_Marker.check "" \<^binding>\<open>document_marker\<close> #>
entity_antiqs no_check "isasystem" \<^binding>\<open>setting\<close> #>
entity_antiqs check_system_option "isasystem" \<^binding>\<open>system_option\<close> #>
entity_antiqs no_check "" \<^binding>\<open>inference\<close> #>
--- a/src/Pure/PIDE/markup.ML Sat Mar 23 20:27:56 2019 +0100
+++ b/src/Pure/PIDE/markup.ML Sun Mar 24 13:48:46 2019 +0100
@@ -20,8 +20,8 @@
val meta_creatorN: string val meta_creator: T
val meta_contributorN: string val meta_contributor: T
val meta_dateN: string val meta_date: T
+ val meta_licenseN: string val meta_license: T
val meta_descriptionN: string val meta_description: T
- val meta_licenseN: string val meta_license: T
val languageN: string
val symbolsN: string
val delimitedN: string
@@ -289,14 +289,14 @@
val instanceN = "instance";
-(* meta data -- see http://dublincore.org/documents/dces *)
+(* meta data -- see https://www.dublincore.org/specifications/dublin-core/dcmi-terms *)
val (meta_titleN, meta_title) = markup_elem "meta_title";
val (meta_creatorN, meta_creator) = markup_elem "meta_creator";
val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor";
val (meta_dateN, meta_date) = markup_elem "meta_date";
+val (meta_licenseN, meta_license) = markup_elem "meta_license";
val (meta_descriptionN, meta_description) = markup_elem "meta_description";
-val (meta_licenseN, meta_license) = markup_elem "meta_license";
(* embedded languages *)
--- a/src/Pure/PIDE/markup.scala Sat Mar 23 20:27:56 2019 +0100
+++ b/src/Pure/PIDE/markup.scala Sun Mar 24 13:48:46 2019 +0100
@@ -95,8 +95,8 @@
val META_CREATOR = "meta_creator"
val META_CONTRIBUTOR = "meta_contributor"
val META_DATE = "meta_date"
+ val META_LICENSE = "meta_license"
val META_DESCRIPTION = "meta_description"
- val META_LICENSE = "meta_license"
/* formal entities */
--- a/src/Pure/Thy/document_marker.ML Sat Mar 23 20:27:56 2019 +0100
+++ b/src/Pure/Thy/document_marker.ML Sun Mar 24 13:48:46 2019 +0100
@@ -7,6 +7,7 @@
signature DOCUMENT_MARKER =
sig
type marker = Proof.context -> Proof.context
+ val check: Proof.context -> string * Position.T -> string * (Token.src -> marker)
val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory
val setup0: binding -> 'a parser -> ('a -> marker) -> theory -> theory
val evaluate: Input.source -> marker
@@ -71,13 +72,13 @@
setup0 (Binding.make ("creator", \<^here>)) Parse.embedded (meta_data Markup.meta_creator) #>
setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #>
setup0 (Binding.make ("date", \<^here>)) Parse.embedded (meta_data Markup.meta_date) #>
+ setup0 (Binding.make ("license", \<^here>)) Parse.embedded (meta_data Markup.meta_license) #>
setup0 (Binding.make ("description", \<^here>)) (Parse.input Parse.embedded)
(fn source => fn ctxt =>
let
val (arg, pos) = Input.source_content source;
val _ = Context_Position.report ctxt pos Markup.words;
- in meta_data Markup.meta_description arg ctxt end) #>
- setup0 (Binding.make ("license", \<^here>)) Parse.embedded (meta_data Markup.meta_license));
+ in meta_data Markup.meta_description arg ctxt end));
fun legacy_tag name =
Input.string (cartouche ("tag " ^ Symbol_Pos.quote_string_qq name));