--- a/NEWS Tue Dec 05 12:14:36 2017 +0100
+++ b/NEWS Tue Dec 05 16:54:37 2017 +0100
@@ -68,6 +68,17 @@
arguments into this format.
+*** Document preparation ***
+
+* System option "document_tags" specifies a default for otherwise
+untagged commands. This is occasionally useful to control the global
+visibility of commands via session options (e.g. in ROOT).
+
+* Document markup commands ('section', 'text' etc.) are implicitly
+tagged as "document" and visible by default. This avoids the application
+of option "document_tags" to these commands.
+
+
*** HOL ***
* SMT module:
--- a/etc/options Tue Dec 05 12:14:36 2017 +0100
+++ b/etc/options Tue Dec 05 16:54:37 2017 +0100
@@ -10,7 +10,9 @@
option document_output : string = ""
-- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
option document_variants : string = "document"
- -- "option alternative document variants (separated by colons)"
+ -- "alternative document variants (separated by colons)"
+option document_tags : string = ""
+ -- "default command tags (separated by commas)"
option thy_output_display : bool = false
-- "indicate output as multi-line display-style material"
--- a/lib/texinputs/isabelle.sty Tue Dec 05 12:14:36 2017 +0100
+++ b/lib/texinputs/isabelle.sty Tue Dec 05 16:54:37 2017 +0100
@@ -250,6 +250,7 @@
\newcommand{\isafoldtag}[1]%
{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
+\isakeeptag{document}
\isakeeptag{theory}
\isakeeptag{proof}
\isakeeptag{ML}
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Tue Dec 05 12:14:36 2017 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Tue Dec 05 16:54:37 2017 +0100
@@ -473,6 +473,7 @@
\<^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 \\
--- a/src/Doc/System/Presentation.thy Tue Dec 05 12:14:36 2017 +0100
+++ b/src/Doc/System/Presentation.thy Tue Dec 05 16:54:37 2017 +0100
@@ -182,7 +182,7 @@
pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to
drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
equivalent to the tag specification
- ``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
+ ``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
\<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in
\<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
--- a/src/Doc/System/Sessions.thy Tue Dec 05 12:14:36 2017 +0100
+++ b/src/Doc/System/Sessions.thy Tue Dec 05 16:54:37 2017 +0100
@@ -195,6 +195,10 @@
possible to use different document variant names (without tags) for
different document root entries, see also \secref{sec:tool-document}.
+ \<^item> @{system_option_def "document_tags"} specifies a default for otherwise
+ untagged commands. This is occasionally useful to control the global
+ visibility of commands via session options (e.g. in \<^verbatim>\<open>ROOT\<close>).
+
\<^item> @{system_option_def "threads"} determines the number of worker threads
for parallel checking of theories and proofs. The default \<open>0\<close> means that a
sensible maximum value is determined by the underlying hardware. For
--- a/src/Pure/Isar/keyword.ML Tue Dec 05 12:14:36 2017 +0100
+++ b/src/Pure/Isar/keyword.ML Tue Dec 05 16:54:37 2017 +0100
@@ -38,6 +38,8 @@
val no_spec: spec
val before_command_spec: spec
val quasi_command_spec: spec
+ val document_heading_spec: spec
+ val document_body_spec: spec
type keywords
val minor_keywords: keywords -> Scan.lexicon
val major_keywords: keywords -> Scan.lexicon
@@ -127,6 +129,8 @@
val no_spec: spec = (("", []), []);
val before_command_spec: spec = ((before_command, []), []);
val quasi_command_spec: spec = ((quasi_command, []), []);
+val document_heading_spec: spec = (("document_heading", []), ["document"]);
+val document_body_spec: spec = (("document_body", []), ["document"]);
type entry =
{pos: Position.T,
--- a/src/Pure/Isar/outer_syntax.ML Tue Dec 05 12:14:36 2017 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Tue Dec 05 16:54:37 2017 +0100
@@ -183,10 +183,10 @@
Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
fun parse_command thy =
- Scan.ahead (before_command |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
+ Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
let
val keywords = Thy_Header.get_keywords thy;
- val command_tags = Parse.command_ -- Parse.tags;
+ val command_tags = Parse.command -- Parse.tags;
val tr0 =
Toplevel.empty
|> Toplevel.name name
--- a/src/Pure/Isar/parse.ML Tue Dec 05 12:14:36 2017 +0100
+++ b/src/Pure/Isar/parse.ML Tue Dec 05 16:54:37 2017 +0100
@@ -15,7 +15,7 @@
val position: 'a parser -> ('a * Position.T) parser
val input: 'a parser -> Input.source parser
val inner_syntax: 'a parser -> string parser
- val command_: string parser
+ val command: string parser
val keyword: string parser
val short_ident: string parser
val long_ident: string parser
@@ -32,7 +32,7 @@
val verbatim: string parser
val cartouche: string parser
val eof: string parser
- val command: string -> string parser
+ val command_name: string -> string parser
val keyword_with: (string -> bool) -> string parser
val keyword_markup: bool * Markup.T -> string -> string parser
val keyword_improper: string -> string parser
@@ -173,7 +173,7 @@
group (fn () => Token.str_of_kind k)
(RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
-val command_ = kind Token.Command;
+val command = kind Token.Command;
val keyword = kind Token.Keyword;
val short_ident = kind Token.Ident;
val long_ident = kind Token.Long_Ident;
@@ -189,7 +189,7 @@
val cartouche = kind Token.Cartouche;
val eof = kind Token.EOF;
-fun command x =
+fun command_name x =
group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x)
(RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x)))
>> Token.content_of;
--- a/src/Pure/ROOT.ML Tue Dec 05 12:14:36 2017 +0100
+++ b/src/Pure/ROOT.ML Tue Dec 05 16:54:37 2017 +0100
@@ -280,6 +280,7 @@
(*theory documents*)
ML_file "Thy/term_style.ML";
ML_file "Isar/outer_syntax.ML";
+ML_file "ML/ml_antiquotations.ML";
ML_file "Thy/thy_output.ML";
ML_file "Thy/document_antiquotations.ML";
ML_file "General/graph_display.ML";
@@ -311,7 +312,6 @@
subsection "Miscellaneous tools and packages for Pure Isabelle";
ML_file "ML/ml_pp.ML";
-ML_file "ML/ml_antiquotations.ML";
ML_file "ML/ml_thms.ML";
ML_file "ML/ml_file.ML";
--- a/src/Pure/Thy/thy_header.ML Tue Dec 05 12:14:36 2017 +0100
+++ b/src/Pure/Thy/thy_header.ML Tue Dec 05 16:54:37 2017 +0100
@@ -77,15 +77,15 @@
((importsN, \<^here>), Keyword.quasi_command_spec),
((keywordsN, \<^here>), Keyword.quasi_command_spec),
((abbrevsN, \<^here>), Keyword.quasi_command_spec),
- ((chapterN, \<^here>), ((Keyword.document_heading, []), [])),
- ((sectionN, \<^here>), ((Keyword.document_heading, []), [])),
- ((subsectionN, \<^here>), ((Keyword.document_heading, []), [])),
- ((subsubsectionN, \<^here>), ((Keyword.document_heading, []), [])),
- ((paragraphN, \<^here>), ((Keyword.document_heading, []), [])),
- ((subparagraphN, \<^here>), ((Keyword.document_heading, []), [])),
- ((textN, \<^here>), ((Keyword.document_body, []), [])),
- ((txtN, \<^here>), ((Keyword.document_body, []), [])),
- ((text_rawN, \<^here>), ((Keyword.document_raw, []), [])),
+ ((chapterN, \<^here>), Keyword.document_heading_spec),
+ ((sectionN, \<^here>), Keyword.document_heading_spec),
+ ((subsectionN, \<^here>), Keyword.document_heading_spec),
+ ((subsubsectionN, \<^here>), Keyword.document_heading_spec),
+ ((paragraphN, \<^here>), Keyword.document_heading_spec),
+ ((subparagraphN, \<^here>), Keyword.document_heading_spec),
+ ((textN, \<^here>), Keyword.document_body_spec),
+ ((txtN, \<^here>), Keyword.document_body_spec),
+ ((text_rawN, \<^here>), ((Keyword.document_raw, []), ["document"])),
((theoryN, \<^here>), ((Keyword.thy_begin, []), ["theory"])),
(("ML", \<^here>), ((Keyword.thy_decl, []), ["ML"]))];
@@ -160,19 +160,19 @@
(* read header *)
val heading =
- (Parse.command chapterN ||
- Parse.command sectionN ||
- Parse.command subsectionN ||
- Parse.command subsubsectionN ||
- Parse.command paragraphN ||
- Parse.command subparagraphN ||
- Parse.command textN ||
- Parse.command txtN ||
- Parse.command text_rawN) --
+ (Parse.command_name chapterN ||
+ Parse.command_name sectionN ||
+ Parse.command_name subsectionN ||
+ Parse.command_name subsubsectionN ||
+ Parse.command_name paragraphN ||
+ Parse.command_name subparagraphN ||
+ Parse.command_name textN ||
+ Parse.command_name txtN ||
+ Parse.command_name text_rawN) --
Parse.tags -- Parse.!!! Parse.document_source;
val header =
- (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
+ (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
fun token_source pos =
Symbol.explode
--- a/src/Pure/Thy/thy_output.ML Tue Dec 05 12:14:36 2017 +0100
+++ b/src/Pure/Thy/thy_output.ML Tue Dec 05 16:54:37 2017 +0100
@@ -314,7 +314,8 @@
in
-fun present_span keywords span state state' (tag_stack, active_tag, newline, buffer, present_cont) =
+fun present_span keywords document_tags span state state'
+ (tag_stack, active_tag, newline, buffer, present_cont) =
let
val present = fold (fn (tok, (flag, 0)) =>
Buffer.add (output_token state' tok)
@@ -332,7 +333,7 @@
if is_some tag' then tag'
else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
else
- (case Keyword.command_tags keywords cmd_name of
+ (case Keyword.command_tags keywords cmd_name @ document_tags of
default_tag :: _ => SOME default_tag
| [] =>
if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
@@ -486,8 +487,10 @@
(* present commands *)
+ val document_tags = space_explode "," (Options.default_string @{system_option document_tags});
+
fun present_command tr span st st' =
- Toplevel.setmp_thread_position tr (present_span keywords span st st');
+ Toplevel.setmp_thread_position tr (present_span keywords document_tags span st st');
fun present _ [] = I
| present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;