# HG changeset patch
# User wenzelm
# Date 1553431726 -3600
# Node ID 82e945d472d58f8385808eb2ca7164b371b5f693
# Parent  708743578e45826115a980e4f35c913dc49af984
documentation of document markers and re-interpreted command tags;

diff -r 708743578e45 -r 82e945d472d5 NEWS
--- 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
diff -r 708743578e45 -r 82e945d472d5 src/Doc/Isar_Ref/Document_Preparation.thy
--- 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.
diff -r 708743578e45 -r 82e945d472d5 src/Doc/Isar_Ref/Spec.thy
--- 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,
diff -r 708743578e45 -r 82e945d472d5 src/Doc/Isar_Ref/document/root.tex
--- 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}
diff -r 708743578e45 -r 82e945d472d5 src/Doc/antiquote_setup.ML
--- 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> #>
diff -r 708743578e45 -r 82e945d472d5 src/Pure/PIDE/markup.ML
--- 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 *)
diff -r 708743578e45 -r 82e945d472d5 src/Pure/PIDE/markup.scala
--- 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 */
diff -r 708743578e45 -r 82e945d472d5 src/Pure/Thy/document_marker.ML
--- 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));