merged
authorwenzelm
Tue Dec 05 16:54:37 2017 +0100 (10 months ago)
changeset 6714194fca35f80ab
parent 67135 1a94352812f4
parent 67140 386a31d6d17a
child 67142 fa1173288322
merged
     1.1 --- a/NEWS	Tue Dec 05 12:14:36 2017 +0100
     1.2 +++ b/NEWS	Tue Dec 05 16:54:37 2017 +0100
     1.3 @@ -68,6 +68,17 @@
     1.4  arguments into this format.
     1.5  
     1.6  
     1.7 +*** Document preparation ***
     1.8 +
     1.9 +* System option "document_tags" specifies a default for otherwise
    1.10 +untagged commands. This is occasionally useful to control the global
    1.11 +visibility of commands via session options (e.g. in ROOT).
    1.12 +
    1.13 +* Document markup commands ('section', 'text' etc.) are implicitly
    1.14 +tagged as "document" and visible by default. This avoids the application
    1.15 +of option "document_tags" to these commands.
    1.16 +
    1.17 +
    1.18  *** HOL ***
    1.19  
    1.20  * SMT module:
     2.1 --- a/etc/options	Tue Dec 05 12:14:36 2017 +0100
     2.2 +++ b/etc/options	Tue Dec 05 16:54:37 2017 +0100
     2.3 @@ -10,7 +10,9 @@
     2.4  option document_output : string = ""
     2.5    -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
     2.6  option document_variants : string = "document"
     2.7 -  -- "option alternative document variants (separated by colons)"
     2.8 +  -- "alternative document variants (separated by colons)"
     2.9 +option document_tags : string = ""
    2.10 +  -- "default command tags (separated by commas)"
    2.11  
    2.12  option thy_output_display : bool = false
    2.13    -- "indicate output as multi-line display-style material"
     3.1 --- a/lib/texinputs/isabelle.sty	Tue Dec 05 12:14:36 2017 +0100
     3.2 +++ b/lib/texinputs/isabelle.sty	Tue Dec 05 16:54:37 2017 +0100
     3.3 @@ -250,6 +250,7 @@
     3.4  \newcommand{\isafoldtag}[1]%
     3.5  {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
     3.6  
     3.7 +\isakeeptag{document}
     3.8  \isakeeptag{theory}
     3.9  \isakeeptag{proof}
    3.10  \isakeeptag{ML}
     4.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Dec 05 12:14:36 2017 +0100
     4.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Tue Dec 05 16:54:37 2017 +0100
     4.3 @@ -473,6 +473,7 @@
     4.4  
     4.5    \<^medskip>
     4.6    \begin{tabular}{ll}
     4.7 +    \<open>document\<close> & document markup commands \\
     4.8      \<open>theory\<close> & theory begin/end \\
     4.9      \<open>proof\<close> & all proof commands \\
    4.10      \<open>ML\<close> & all commands involving ML code \\
     5.1 --- a/src/Doc/System/Presentation.thy	Tue Dec 05 12:14:36 2017 +0100
     5.2 +++ b/src/Doc/System/Presentation.thy	Tue Dec 05 16:54:37 2017 +0100
     5.3 @@ -182,7 +182,7 @@
     5.4    pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to
     5.5    drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
     5.6    equivalent to the tag specification
     5.7 -  ``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
     5.8 +  ``\<^verbatim>\<open>+document,+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
     5.9    \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in
    5.10    \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
    5.11  
     6.1 --- a/src/Doc/System/Sessions.thy	Tue Dec 05 12:14:36 2017 +0100
     6.2 +++ b/src/Doc/System/Sessions.thy	Tue Dec 05 16:54:37 2017 +0100
     6.3 @@ -195,6 +195,10 @@
     6.4      possible to use different document variant names (without tags) for
     6.5      different document root entries, see also \secref{sec:tool-document}.
     6.6  
     6.7 +    \<^item> @{system_option_def "document_tags"} specifies a default for otherwise
     6.8 +    untagged commands. This is occasionally useful to control the global
     6.9 +    visibility of commands via session options (e.g. in \<^verbatim>\<open>ROOT\<close>).
    6.10 +
    6.11      \<^item> @{system_option_def "threads"} determines the number of worker threads
    6.12      for parallel checking of theories and proofs. The default \<open>0\<close> means that a
    6.13      sensible maximum value is determined by the underlying hardware. For
     7.1 --- a/src/Pure/Isar/keyword.ML	Tue Dec 05 12:14:36 2017 +0100
     7.2 +++ b/src/Pure/Isar/keyword.ML	Tue Dec 05 16:54:37 2017 +0100
     7.3 @@ -38,6 +38,8 @@
     7.4    val no_spec: spec
     7.5    val before_command_spec: spec
     7.6    val quasi_command_spec: spec
     7.7 +  val document_heading_spec: spec
     7.8 +  val document_body_spec: spec
     7.9    type keywords
    7.10    val minor_keywords: keywords -> Scan.lexicon
    7.11    val major_keywords: keywords -> Scan.lexicon
    7.12 @@ -127,6 +129,8 @@
    7.13  val no_spec: spec = (("", []), []);
    7.14  val before_command_spec: spec = ((before_command, []), []);
    7.15  val quasi_command_spec: spec = ((quasi_command, []), []);
    7.16 +val document_heading_spec: spec = (("document_heading", []), ["document"]);
    7.17 +val document_body_spec: spec = (("document_body", []), ["document"]);
    7.18  
    7.19  type entry =
    7.20   {pos: Position.T,
     8.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Dec 05 12:14:36 2017 +0100
     8.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Dec 05 16:54:37 2017 +0100
     8.3 @@ -183,10 +183,10 @@
     8.4    Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
     8.5  
     8.6  fun parse_command thy =
     8.7 -  Scan.ahead (before_command |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
     8.8 +  Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) =>
     8.9      let
    8.10        val keywords = Thy_Header.get_keywords thy;
    8.11 -      val command_tags = Parse.command_ -- Parse.tags;
    8.12 +      val command_tags = Parse.command -- Parse.tags;
    8.13        val tr0 =
    8.14          Toplevel.empty
    8.15          |> Toplevel.name name
     9.1 --- a/src/Pure/Isar/parse.ML	Tue Dec 05 12:14:36 2017 +0100
     9.2 +++ b/src/Pure/Isar/parse.ML	Tue Dec 05 16:54:37 2017 +0100
     9.3 @@ -15,7 +15,7 @@
     9.4    val position: 'a parser -> ('a * Position.T) parser
     9.5    val input: 'a parser -> Input.source parser
     9.6    val inner_syntax: 'a parser -> string parser
     9.7 -  val command_: string parser
     9.8 +  val command: string parser
     9.9    val keyword: string parser
    9.10    val short_ident: string parser
    9.11    val long_ident: string parser
    9.12 @@ -32,7 +32,7 @@
    9.13    val verbatim: string parser
    9.14    val cartouche: string parser
    9.15    val eof: string parser
    9.16 -  val command: string -> string parser
    9.17 +  val command_name: string -> string parser
    9.18    val keyword_with: (string -> bool) -> string parser
    9.19    val keyword_markup: bool * Markup.T -> string -> string parser
    9.20    val keyword_improper: string -> string parser
    9.21 @@ -173,7 +173,7 @@
    9.22    group (fn () => Token.str_of_kind k)
    9.23      (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
    9.24  
    9.25 -val command_ = kind Token.Command;
    9.26 +val command = kind Token.Command;
    9.27  val keyword = kind Token.Keyword;
    9.28  val short_ident = kind Token.Ident;
    9.29  val long_ident = kind Token.Long_Ident;
    9.30 @@ -189,7 +189,7 @@
    9.31  val cartouche = kind Token.Cartouche;
    9.32  val eof = kind Token.EOF;
    9.33  
    9.34 -fun command x =
    9.35 +fun command_name x =
    9.36    group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x)
    9.37      (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x)))
    9.38    >> Token.content_of;
    10.1 --- a/src/Pure/ROOT.ML	Tue Dec 05 12:14:36 2017 +0100
    10.2 +++ b/src/Pure/ROOT.ML	Tue Dec 05 16:54:37 2017 +0100
    10.3 @@ -280,6 +280,7 @@
    10.4  (*theory documents*)
    10.5  ML_file "Thy/term_style.ML";
    10.6  ML_file "Isar/outer_syntax.ML";
    10.7 +ML_file "ML/ml_antiquotations.ML";
    10.8  ML_file "Thy/thy_output.ML";
    10.9  ML_file "Thy/document_antiquotations.ML";
   10.10  ML_file "General/graph_display.ML";
   10.11 @@ -311,7 +312,6 @@
   10.12  subsection "Miscellaneous tools and packages for Pure Isabelle";
   10.13  
   10.14  ML_file "ML/ml_pp.ML";
   10.15 -ML_file "ML/ml_antiquotations.ML";
   10.16  ML_file "ML/ml_thms.ML";
   10.17  ML_file "ML/ml_file.ML";
   10.18  
    11.1 --- a/src/Pure/Thy/thy_header.ML	Tue Dec 05 12:14:36 2017 +0100
    11.2 +++ b/src/Pure/Thy/thy_header.ML	Tue Dec 05 16:54:37 2017 +0100
    11.3 @@ -77,15 +77,15 @@
    11.4       ((importsN, \<^here>), Keyword.quasi_command_spec),
    11.5       ((keywordsN, \<^here>), Keyword.quasi_command_spec),
    11.6       ((abbrevsN, \<^here>), Keyword.quasi_command_spec),
    11.7 -     ((chapterN, \<^here>), ((Keyword.document_heading, []), [])),
    11.8 -     ((sectionN, \<^here>), ((Keyword.document_heading, []), [])),
    11.9 -     ((subsectionN, \<^here>), ((Keyword.document_heading, []), [])),
   11.10 -     ((subsubsectionN, \<^here>), ((Keyword.document_heading, []), [])),
   11.11 -     ((paragraphN, \<^here>), ((Keyword.document_heading, []), [])),
   11.12 -     ((subparagraphN, \<^here>), ((Keyword.document_heading, []), [])),
   11.13 -     ((textN, \<^here>), ((Keyword.document_body, []), [])),
   11.14 -     ((txtN, \<^here>), ((Keyword.document_body, []), [])),
   11.15 -     ((text_rawN, \<^here>), ((Keyword.document_raw, []), [])),
   11.16 +     ((chapterN, \<^here>), Keyword.document_heading_spec),
   11.17 +     ((sectionN, \<^here>), Keyword.document_heading_spec),
   11.18 +     ((subsectionN, \<^here>), Keyword.document_heading_spec),
   11.19 +     ((subsubsectionN, \<^here>), Keyword.document_heading_spec),
   11.20 +     ((paragraphN, \<^here>), Keyword.document_heading_spec),
   11.21 +     ((subparagraphN, \<^here>), Keyword.document_heading_spec),
   11.22 +     ((textN, \<^here>), Keyword.document_body_spec),
   11.23 +     ((txtN, \<^here>), Keyword.document_body_spec),
   11.24 +     ((text_rawN, \<^here>), ((Keyword.document_raw, []), ["document"])),
   11.25       ((theoryN, \<^here>), ((Keyword.thy_begin, []), ["theory"])),
   11.26       (("ML", \<^here>), ((Keyword.thy_decl, []), ["ML"]))];
   11.27  
   11.28 @@ -160,19 +160,19 @@
   11.29  (* read header *)
   11.30  
   11.31  val heading =
   11.32 -  (Parse.command chapterN ||
   11.33 -    Parse.command sectionN ||
   11.34 -    Parse.command subsectionN ||
   11.35 -    Parse.command subsubsectionN ||
   11.36 -    Parse.command paragraphN ||
   11.37 -    Parse.command subparagraphN ||
   11.38 -    Parse.command textN ||
   11.39 -    Parse.command txtN ||
   11.40 -    Parse.command text_rawN) --
   11.41 +  (Parse.command_name chapterN ||
   11.42 +    Parse.command_name sectionN ||
   11.43 +    Parse.command_name subsectionN ||
   11.44 +    Parse.command_name subsubsectionN ||
   11.45 +    Parse.command_name paragraphN ||
   11.46 +    Parse.command_name subparagraphN ||
   11.47 +    Parse.command_name textN ||
   11.48 +    Parse.command_name txtN ||
   11.49 +    Parse.command_name text_rawN) --
   11.50    Parse.tags -- Parse.!!! Parse.document_source;
   11.51  
   11.52  val header =
   11.53 -  (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args;
   11.54 +  (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
   11.55  
   11.56  fun token_source pos =
   11.57    Symbol.explode
    12.1 --- a/src/Pure/Thy/thy_output.ML	Tue Dec 05 12:14:36 2017 +0100
    12.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Dec 05 16:54:37 2017 +0100
    12.3 @@ -314,7 +314,8 @@
    12.4  
    12.5  in
    12.6  
    12.7 -fun present_span keywords span state state' (tag_stack, active_tag, newline, buffer, present_cont) =
    12.8 +fun present_span keywords document_tags span state state'
    12.9 +    (tag_stack, active_tag, newline, buffer, present_cont) =
   12.10    let
   12.11      val present = fold (fn (tok, (flag, 0)) =>
   12.12          Buffer.add (output_token state' tok)
   12.13 @@ -332,7 +333,7 @@
   12.14        if is_some tag' then tag'
   12.15        else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
   12.16        else
   12.17 -        (case Keyword.command_tags keywords cmd_name of
   12.18 +        (case Keyword.command_tags keywords cmd_name @ document_tags of
   12.19            default_tag :: _ => SOME default_tag
   12.20          | [] =>
   12.21              if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
   12.22 @@ -486,8 +487,10 @@
   12.23  
   12.24      (* present commands *)
   12.25  
   12.26 +    val document_tags = space_explode "," (Options.default_string @{system_option document_tags});
   12.27 +
   12.28      fun present_command tr span st st' =
   12.29 -      Toplevel.setmp_thread_position tr (present_span keywords span st st');
   12.30 +      Toplevel.setmp_thread_position tr (present_span keywords document_tags span st st');
   12.31  
   12.32      fun present _ [] = I
   12.33        | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;