--- a/NEWS Tue Jun 26 17:22:43 2018 +0200
+++ b/NEWS Tue Jun 26 19:29:14 2018 +0200
@@ -151,9 +151,9 @@
theory Pure. Thus elementary antiquotations may be used in markup
commands (e.g. 'chapter', 'section', 'text') and formal comments.
-* 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).
+* System option "document_tags" specifies alternative command tags. 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
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Tue Jun 26 17:22:43 2018 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Tue Jun 26 19:29:14 2018 +0200
@@ -391,7 +391,7 @@
atom: @{syntax short_ident} | @{syntax int} | @{syntax float} | @{syntax cartouche}
\<close>}
- Each @{syntax entry} is a name-value pair: if the value is omitted, if
+ Each @{syntax entry} is a name-value pair: if the value is omitted, it
defaults to \<^verbatim>\<open>true\<close> (intended for Boolean properties). The following
standard block properties are supported:
--- a/src/Doc/System/Environment.thy Tue Jun 26 17:22:43 2018 +0200
+++ b/src/Doc/System/Environment.thy Tue Jun 26 19:29:14 2018 +0200
@@ -73,7 +73,7 @@
minimum.
\<^medskip>
- A few variables are somewhat special, e.g. @{setting_def ISABELLE_TOOL} is
+ A few variables are somewhat special, e.g.\ @{setting_def ISABELLE_TOOL} is
set automatically to the absolute path name of the @{executable isabelle}
executables.
@@ -207,7 +207,7 @@
files.
\<^descr>[@{setting_def ISABELLE_TOOL_JAVA_OPTIONS}] is passed to the \<^verbatim>\<open>java\<close>
- executable when running Isabelle tools (e.g. @{tool build}). This is
+ executable when running Isabelle tools (e.g.\ @{tool build}). This is
occasionally helpful to provide more heap space, via additional options like
\<^verbatim>\<open>-Xms1g -Xmx4g\<close>.
\<close>
--- a/src/Doc/System/Server.thy Tue Jun 26 17:22:43 2018 +0200
+++ b/src/Doc/System/Server.thy Tue Jun 26 19:29:14 2018 +0200
@@ -481,7 +481,7 @@
when building a session image). Apart from a regular output message, it also
reveals the formal theory name (e.g.\ \<^verbatim>\<open>"HOL.Nat"\<close>) and session name (e.g.\
\<^verbatim>\<open>"HOL"\<close>). Note that some rare theory names lack a proper session prefix,
- e.g. theory \<^verbatim>\<open>"Main"\<close> in session \<^verbatim>\<open>"HOL"\<close>.
+ e.g.\ theory \<^verbatim>\<open>"Main"\<close> in session \<^verbatim>\<open>"HOL"\<close>.
\<^item> \<^bold>\<open>type\<close>~\<open>timing = {elapsed: double, cpu: double, gc: double}\<close> refers to
common Isabelle timing information in seconds, usually with a precision of
--- a/src/Doc/System/Sessions.thy Tue Jun 26 17:22:43 2018 +0200
+++ b/src/Doc/System/Sessions.thy Tue Jun 26 19:29:14 2018 +0200
@@ -199,9 +199,11 @@
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 "document_tags"} specifies alternative command tags
+ as a comma-separated list of items: either ``\<open>command\<close>\<^verbatim>\<open>%\<close>\<open>tag\<close>'' for a
+ specific command, or ``\<^verbatim>\<open>%\<close>\<open>tag\<close>'' as default for all other 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
@@ -563,7 +565,7 @@
-n no build of session
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-s system build mode for session image
- -x PATTERN extract files matching pattern (e.g. "*:**" for all)
+ -x PATTERN extract files matching pattern (e.g.\ "*:**" for all)
List or export theory exports for SESSION: named blobs produced by
isabelle build. Option -l or -x is required; option -x may be repeated.
--- a/src/Doc/manual.bib Tue Jun 26 17:22:43 2018 +0200
+++ b/src/Doc/manual.bib Tue Jun 26 19:29:14 2018 +0200
@@ -1613,7 +1613,8 @@
title = {{ML} for the Working Programmer},
year = 1996,
edition = {2nd},
- publisher = CUP}
+ publisher = CUP,
+ note = {\url{https://www.cl.cam.ac.uk/~lp15/MLbook}}}
@article{paulson-natural,
author = {Lawrence C. Paulson},
--- a/src/HOL/ROOT Tue Jun 26 17:22:43 2018 +0200
+++ b/src/HOL/ROOT Tue Jun 26 19:29:14 2018 +0200
@@ -58,7 +58,7 @@
document_files "root.bib" "root.tex"
session "HOL-Analysis" (main timing) in Analysis = HOL +
- options [document_tags = "unimportant",
+ options [document_tags = "%unimportant",
document_variants = "document:manual=-proof,-ML,-unimportant"]
sessions
"HOL-Library"
--- a/src/Pure/Isar/toplevel.ML Tue Jun 26 17:22:43 2018 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Jun 26 19:29:14 2018 +0200
@@ -21,6 +21,7 @@
val theory_of: state -> theory
val proof_of: state -> Proof.state
val proof_position_of: state -> int
+ val is_end_theory: state -> bool
val end_theory: Position.T -> state -> theory
val presentation_context: state -> Proof.context
val presentation_state: Proof.context -> state
@@ -165,6 +166,9 @@
Proof (prf, _) => Proof_Node.position prf
| _ => ~1);
+fun is_end_theory (State (NONE, SOME (Theory (Context.Theory _, _)))) = true
+ | is_end_theory _ = false;
+
fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
| end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
| end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);
--- a/src/Pure/Pure.thy Tue Jun 26 17:22:43 2018 +0200
+++ b/src/Pure/Pure.thy Tue Jun 26 19:29:14 2018 +0200
@@ -86,7 +86,7 @@
"prop" "term" "typ" "print_codesetup" "unused_thms" :: diag
and "print_state" :: diag
and "welcome" :: diag
- and "end" :: thy_end % "theory"
+ and "end" :: thy_end
and "realizers" :: thy_decl
and "realizability" :: thy_decl
and "extract_type" "extract" :: thy_decl
--- a/src/Pure/Thy/present.ML Tue Jun 26 17:22:43 2018 +0200
+++ b/src/Pure/Thy/present.ML Tue Jun 26 19:29:14 2018 +0200
@@ -9,7 +9,7 @@
val get_bibtex_entries: theory -> string list
val theory_qualifier: theory -> string
val document_option: Options.T -> {enabled: bool, disabled: bool}
- val document_variants: string -> (string * string) list
+ val document_variants: Options.T -> (string * string) list
val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
(Path.T * Path.T) list -> Path.T -> string * string -> bool -> unit
val finish: unit -> unit
@@ -148,14 +148,14 @@
| "false" => {enabled = false, disabled = true}
| _ => {enabled = true, disabled = false});
-fun document_variants str =
+fun document_variants options =
let
- fun read_variant s =
- (case space_explode "=" s of
- [name] => (name, "")
- | [name, tags] => (name, tags)
- | _ => error ("Malformed document variant specification: " ^ quote s));
- val variants = map read_variant (space_explode ":" str);
+ val variants =
+ space_explode ":" (Options.string options "document_variants") |> map (fn s =>
+ (case space_explode "=" s of
+ [name] => (name, "")
+ | [name, tags] => (name, tags)
+ | _ => error ("Malformed document variant specification: " ^ quote s)));
val _ =
(case duplicates (op =) (map #1 variants) of
[] => ()
--- a/src/Pure/Thy/thy_info.ML Tue Jun 26 17:22:43 2018 +0200
+++ b/src/Pure/Thy/thy_info.ML Tue Jun 26 19:29:14 2018 +0200
@@ -56,7 +56,7 @@
if exists (Toplevel.is_skipped_proof o #state) segments then ()
else
let
- val body = Thy_Output.present_thy thy segments;
+ val body = Thy_Output.present_thy options thy segments;
val option = Present.document_option options;
in
if #disabled option then ()
--- a/src/Pure/Thy/thy_output.ML Tue Jun 26 17:22:43 2018 +0200
+++ b/src/Pure/Thy/thy_output.ML Tue Jun 26 19:29:14 2018 +0200
@@ -11,7 +11,7 @@
val output_token: Proof.context -> Token.T -> Latex.text list
val output_source: Proof.context -> string -> Latex.text list
type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state}
- val present_thy: theory -> segment list -> Latex.text list
+ val present_thy: Options.T -> theory -> segment list -> Latex.text list
val pretty_term: Proof.context -> term -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
val lines: Latex.text list -> Latex.text list
@@ -239,9 +239,45 @@
fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
+fun read_tag s =
+ (case space_explode "%" s of
+ ["", b] => (SOME b, NONE)
+ | [a, b] => (NONE, SOME (a, b))
+ | _ => error ("Bad document_tags specification: " ^ quote s));
+
in
-fun present_span thy keywords document_tags span state state'
+fun make_command_tag options keywords =
+ let
+ val document_tags =
+ map read_tag (space_explode "," (Options.string options \<^system_option>\<open>document_tags\<close>));
+ val document_tags_default = map_filter #1 document_tags;
+ val document_tags_command = map_filter #2 document_tags;
+ in
+ fn {cmd_name, cmd_tags, tag, active_tag} => fn state => fn state' =>
+ let
+ val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
+
+ val keyword_tags =
+ if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"]
+ else Keyword.command_tags keywords cmd_name;
+ val command_tags =
+ the_list (AList.lookup (op =) document_tags_command cmd_name) @
+ keyword_tags @ document_tags_default;
+
+ val active_tag' =
+ if is_some tag' then tag'
+ else
+ (case command_tags of
+ default_tag :: _ => SOME default_tag
+ | [] =>
+ if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
+ then active_tag
+ else NONE);
+ in {tag' = tag', active_tag' = active_tag'} end
+ end;
+
+fun present_span thy command_tag span state state'
(tag_stack, active_tag, newline, latex, present_cont) =
let
val ctxt' =
@@ -255,23 +291,13 @@
val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
val (tag, tags) = tag_stack;
- val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
+ val {tag', active_tag'} =
+ command_tag {cmd_name = cmd_name, cmd_tags = cmd_tags, tag = tag, active_tag = active_tag}
+ state state';
+ val edge = (active_tag, active_tag');
val nesting = Toplevel.level state' - Toplevel.level state;
- val active_tag' =
- 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 @ document_tags of
- default_tag :: _ => SOME default_tag
- | [] =>
- if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
- then active_tag
- else NONE);
-
- val edge = (active_tag, active_tag');
-
val newline' =
if is_none active_tag' then span_newline else newline;
@@ -341,7 +367,7 @@
type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state};
-fun present_thy thy (segments: segment list) =
+fun present_thy options thy (segments: segment list) =
let
val keywords = Thy_Header.get_keywords thy;
@@ -422,11 +448,10 @@
(* present commands *)
- val document_tags = space_explode "," (Options.default_string \<^system_option>\<open>document_tags\<close>);
+ val command_tag = make_command_tag options keywords;
fun present_command tr span st st' =
- Toplevel.setmp_thread_position tr
- (present_span thy keywords document_tags span st st');
+ Toplevel.setmp_thread_position tr (present_span thy command_tag span st st');
fun present _ [] = I
| present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
--- a/src/Pure/Tools/build.ML Tue Jun 26 17:22:43 2018 +0200
+++ b/src/Pure/Tools/build.ML Tue Jun 26 19:29:14 2018 +0200
@@ -208,7 +208,7 @@
browser_info
(Options.default_string "document")
(Options.default_string "document_output")
- (Present.document_variants (Options.default_string "document_variants"))
+ (Present.document_variants (Options.default ()))
document_files
graph_file
parent_name