# HG changeset patch # User wenzelm # Date 1530034154 -7200 # Node ID 0854edc4d415b4fad6d8751cafa74702fa79e71f # Parent a8ada04583e7637566dca2cce78e69e4c373b453# Parent b20980997cd205d0cdf0f721eeb5e0af1831d9db merged diff -r a8ada04583e7 -r 0854edc4d415 NEWS --- 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 diff -r a8ada04583e7 -r 0854edc4d415 src/Doc/Isar_Ref/Inner_Syntax.thy --- 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} \} - 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>\true\ (intended for Boolean properties). The following standard block properties are supported: diff -r a8ada04583e7 -r 0854edc4d415 src/Doc/System/Environment.thy --- 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>\java\ - 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>\-Xms1g -Xmx4g\. \ diff -r a8ada04583e7 -r 0854edc4d415 src/Doc/System/Server.thy --- 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>\"HOL.Nat"\) and session name (e.g.\ \<^verbatim>\"HOL"\). Note that some rare theory names lack a proper session prefix, - e.g. theory \<^verbatim>\"Main"\ in session \<^verbatim>\"HOL"\. + e.g.\ theory \<^verbatim>\"Main"\ in session \<^verbatim>\"HOL"\. \<^item> \<^bold>\type\~\timing = {elapsed: double, cpu: double, gc: double}\ refers to common Isabelle timing information in seconds, usually with a precision of diff -r a8ada04583e7 -r 0854edc4d415 src/Doc/System/Sessions.thy --- 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>\ROOT\). + \<^item> @{system_option_def "document_tags"} specifies alternative command tags + as a comma-separated list of items: either ``\command\\<^verbatim>\%\\tag\'' for a + specific command, or ``\<^verbatim>\%\\tag\'' as default for all other commands. This + is occasionally useful to control the global visibility of commands via + session options (e.g.\ in \<^verbatim>\ROOT\). \<^item> @{system_option_def "threads"} determines the number of worker threads for parallel checking of theories and proofs. The default \0\ 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. diff -r a8ada04583e7 -r 0854edc4d415 src/Doc/manual.bib --- 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}, diff -r a8ada04583e7 -r 0854edc4d415 src/HOL/ROOT --- 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" diff -r a8ada04583e7 -r 0854edc4d415 src/Pure/Isar/toplevel.ML --- 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); diff -r a8ada04583e7 -r 0854edc4d415 src/Pure/Pure.thy --- 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 diff -r a8ada04583e7 -r 0854edc4d415 src/Pure/Thy/present.ML --- 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 [] => () diff -r a8ada04583e7 -r 0854edc4d415 src/Pure/Thy/thy_info.ML --- 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 () diff -r a8ada04583e7 -r 0854edc4d415 src/Pure/Thy/thy_output.ML --- 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>\document_tags\)); + 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>\document_tags\); + 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; diff -r a8ada04583e7 -r 0854edc4d415 src/Pure/Tools/build.ML --- 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