# HG changeset patch # User wenzelm # Date 1637952261 -3600 # Node ID 5280c02f29dccf0a640f5f7e87b2275c34cea001 # Parent ba59c691b3ee1d4e67df1f8c41a77810c700846a# Parent c5ce1e2f26ab0c52ec06177eb325397848d81b34 merged diff -r ba59c691b3ee -r 5280c02f29dc .hgtags --- a/.hgtags Thu Nov 25 14:02:51 2021 +0100 +++ b/.hgtags Fri Nov 26 19:44:21 2021 +0100 @@ -42,3 +42,4 @@ 81cc8f2ea9e720a68f0ba96e2b8d8e98a5ff3152 Isabelle2021-1-RC1 b92b5a57521b27cf592b835caa8e8d73e05070d2 Isabelle2021-1-RC2 2b212c8138a57096487461fa353386f753ff7a11 Isabelle2021-1-RC3 +2336356d4180b948eb9070f3f9f8986cda7e8f76 Isabelle2021-1-RC4 diff -r ba59c691b3ee -r 5280c02f29dc Admin/components/components.sha1 --- a/Admin/components/components.sha1 Thu Nov 25 14:02:51 2021 +0100 +++ b/Admin/components/components.sha1 Fri Nov 26 19:44:21 2021 +0100 @@ -96,6 +96,7 @@ d94e6da7299004890c04a7b395a3f2d381a3281e flatlaf-1.0-rc3.tar.gz 7ca3e6a8c9bd837990e64d89e7fa07a7e7cf78ff flatlaf-1.0.tar.gz 9908e5ab721f1c0035c0ab04dc7ad0bd00a8db27 flatlaf-1.2.tar.gz +9534b721b7b78344f3225067ee4df28a5440b87e flatlaf-1.6.4.tar.gz 212a0f1f867511722024cc60156fd71872a16f92 flatlaf-1.6.tar.gz f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.tar.gz 71259aa46134e6cf2c6473b4fc408051b3336490 gnu-utils-20211030.tar.gz @@ -333,6 +334,7 @@ 0f1c903b043acf7b221821d8b6374b3f943a122b polyml-5.9-610a153b941d.tar.gz 5f00a47b8f5180b33e68fcc6c343b061957a0a98 polyml-5.9-960de0cd0795.tar.gz 7056b285af67902b32f5049349a064f073f05860 polyml-5.9-cc80e2b43c38.tar.gz +0c396bd6b46ff11a2432b91aab2be0248bd9b0a4 polyml-5.9.tar.gz 49f1adfacdd6d29fa9f72035d94a31eaac411a97 polyml-test-0a6ebca445fc.tar.gz 2a8c4421e0a03c0d6ad556b3c36c34eb11568adb polyml-test-1236652ebd55.tar.gz 8e83fb5088cf265902b8da753a8eac5fe3f6a14b polyml-test-159dc81efc3b.tar.gz @@ -436,6 +438,7 @@ d33e1e36139e86b9e9a48d8b46a6f90d7863a51c verit-2021.06-rmx-1.tar.gz c11d1120fcefaec79f099fe2be05b03cd2aed8b9 verit-2021.06-rmx.tar.gz b576fd5d89767c1067541d4839fb749c6a68d22c verit-2021.06.1-rmx.tar.gz +19c6e5677b0a26cbc5805da79d00d06a66b7a671 verit-2021.06.2-rmx.tar.gz 81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz fe15e1079cf5ad86f3cbab4553722a0d20002d11 windows_app-20130905.tar.gz e6a43b7b3b21295853bd2a63b27ea20bd6102f5f windows_app-20130906.tar.gz diff -r ba59c691b3ee -r 5280c02f29dc Admin/components/main --- a/Admin/components/main Thu Nov 25 14:02:51 2021 +0100 +++ b/Admin/components/main Fri Nov 26 19:44:21 2021 +0100 @@ -5,7 +5,7 @@ csdp-6.1.1 cvc4-1.8 e-2.6-1 -flatlaf-1.6 +flatlaf-1.6.4 idea-icons-20210508 isabelle_fonts-20211004 isabelle_setup-20211109 @@ -17,7 +17,7 @@ minisat-2.2.1-1 nunchaku-0.5 opam-2.0.7 -polyml-5.9-610a153b941d +polyml-5.9 postgresql-42.2.24 scala-2.13.5 smbc-0.4.1 @@ -26,7 +26,7 @@ ssh-java-20190323 stack-2.7.3 vampire-4.6 -verit-2021.06.1-rmx +verit-2021.06.2-rmx xz-java-1.9 z3-4.4.0_4.4.1 zipperposition-2.1-1 diff -r ba59c691b3ee -r 5280c02f29dc Admin/polyml/README --- a/Admin/polyml/README Thu Nov 25 14:02:51 2021 +0100 +++ b/Admin/polyml/README Fri Nov 26 19:44:21 2021 +0100 @@ -3,8 +3,8 @@ This compilation of Poly/ML (https://www.polyml.org) is based on the source distribution from -https://github.com/polyml/polyml/commit/610a153b941d (shortly before -official version 5.9). +https://github.com/polyml/polyml/commit/39d96a2def90 (official release +5.9 with minimal additions fixes-5.9). The Isabelle repository provides an administrative tool "isabelle build_polyml", which can be used in the polyml component directory as @@ -55,4 +55,4 @@ Makarius - 14-Nov-2021 + 26-Nov-2021 diff -r ba59c691b3ee -r 5280c02f29dc NEWS --- a/NEWS Thu Nov 25 14:02:51 2021 +0100 +++ b/NEWS Fri Nov 26 19:44:21 2021 +0100 @@ -129,9 +129,18 @@ explicitly requires document_build=build. Minor INCOMPATIBILITY, need to adjust session ROOT options. +* Option "document_comment_latex" enables regular LaTeX comment.sty, +instead of the historic version for plain TeX (default). The latter is +much faster, but in conflict with LaTeX classes like Dagstuhl LIPIcs. + * Option "document_echo" informs about document file names during session presentation. +* Option "document_heading_prefix" specifies a prefix for the LaTeX +macro names generated from document heading commands like 'chapter', +'section' etc. The default is "isamarkup", so 'section' becomes +"\isamarkupsection" for example. + * The command-line tool "isabelle latex" has been discontinued, INCOMPATIBILITY for old document build scripts. @@ -217,6 +226,24 @@ min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4. Minor INCOMPATIBILITY. +* The Mirabelle testing tool is now part of Main HOL, and accessible via +the command-line tool "isabelle mirabelle" (implemented in +Isabelle/Scala). It has become more robust and supports parallelism +within Isabelle/ML. + +* Nitpick: External solver "MiniSat" is available for all supported +Isabelle platforms (including 64bit Windows and ARM); while +"MiniSat_JNI" only works for Intel Linux and macOS. + +* Nitpick/Kodkod: default is back to external Java process (option +kodkod_scala = false), both for PIDE and batch builds. This reduces +confusion and increases robustness of timeouts, despite substantial +overhead to run an external JVM. For more fine-grained control, the +kodkod_scala option can be modified within the formal theory context +like this: + + declare [[kodkod_scala = false]] + * Sledgehammer: - Update of bundled provers: . E 2.6 @@ -224,7 +251,7 @@ . veriT 2021.06.1-rmx . Zipperposition 2.1 . Z3 4.4.1 for arm64-linux, which approximates Z3 4.4.0pre, - but sometimes failes or crashes + but sometimes fails or crashes - Adjusted default provers: cvc4 vampire verit e spass z3 zipperposition - Adjusted Zipperposition's slicing. @@ -242,10 +269,6 @@ version 2.4 (release 20200713). The new version fixes one implementation defect. Very slight INCOMPATIBILITY. -* Nitpick: External solver "MiniSat" is available for all supported -Isabelle platforms (including 64bit Windows and ARM); while -"MiniSat_JNI" only works for Intel Linux and macOS. - * Theory HOL-Library.Lattice_Syntax has been superseded by bundle "lattice_syntax": it can be used in a local context via 'include' or in a global theory via 'unbundle'. The opposite declarations are bundled as @@ -408,11 +431,11 @@ syntactic order. The original order of occurrences may be recovered as well, e.g. via TFrees.list_set. -* Thm.instantiate, Thm.generalize and related operations require -scalable datastructures from structure TVars, Vars, Names etc. -INCOMPATIBILITY: e.g. use TVars.empty and TVars.make for immediate -adoption; better use TVars.add, TVars.add_tfrees etc. for scalable -accumulation of items. +* Thm.instantiate, Thm.generalize and related operations (e.g. +Variable.import) now use scalable data structures from structure TVars, +Vars, Names etc. INCOMPATIBILITY: e.g. use TVars.empty and TVars.make +for immediate adoption; better use TVars.add, TVars.add_tfrees etc. for +scalable accumulation of items. * Thm.instantiate_beta applies newly emerging abstractions to their arguments in the term, but leaves other beta-redexes unchanged --- in @@ -524,6 +547,9 @@ *** System *** +* Almost complete support for arm64-linux platform. The reference +platform is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit). + * Update to OpenJDK 17: the current long-term support version of Java. * Update to Poly/ML 5.9 with improved support for ARM on Linux. On @@ -561,17 +587,21 @@ INCOMPATIBILITY: HTTP proxy configuration now works via JVM properties https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html +* System options may declare an implicit standard value, which is used +when the option is activated without providing an explicit value, e.g. +"isabelle build -o document -o document_output" instead of +"isabelle build -o document=true -o document_output=output". For options +of type "bool", the standard is always "true" and cannot be specified +differently. + +* System option "document=true" is an alias for "document=pdf", and +"document=false" is an alias for "document=" (empty string). + * System option "system_log" specifies an optional log file for internal -messages produced by Output.system_message in Isabelle/ML; the value -"true" refers to console progress of the build job. This works for +messages produced by Output.system_message in Isabelle/ML; the standard +value "-" refers to console progress of the build job. This works for "isabelle build" or any derivative of it. -* System options of type string may be set to "true" using the short -notation of type bool. E.g. "isabelle build -o system_log". - -* System option "document=true" is an alias for "document=pdf" and thus -can be used in the short form. E.g. "isabelle build -o document". - * Command-line tool "isabelle version" supports repository archives (without full .hg directory). It also provides more options. @@ -582,11 +612,11 @@ (native Windows) or ISABELLE_APPLE_PLATFORM64 (Apple Silicon). * Timeouts for Isabelle/ML tools are subject to system option -"timeout_scale" --- this already used for the overall session build -process before, and allows to adapt to slow machines. The underlying -Timeout.apply in Isabelle/ML treats an original timeout specification 0 -as no timeout; before it meant immediate timeout. Rare INCOMPATIBILITY -in boundary cases. +"timeout_scale", to support adjustments to slow machines. Before, +timeout_scale was only used for the overall session build process, now +it affects the underlying Timeout.apply in Isabelle/ML as well. It +treats a timeout specification 0 as "no timeout", instead of "immediate +timeout". Rare INCOMPATIBILITY in boundary cases. @@ -961,8 +991,8 @@ /usr/local/bin/isabelle-phabricator-upgrade and each installation root directory (e.g. /var/www/phabricator-vcs/libphutil). -* Almost complete support for arm64-linux platform. The reference -platform is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit). +* Experimental support for arm64-linux platform. The reference platform +is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit). * Support for Apple Silicon, using mostly x86_64-darwin runtime translation via Rosetta 2 (e.g. Poly/ML and external provers), but also diff -r ba59c691b3ee -r 5280c02f29dc etc/options --- a/etc/options Thu Nov 25 14:02:51 2021 +0100 +++ b/etc/options Fri Nov 26 19:44:21 2021 +0100 @@ -5,9 +5,9 @@ option browser_info : bool = false -- "generate theory browser information" -option document : string = "" +option document : string = "" (standard "true") -- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")" -option document_output : string = "" +option document_output : string = "" (standard "output") -- "document output directory" option document_echo : bool = false -- "inform about document file names during session presentation" @@ -17,10 +17,14 @@ -- "default command tags (separated by commas)" option document_bibliography : bool = false -- "explicitly enable use of bibtex (default: according to presence of root.bib)" -option document_build : string = "lualatex" - -- "document build engine (e.g. lualatex, pdflatex, build)" +option document_build : string = "lualatex" (standard "build") + -- "document build engine (e.g. build, lualatex, pdflatex)" option document_logo : string = "" -- "generate named instance of Isabelle logo (underscore means unnamed variant)" +option document_heading_prefix : string = "isamarkup" (standard) + -- "prefix for LaTeX macros generated from 'chapter', 'section' etc." +option document_comment_latex : bool = false + -- "use regular LaTeX version of comment.sty, instead of historic plain TeX version" option thy_output_display : bool = false -- "indicate output as multi-line display-style material" @@ -128,11 +132,11 @@ option process_output_tail : int = 40 -- "build process output tail shown to user (in lines, 0 = unlimited)" -option profiling : string = "" +option profiling : string = "" (standard "time") -- "ML profiling (possible values: time, allocations)" -option system_log : string = "" - -- "output for system messages (log file or \"true\" for console progress)" +option system_log : string = "" (standard "-") + -- "output for system messages (log file or \"-\" for console progress)" option system_heaps : bool = false -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" diff -r ba59c691b3ee -r 5280c02f29dc lib/texinputs/isabelle.sty --- a/lib/texinputs/isabelle.sty Thu Nov 25 14:02:51 2021 +0100 +++ b/lib/texinputs/isabelle.sty Fri Nov 26 19:44:21 2021 +0100 @@ -275,29 +275,8 @@ \newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}} -% tagged regions - -%plain TeX version of comment package -- much faster! -\let\isafmtname\fmtname\def\fmtname{plain} -\usepackage{comment} -\let\fmtname\isafmtname +% tags \newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}} -\newcommand{\isakeeptag}[1]% -{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}} -\newcommand{\isadroptag}[1]% -{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}} -\newcommand{\isafoldtag}[1]% -{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}} - -\isakeeptag{document} -\isakeeptag{theory} -\isakeeptag{proof} -\isakeeptag{ML} -\isakeeptag{visible} -\isadroptag{invisible} -\isakeeptag{important} -\isakeeptag{unimportant} - \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{} diff -r ba59c691b3ee -r 5280c02f29dc src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Doc/System/Sessions.thy Fri Nov 26 19:44:21 2021 +0100 @@ -273,8 +273,8 @@ \<^item> @{system_option_def system_log} specifies an optional log file for low-level messages produced by \<^ML>\Output.system_message\ in - Isabelle/ML; the value ``\<^verbatim>\true\'' refers to console progress of the build - job. + Isabelle/ML; the standard value ``\<^verbatim>\-\'' refers to console progress of the + build job. \<^item> @{system_option_def "system_heaps"} determines the directories for session heap images: \<^path>\$ISABELLE_HEAPS\ is the user directory and diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Library/Tools/smt_word.ML --- a/src/HOL/Library/Tools/smt_word.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Library/Tools/smt_word.ML Fri Nov 26 19:44:21 2021 +0100 @@ -19,14 +19,17 @@ (* "QF_AUFBV" is too restrictive for Isabelle's problems, which contain aritmetic and quantifiers. Better set the logic to "" and make at least Z3 happy. *) -fun smtlib_logic ts = - if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE +fun smtlib_logic "z3" ts = + if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE + | smtlib_logic "verit" _ = NONE + | smtlib_logic _ ts = + if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "AUFBVLIRA" else NONE (* SMT-LIB builtins *) local - val smtlibC = SMTLIB_Interface.smtlibC + val smtlibC = SMTLIB_Interface.smtlibC @ SMTLIB_Interface.bvsmlibC val wordT = \<^typ>\'a::len word\ diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Nitpick_Examples/Tests_Nits.thy --- a/src/HOL/Nitpick_Examples/Tests_Nits.thy Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy Fri Nov 26 19:44:21 2021 +0100 @@ -11,6 +11,6 @@ imports Main begin -ML \() |> getenv "KODKODI" <> "" ? Nitpick_Tests.run_all_tests\ +ML \if getenv "KODKODI" = "" then () else Nitpick_Tests.run_all_tests \<^context>\ end diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Nitpick_Examples/minipick.ML --- a/src/HOL/Nitpick_Examples/minipick.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Nitpick_Examples/minipick.ML Fri Nov 26 19:44:21 2021 +0100 @@ -395,11 +395,12 @@ fun solve_any_kodkod_problem thy problems = let val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params thy [] + val kodkod_scala = Config.get_global thy Kodkod.kodkod_scala val deadline = Timeout.end_time timeout val max_threads = 1 val max_solutions = 1 in - case solve_any_problem debug overlord deadline max_threads max_solutions + case solve_any_problem kodkod_scala debug overlord deadline max_threads max_solutions problems of Normal ([], _, _) => "none" | Normal _ => "genuine" diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Fri Nov 26 19:44:21 2021 +0100 @@ -166,7 +166,8 @@ val is_problem_trivially_false : problem -> bool val problems_equivalent : problem * problem -> bool val solve_any_problem : - bool -> bool -> Time.time -> int -> int -> problem list -> outcome + bool -> bool -> bool -> Time.time -> int -> int -> problem list -> outcome + val kodkod_scala : bool Config.T end; structure Kodkod : KODKOD = @@ -958,7 +959,7 @@ is partly due to the JVM and partly due to the ML "bash" function. *) val fudge_ms = 250 -fun uncached_solve_any_problem overlord deadline max_threads0 max_solutions problems = +fun uncached_solve_any_problem kodkod_scala overlord deadline max_threads0 max_solutions problems = let val j = find_index (curry (op =) True o #formula) problems val indexed_problems = if j >= 0 then @@ -975,8 +976,7 @@ then Options.default_int \<^system_option>\kodkod_max_threads\ else max_threads0 - val external_process = - not (Options.default_bool \<^system_option>\kodkod_scala\) orelse overlord + val external_process = not kodkod_scala orelse overlord val timeout0 = Time.toMilliseconds (deadline - Time.now ()) val timeout = if external_process then timeout0 - fudge_ms else timeout0 @@ -1058,11 +1058,11 @@ Synchronized.var "Kodkod.cached_outcome" (NONE : ((int * problem list) * outcome) option) -fun solve_any_problem debug overlord deadline max_threads max_solutions +fun solve_any_problem kodkod_scala debug overlord deadline max_threads max_solutions problems = let fun do_solve () = - uncached_solve_any_problem overlord deadline max_threads max_solutions + uncached_solve_any_problem kodkod_scala overlord deadline max_threads max_solutions problems in if debug orelse overlord then @@ -1085,4 +1085,6 @@ end end +val kodkod_scala = Attrib.setup_option_bool (\<^system_option>\kodkod_scala\, \<^here>) + end; diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Nov 26 19:44:21 2021 +0100 @@ -692,6 +692,7 @@ fun solve_any_problem (found_really_genuine, max_potential, max_genuine, donno) first_time problems = let + val kodkod_scala = Config.get ctxt KK.kodkod_scala val max_potential = Int.max (0, max_potential) val max_genuine = Int.max (0, max_genuine) fun print_and_check genuine (j, bounds) = @@ -702,7 +703,7 @@ if max_solutions <= 0 then (found_really_genuine, 0, 0, donno) else - case KK.solve_any_problem debug overlord deadline max_threads + case KK.solve_any_problem kodkod_scala debug overlord deadline max_threads max_solutions (map fst problems) of KK.Normal ([], unsat_js, s) => (update_checked_problems problems unsat_js; show_kodkod_warning s; diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Nov 26 19:44:21 2021 +0100 @@ -7,7 +7,7 @@ signature NITPICK_TESTS = sig - val run_all_tests : unit -> unit + val run_all_tests : Proof.context -> unit end; structure Nitpick_Tests : NITPICK_TESTS = @@ -208,15 +208,17 @@ formula = formula} end -fun run_all_tests () = +fun run_all_tests ctxt = let - val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params \<^theory> [] + val thy = Proof_Context.theory_of ctxt + val {debug, overlord, timeout, ...} = Nitpick_Commands.default_params thy [] + val kodkod_scala = Config.get ctxt Kodkod.kodkod_scala val deadline = Timeout.end_time timeout val max_threads = 1 val max_solutions = 1 in - case Kodkod.solve_any_problem debug overlord deadline max_threads max_solutions - (map (problem_for_nut \<^context>) tests) of + case Kodkod.solve_any_problem kodkod_scala debug overlord deadline max_threads max_solutions + (map (problem_for_nut ctxt) tests) of Kodkod.Normal ([], _, _) => () | _ => error "Tests failed" end diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Tools/SMT/cvc4_interface.ML --- a/src/HOL/Tools/SMT/cvc4_interface.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Tools/SMT/cvc4_interface.ML Fri Nov 26 19:44:21 2021 +0100 @@ -23,7 +23,7 @@ local fun translate_config order ctxt = {order = order, - logic = K "(set-logic ALL_SUPPORTED)\n", + logic = K (K "(set-logic ALL_SUPPORTED)\n"), fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP], serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)} in diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Tools/SMT/smt_config.ML --- a/src/HOL/Tools/SMT/smt_config.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Tools/SMT/smt_config.ML Fri Nov 26 19:44:21 2021 +0100 @@ -34,6 +34,7 @@ val monomorph_instances: int Config.T val explicit_application: int Config.T val higher_order: bool Config.T + val native_bv: bool Config.T val nat_as_int: bool Config.T val infer_triggers: bool Config.T val debug_files: string Config.T @@ -194,6 +195,7 @@ val monomorph_instances = Attrib.setup_config_int \<^binding>\smt_monomorph_instances\ (K 500) val explicit_application = Attrib.setup_config_int \<^binding>\smt_explicit_application\ (K 1) val higher_order = Attrib.setup_config_bool \<^binding>\smt_higher_order\ (K false) +val native_bv = Attrib.setup_config_bool \<^binding>\native_bv\ (K true) val nat_as_int = Attrib.setup_config_bool \<^binding>\smt_nat_as_int\ (K false) val infer_triggers = Attrib.setup_config_bool \<^binding>\smt_infer_triggers\ (K false) val debug_files = Attrib.setup_config_string \<^binding>\smt_debug_files\ (K "") diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Tools/SMT/smt_real.ML --- a/src/HOL/Tools/SMT/smt_real.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Tools/SMT/smt_real.ML Fri Nov 26 19:44:21 2021 +0100 @@ -10,7 +10,7 @@ (* SMT-LIB logic *) -fun smtlib_logic ts = +fun smtlib_logic _ ts = if exists (Term.exists_type (Term.exists_subtype (equal \<^typ>\real\))) ts then SOME "AUFLIRA" else NONE diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Fri Nov 26 19:44:21 2021 +0100 @@ -132,7 +132,7 @@ val (str, replay_data as {context = ctxt', ...}) = ithms |> tap (trace_assms ctxt) - |> SMT_Translate.translate ctxt smt_options comments + |> SMT_Translate.translate ctxt name smt_options comments ||> tap trace_replay_data in (run_solver ctxt' name (make_command command options) str, replay_data) end diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Tools/SMT/smt_systems.ML --- a/src/HOL/Tools/SMT/smt_systems.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Tools/SMT/smt_systems.ML Fri Nov 26 19:44:21 2021 +0100 @@ -77,6 +77,8 @@ else if Config.get ctxt SMT_Config.higher_order then SMTLIB_Interface.hosmtlibC + else if Config.get ctxt SMT_Config.native_bv then + SMTLIB_Interface.bvsmlibC else SMTLIB_Interface.smtlibC in @@ -147,7 +149,9 @@ ["-smt2"] fun select_class ctxt = - if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C else SMTLIB_Interface.smtlibC + if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C + else if Config.get ctxt SMT_Config.native_bv then SMTLIB_Interface.bvsmlibC + else SMTLIB_Interface.smtlibC in val z3: SMT_Solver.solver_config = { diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Tools/SMT/smt_translate.ML Fri Nov 26 19:44:21 2021 +0100 @@ -22,7 +22,7 @@ funcs: (string * (string list * string)) list } type config = { order: SMT_Util.order, - logic: term list -> string, + logic: string -> term list -> string, fp_kinds: BNF_Util.fp_kind list, serialize: (string * string) list -> string list -> sign -> sterm list -> string } type replay_data = { @@ -35,7 +35,7 @@ (*translation*) val add_config: SMT_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic - val translate: Proof.context -> (string * string) list -> string list -> (int * thm) list -> + val translate: Proof.context -> string -> (string * string) list -> string list -> (int * thm) list -> string * replay_data end; @@ -66,7 +66,7 @@ type config = { order: SMT_Util.order, - logic: term list -> string, + logic: string -> term list -> string, fp_kinds: BNF_Util.fp_kind list, serialize: (string * string) list -> string list -> sign -> sterm list -> string } @@ -487,7 +487,7 @@ "for solver class " ^ quote (SMT_Util.string_of_class cs))) end -fun translate ctxt smt_options comments ithms = +fun translate ctxt prover smt_options comments ithms = let val {order, logic, fp_kinds, serialize} = get_config ctxt @@ -529,7 +529,7 @@ |>> order = SMT_Util.First_Order ? apfst (cons fun_app_eq) in (ts4, tr_context) - |-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2 + |-> intermediate (logic prover) dtyps (builtin SMT_Builtin.dest_builtin) ctxt2 |>> uncurry (serialize smt_options comments) ||> replay_data_of ctxt2 ll_defs rewrite_rules ithms end diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Tools/SMT/smtlib_interface.ML --- a/src/HOL/Tools/SMT/smtlib_interface.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Fri Nov 26 19:44:21 2021 +0100 @@ -9,7 +9,9 @@ sig val smtlibC: SMT_Util.class val hosmtlibC: SMT_Util.class - val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic + val bvsmlibC: SMT_Util.class + val add_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic + val del_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config val assert_name_of_index: int -> string val assert_index_of_name: string -> int @@ -23,7 +25,7 @@ val smtlibC = ["smtlib"] (* SMT-LIB 2 *) val hosmtlibC = smtlibC @ hoC (* possibly SMT-LIB 3 *) - +val bvsmlibC = smtlibC @ ["BV"] (* if BV are supported *) (* builtins *) @@ -73,17 +75,18 @@ structure Logics = Generic_Data ( - type T = (int * (term list -> string option)) list + type T = (int * (string -> term list -> string option)) list val empty = [] fun merge data = Ord_List.merge fst_int_ord data ) fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf) +fun del_logic pf = Logics.map (Ord_List.remove fst_int_ord pf) -fun choose_logic ctxt ts = +fun choose_logic ctxt prover ts = let fun choose [] = "AUFLIA" - | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs) + | choose ((_, f) :: fs) = (case f prover ts of SOME s => s | NONE => choose fs) in (case choose (Logics.get (Context.Proof ctxt)) of "" => "" (* for default Z3 logic, a subset of everything *) diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Tools/SMT/verit_proof.ML --- a/src/HOL/Tools/SMT/verit_proof.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Tools/SMT/verit_proof.ML Fri Nov 26 19:44:21 2021 +0100 @@ -174,7 +174,8 @@ map fst strategies end -fun verit_tac ctxt = SMT_Solver.smt_tac (Context.proof_map (SMT_Config.select_solver "verit") ctxt) +val select_verit = SMT_Config.select_solver "verit" +fun verit_tac ctxt = SMT_Solver.smt_tac (Config.put SMT_Config.native_bv false ((Context.proof_map select_verit ctxt))) fun verit_tac_stgy stgy ctxt = verit_tac (Context.proof_of (select_veriT_stgy stgy (Context.Proof ctxt))) datatype raw_veriT_node = Raw_VeriT_Node of { diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Tools/SMT/z3_interface.ML --- a/src/HOL/Tools/SMT/z3_interface.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Tools/SMT/z3_interface.ML Fri Nov 26 19:44:21 2021 +0100 @@ -26,7 +26,7 @@ val z3C = ["z3"] -val smtlib_z3C = SMTLIB_Interface.smtlibC @ z3C +val smtlib_z3C = SMTLIB_Interface.smtlibC @ SMTLIB_Interface.bvsmlibC @ z3C (* interface *) @@ -34,7 +34,7 @@ local fun translate_config ctxt = {order = SMT_Util.First_Order, - logic = K "", + logic = K (K ""), fp_kinds = [BNF_Util.Least_FP], serialize = #serialize (SMTLIB_Interface.translate_config SMT_Util.First_Order ctxt)} diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/Tools/etc/options --- a/src/HOL/Tools/etc/options Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/Tools/etc/options Fri Nov 26 19:44:21 2021 +0100 @@ -38,7 +38,7 @@ public option MaSh : string = "sml" -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)" -public option kodkod_scala : bool = true +public option kodkod_scala : bool = false -- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)" public option kodkod_max_threads : int = 0 diff -r ba59c691b3ee -r 5280c02f29dc src/HOL/ex/Cartouche_Examples.thy --- a/src/HOL/ex/Cartouche_Examples.thy Thu Nov 25 14:02:51 2021 +0100 +++ b/src/HOL/ex/Cartouche_Examples.thy Fri Nov 26 19:44:21 2021 +0100 @@ -5,10 +5,8 @@ section \Some examples with text cartouches\ theory Cartouche_Examples -imports Main -keywords - "cartouche" :: diag and - "text_cartouche" :: thy_decl + imports Main + keywords "cartouche" :: diag begin subsection \Regular outer syntax\ @@ -135,14 +133,7 @@ subsubsection \Uniform nesting of sub-languages: document source, ML, term, string literals\ -ML \ - Outer_Syntax.command - \<^command_keyword>\text_cartouche\ "" - (Parse.opt_target -- Parse.input Parse.cartouche - >> Pure_Syn.document_command {markdown = true}) -\ - -text_cartouche +text \ \<^ML>\ ( diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Admin/build_doc.scala --- a/src/Pure/Admin/build_doc.scala Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Admin/build_doc.scala Fri Nov 26 19:44:21 2021 +0100 @@ -52,6 +52,7 @@ { case (doc, session) => try { + progress.expose_interrupt() progress.echo("Documentation " + quote(doc) + " ...") using(store.open_database_context())(db_context => diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Admin/build_release.scala Fri Nov 26 19:44:21 2021 +0100 @@ -823,9 +823,6 @@ val other_isabelle = context.other_isabelle(tmp_dir) - Isabelle_System.make_directory(other_isabelle.etc) - File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n") - other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs + " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" + " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Admin/build_verit.scala --- a/src/Pure/Admin/build_verit.scala Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Admin/build_verit.scala Fri Nov 26 19:44:21 2021 +0100 @@ -9,7 +9,7 @@ object Build_VeriT { - val default_download_url = "https://verit.loria.fr/rmx/2021.06/verit-2021.06-rmx.tar.gz" + val default_download_url = "https://verit.loria.fr/rmx/2021.06.2/verit-2021.06.2-rmx.tar.gz" /* build veriT */ diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/General/file.scala --- a/src/Pure/General/file.scala Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/General/file.scala Fri Nov 26 19:44:21 2021 +0100 @@ -292,4 +292,36 @@ else if (Platform.is_windows) Isabelle_System.chmod("a-x", path) else path.file.setExecutable(flag, false) } + + + /* content */ + + object Content + { + def apply(path: Path, content: Bytes): Content = new Content_Bytes(path, content) + def apply(path: Path, content: String): Content = new Content_String(path, content) + def apply(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content) + } + + trait Content + { + def path: Path + def write(dir: Path): Unit + } + + final class Content_Bytes private[File](val path: Path, content: Bytes) extends Content + { + def write(dir: Path): Unit = Bytes.write(dir + path, content) + } + + final class Content_String private[File](val path: Path, content: String) extends Content + { + def write(dir: Path): Unit = File.write(dir + path, content) + } + + final class Content_XML private[File](val path: Path, content: XML.Body) + { + def output(out: XML.Body => String): Content_String = + new Content_String(path, out(content)) + } } diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Isar/token.ML Fri Nov 26 19:44:21 2021 +0100 @@ -31,7 +31,8 @@ Fact of string option * thm list | Attribute of morphism -> attribute | Declaration of declaration | - Files of file Exn.result list + Files of file Exn.result list | + Output of XML.body option val pos_of: T -> Position.T val adjust_offsets: (int -> int option) -> T -> T val eof: T @@ -73,6 +74,8 @@ val file_source: file -> Input.source val get_files: T -> file Exn.result list val put_files: file Exn.result list -> T -> T + val get_output: T -> XML.body option + val put_output: XML.body -> T -> T val get_value: T -> value option val reports_of_value: T -> Position.report list val name_value: name_value -> value @@ -197,7 +200,8 @@ Fact of string option * thm list | (*optional name for dynamic fact, i.e. fact "variable"*) Attribute of morphism -> attribute | Declaration of declaration | - Files of file Exn.result list; + Files of file Exn.result list | + Output of XML.body option; type src = T list; @@ -411,6 +415,15 @@ | put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok)); +(* document output *) + +fun get_output (Token (_, _, Value (SOME (Output output)))) = output + | get_output _ = NONE; + +fun put_output output (Token (x, y, Slot)) = Token (x, y, Value (SOME (Output (SOME output)))) + | put_output _ tok = raise Fail ("Cannot put document output here" ^ Position.here (pos_of tok)); + + (* access values *) fun get_value (Token (_, _, Value v)) = v @@ -491,7 +504,8 @@ | Fact (a, ths) => Fact (a, Morphism.fact phi ths) | Attribute att => Attribute (Morphism.transform phi att) | Declaration decl => Declaration (Morphism.transform phi decl) - | Files _ => v)); + | Files _ => v + | Output _ => v)); (* static binding *) diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Isar/toplevel.ML Fri Nov 26 19:44:21 2021 +0100 @@ -17,6 +17,7 @@ val is_skipped_proof: state -> bool val level: state -> int val previous_theory_of: state -> theory option + val output_of: state -> Latex.text option val context_of: state -> Proof.context val generic_theory_of: state -> generic_theory val theory_of: state -> theory @@ -30,6 +31,7 @@ val pretty_state: state -> Pretty.T list val string_of_state: state -> string val pretty_abstract: state -> Pretty.T + type presentation = state -> Latex.text option type transition val empty: transition val name_of: transition -> string @@ -44,6 +46,7 @@ val is_init: transition -> bool val modify_init: (unit -> theory) -> transition -> transition val exit: transition -> transition + val present: (state -> Latex.text) -> transition -> transition val keep: (state -> unit) -> transition -> transition val keep': (bool -> state -> unit) -> transition -> transition val keep_proof: (state -> unit) -> transition -> transition @@ -62,7 +65,7 @@ (bool -> local_theory -> local_theory) -> transition -> transition val local_theory: (bool * Position.T) option -> (xstring * Position.T) option -> (local_theory -> local_theory) -> transition -> transition - val present_local_theory: (xstring * Position.T) option -> (state -> unit) -> + val present_local_theory: (xstring * Position.T) option -> (state -> Latex.text) -> transition -> transition val local_theory_to_proof': (bool * Position.T) option -> (xstring * Position.T) option -> (bool -> local_theory -> Proof.state) -> transition -> transition @@ -137,20 +140,20 @@ fun node_presentation node = (node, cases_node init_presentation Context.proof_of Proof.context_of node); - datatype state = - State of node_presentation * theory option; - (*current node with presentation context, previous theory*) + State of node_presentation * (theory option * Latex.text option); + (*current node with presentation context, previous theory, document output*) fun node_of (State ((node, _), _)) = node; -fun previous_theory_of (State (_, prev_thy)) = prev_thy; +fun previous_theory_of (State (_, (prev_thy, _))) = prev_thy; +fun output_of (State (_, (_, output))) = output; -fun init_toplevel () = State (node_presentation Toplevel, NONE); -fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), NONE); +fun init_toplevel () = State (node_presentation Toplevel, (NONE, NONE)); +fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), (NONE, NONE)); val prev_theory = Config.declare_int ("prev_theory", Position.none) (K 0); fun get_prev_theory thy = Config.get_global thy prev_theory; -fun set_prev_theory (State (_, SOME prev_thy)) (Theory gthy) = +fun set_prev_theory (State (_, (SOME prev_thy, _))) (Theory gthy) = let val put = Config.put_global prev_theory (Context.theory_identifier prev_thy); val gthy' = gthy |> Context.mapping put (Local_Theory.raw_theory put); @@ -202,10 +205,10 @@ Proof (prf, _) => Proof_Node.position prf | _ => ~1); -fun is_end_theory (State ((Toplevel, _), SOME _)) = true +fun is_end_theory (State ((Toplevel, _), (SOME _, _))) = true | is_end_theory _ = false; -fun end_theory _ (State ((Toplevel, _), SOME thy)) = thy +fun end_theory _ (State ((Toplevel, _), (SOME thy, _))) = thy | end_theory pos _ = error ("Malformed theory" ^ Position.here pos); @@ -221,11 +224,11 @@ fun presentation_context (state as State (current, _)) = presentation_context0 state - |> Presentation_State.put (SOME (State (current, NONE))); + |> Presentation_State.put (SOME (State (current, (NONE, NONE)))); fun presentation_state ctxt = (case Presentation_State.get ctxt of - NONE => State (node_presentation (Theory (Context.Proof ctxt)), NONE) + NONE => State (node_presentation (Theory (Context.Proof ctxt)), (NONE, NONE)) | SOME state => state); @@ -261,6 +264,13 @@ (** toplevel transitions **) +(* presentation *) + +type presentation = state -> Latex.text option; +val no_presentation: presentation = K NONE; +fun presentation g : presentation = SOME o g; + + (* primitive transitions *) datatype trans = @@ -269,36 +279,37 @@ (*formal exit of theory*) Exit | (*peek at state*) - Keep of bool -> state -> unit | + Keep of bool -> presentation | (*node transaction and presentation*) - Transaction of (bool -> node -> node_presentation) * (state -> unit); + Transaction of (bool -> node -> node_presentation) * presentation; local exception FAILURE of state * exn; +fun apply_presentation g (st as State (node, (prev_thy, _))) = + State (node, (prev_thy, g st)); + fun apply f g node = let val node_pr = node_presentation node; val context = cases_proper_node I (Context.Proof o Proof.context_of) node; - fun state_error e node_pr' = (State (node_pr', get_theory node), e); + fun make_state node_pr' = State (node_pr', (get_theory node, NONE)); - val (result, err) = - node - |> Runtime.controlled_execution (SOME context) f - |> state_error NONE - handle exn => state_error (SOME exn) node_pr; + val (st', err) = + (Runtime.controlled_execution (SOME context) (f #> make_state #> apply_presentation g) node, + NONE) handle exn => (make_state node_pr, SOME exn); in (case err of - NONE => tap g result - | SOME exn => raise FAILURE (result, exn)) + NONE => st' + | SOME exn => raise FAILURE (st', exn)) end; fun apply_tr int trans state = (case (trans, node_of state) of (Init f, Toplevel) => Runtime.controlled_execution NONE (fn () => - State (node_presentation (Theory (Context.Theory (f ()))), NONE)) () + State (node_presentation (Theory (Context.Theory (f ()))), (NONE, NONE))) () | (Exit, node as Theory (Context.Theory thy)) => let val State ((node', pr_ctxt), _) = @@ -306,11 +317,15 @@ (fn _ => node_presentation (Theory (Context.Theory (tap Thm.expose_theory (Theory.end_theory thy))))) - (K ()); - in State ((Toplevel, pr_ctxt), get_theory node') end + no_presentation; + in State ((Toplevel, pr_ctxt), (get_theory node', NONE)) end | (Keep f, node) => Runtime.controlled_execution (try generic_theory_of state) - (fn () => (f int state; State (node_presentation node, previous_theory_of state))) () + (fn () => + let + val prev_thy = previous_theory_of state; + val state' = State (node_presentation node, (prev_thy, NONE)); + in apply_presentation (fn st => f int st) state' end) () | (Transaction _, Toplevel) => raise UNDEF | (Transaction (f, g), node) => apply (fn x => f int x) g (set_prev_theory state node) | _ => raise UNDEF); @@ -403,13 +418,14 @@ fun modify_init f tr = if is_init tr then init_theory f (reset_trans tr) else tr; val exit = add_trans Exit; -val keep' = add_trans o Keep; fun present_transaction f g = add_trans (Transaction (f, g)); -fun transaction f = present_transaction f (K ()); -fun transaction0 f = present_transaction (node_presentation oo f) (K ()); +fun transaction f = present_transaction f no_presentation; +fun transaction0 f = present_transaction (node_presentation oo f) no_presentation; -fun keep f = add_trans (Keep (fn _ => f)); +fun present f = add_trans (Keep (K (presentation f))); +fun keep f = add_trans (Keep (fn _ => fn st => let val () = f st in NONE end)); +fun keep' f = add_trans (Keep (fn int => fn st => let val () = f int st in NONE end)); fun keep_proof f = keep (fn st => @@ -495,15 +511,16 @@ |> Local_Theory.reset_group; in (Theory (finish lthy'), lthy') end | _ => raise UNDEF)) - (K ()); + no_presentation; fun local_theory restricted target f = local_theory' restricted target (K f); -fun present_local_theory target = present_transaction (fn _ => +fun present_local_theory target g = present_transaction (fn _ => (fn Theory gthy => let val (finish, lthy) = Target_Context.switch_named_cmd target gthy; in (Theory (finish lthy), lthy) end - | _ => raise UNDEF)); + | _ => raise UNDEF)) + (presentation g); (* proof transitions *) diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/PIDE/markup.ML Fri Nov 26 19:44:21 2021 +0100 @@ -153,8 +153,13 @@ val latex_macro0N: string val latex_macro0: string -> T val latex_macroN: string val latex_macro: string -> T val latex_environmentN: string val latex_environment: string -> T + val latex_headingN: string val latex_heading: string -> T + val latex_bodyN: string val latex_body: string -> T val latex_index_itemN: string val latex_index_item: T val latex_index_entryN: string val latex_index_entry: string -> T + val latex_delimN: string val latex_delim: string -> T + val latex_tagN: string val latex_tag: string -> T + val optional_argumentN: string val optional_argument: string -> T -> T val markdown_paragraphN: string val markdown_paragraph: T val markdown_itemN: string val markdown_item: T val markdown_bulletN: string val markdown_bullet: int -> T @@ -584,8 +589,15 @@ val (latex_macro0N, latex_macro0) = markup_string "latex_macro0" nameN; val (latex_macroN, latex_macro) = markup_string "latex_macro" nameN; val (latex_environmentN, latex_environment) = markup_string "latex_environment" nameN; +val (latex_headingN, latex_heading) = markup_string "latex_heading" kindN; +val (latex_bodyN, latex_body) = markup_string "latex_body" kindN; val (latex_index_itemN, latex_index_item) = markup_elem "latex_index_item"; val (latex_index_entryN, latex_index_entry) = markup_string "latex_index_entry" kindN; +val (latex_delimN, latex_delim) = markup_string "latex_delim" nameN; +val (latex_tagN, latex_tag) = markup_string "latex_tag" nameN; + +val optional_argumentN = "optional_argument"; +fun optional_argument arg = properties [(optional_argumentN, arg)]; (* Markdown document structure *) diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/PIDE/markup.scala Fri Nov 26 19:44:21 2021 +0100 @@ -375,9 +375,16 @@ val Latex_Macro0 = new Markup_String("latex_macro0", NAME) val Latex_Macro = new Markup_String("latex_macro", NAME) val Latex_Environment = new Markup_String("latex_environment", NAME) + val Latex_Heading = new Markup_String("latex_heading", KIND) + val Latex_Body = new Markup_String("latex_body", KIND) + val Latex_Delim = new Markup_String("latex_delim", NAME) + val Latex_Tag = new Markup_String("latex_tag", NAME) + val Latex_Index_Item = new Markup_Elem("latex_index_item") val Latex_Index_Entry = new Markup_String("latex_index_entry", KIND) + val Optional_Argument = new Properties.String("optional_argument") + /* Markdown document structure */ @@ -773,6 +780,8 @@ { def is_empty: Boolean = name.isEmpty + def position_properties: Position.T = properties.filter(Markup.position_property) + def markup(s: String): String = YXML.string_of_tree(XML.Elem(this, List(XML.Text(s)))) diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/ROOT --- a/src/Pure/ROOT Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/ROOT Fri Nov 26 19:44:21 2021 +0100 @@ -26,11 +26,16 @@ description " Miscellaneous examples and experiments for Isabelle/Pure. " + options [document_heading_prefix = ""] sessions "Pure-Examples" - theories + theories [document = false] Def Def_Examples Guess Guess_Examples - + theories + Alternative_Headings + Alternative_Headings_Examples + document_files + "root.tex" diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/System/options.scala --- a/src/Pure/System/options.scala Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/System/options.scala Fri Nov 26 19:44:21 2021 +0100 @@ -33,14 +33,21 @@ typ: Type, value: String, default_value: String, + standard_value: Option[String], description: String, section: String) { + private def print_value(x: String): String = if (typ == Options.String) quote(x) else x + private def print_standard: String = + standard_value match { + case None => "" + case Some(s) if s == default_value => " (standard)" + case Some(s) => " (standard " + print_value(s) + ")" + } private def print(default: Boolean): String = { val x = if (default) default_value else value - "option " + name + " : " + typ.print + " = " + - (if (typ == Options.String) quote(x) else x) + + "option " + name + " : " + typ.print + " = " + print_value(x) + print_standard + (if (description == "") "" else "\n -- " + quote(description)) } @@ -67,14 +74,17 @@ private val SECTION = "section" private val PUBLIC = "public" private val OPTION = "option" + private val STANDARD = "standard" private val OPTIONS = Path.explode("etc/options") private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences") val options_syntax: Outer_Syntax = - Outer_Syntax.empty + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded + + Outer_Syntax.empty + ":" + "=" + "--" + "(" + ")" + + Symbol.comment + Symbol.comment_decoded + (SECTION, Keyword.DOCUMENT_HEADING) + (PUBLIC, Keyword.BEFORE_COMMAND) + - (OPTION, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL) + + STANDARD val prefs_syntax: Outer_Syntax = Outer_Syntax.empty + "=" @@ -86,6 +96,8 @@ opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^ { case s ~ n => if (s.isDefined) "-" + n else n } | atom("option value", tok => tok.is_name || tok.is_float) + val option_standard: Parser[Option[String]] = + $$$("(") ~! $$$(STANDARD) ~ opt(option_value) ~ $$$(")") ^^ { case _ ~ _ ~ a ~ _ => a } } private object Parser extends Parser @@ -98,9 +110,10 @@ command(SECTION) ~! text ^^ { case _ ~ a => (options: Options) => options.set_section(a) } | opt($$$(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~ - $$$("=") ~ option_value ~ (comment_marker ~! text ^^ { case _ ~ x => x } | success(""))) ^^ - { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e) => - (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) } + $$$("=") ~ option_value ~ opt(option_standard) ~ + (comment_marker ~! text ^^ { case _ ~ x => x } | success(""))) ^^ + { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e ~ f) => + (options: Options) => options.declare(a.isDefined, pos, b, c, d, e, f) } } val prefs_entry: Parser[Options => Options] = @@ -302,6 +315,7 @@ name: String, typ_name: String, value: String, + standard: Option[Option[String]], description: String): Options = { options.get(name) match { @@ -319,7 +333,16 @@ error("Unknown type for option " + quote(name) + " : " + quote(typ_name) + Position.here(pos)) } - val opt = Options.Opt(public, pos, name, typ, value, value, description, section) + val standard_value = + standard match { + case None => None + case Some(_) if typ == Options.Bool => + error("Illegal standard value for option " + quote(name) + " : " + typ_name + + Position.here) + case Some(s) => Some(s.getOrElse(value)) + } + val opt = + Options.Opt(public, pos, name, typ, value, value, standard_value, description, section) (new Options(options + (name -> opt), section)).check_value(name) } } @@ -328,7 +351,7 @@ { if (options.isDefinedAt(name)) this + (name, value) else { - val opt = Options.Opt(false, Position.none, name, Options.Unknown, value, value, "", "") + val opt = Options.Opt(false, Position.none, name, Options.Unknown, value, value, None, "", "") new Options(options + (name -> opt), section) } } @@ -342,9 +365,9 @@ def + (name: String, opt_value: Option[String]): Options = { val opt = check_name(name) - opt_value match { + opt_value orElse opt.standard_value match { case Some(value) => this + (name, value) - case None if opt.typ == Options.Bool | opt.typ == Options.String => this + (name, "true") + case None if opt.typ == Options.Bool => this + (name, "true") case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print) } } diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Thy/document_build.scala Fri Nov 26 19:44:21 2021 +0100 @@ -11,31 +11,6 @@ { /* document variants */ - object Content - { - def apply(path: Path, content: Bytes): Content = new Content_Bytes(path, content) - def apply(path: Path, content: String): Content = new Content_String(path, content) - def apply(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content) - } - trait Content - { - def path: Path - def write(dir: Path): Unit - } - final class Content_Bytes private[Document_Build](val path: Path, content: Bytes) extends Content - { - def write(dir: Path): Unit = Bytes.write(dir + path, content) - } - final class Content_String private[Document_Build](val path: Path, content: String) extends Content - { - def write(dir: Path): Unit = File.write(dir + path, content) - } - final class Content_XML private[Document_Build](val path: Path, content: XML.Body) - { - def output(out: XML.Body => String): Content_String = - new Content_String(path, out(content)) - } - abstract class Document_Name { def name: String @@ -46,36 +21,17 @@ object Document_Variant { - def parse(name: String, tags: String): Document_Variant = - Document_Variant(name, Library.space_explode(',', tags)) - def parse(opt: String): Document_Variant = Library.space_explode('=', opt) match { - case List(name) => Document_Variant(name, Nil) - case List(name, tags) => parse(name, tags) + case List(name) => Document_Variant(name, Latex.Tags.empty) + case List(name, tags) => Document_Variant(name, Latex.Tags(tags)) case _ => error("Malformed document variant: " + quote(opt)) } } - sealed case class Document_Variant(name: String, tags: List[String]) extends Document_Name + sealed case class Document_Variant(name: String, tags: Latex.Tags) extends Document_Name { - def print_tags: String = tags.mkString(",") - def print: String = if (tags.isEmpty) name else name + "=" + print_tags - - def isabelletags: Content = - { - val path = Path.explode("isabelletags.sty") - val content = - Library.terminate_lines( - tags.map(tag => - tag.toList match { - case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" - case '-' :: cs => "\\isadroptag{" + cs.mkString + "}" - case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" - case cs => "\\isakeeptag{" + cs.mkString + "}" - })) - Content(path, content) - } + def print: String = if (tags.toString.isEmpty) name else name + "=" + tags.toString } sealed case class Document_Input(name: String, sources: SHA1.Digest) @@ -162,9 +118,11 @@ /* context */ + val texinputs: Path = Path.explode("~~/lib/texinputs") + val isabelle_styles: List[Path] = - List("comment.sty", "isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty"). - map(name => Path.explode("~~/lib/texinputs") + Path.basic(name)) + List("isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty"). + map(name => texinputs + Path.basic(name)) def context( session: String, @@ -174,7 +132,7 @@ { val info = deps.sessions_structure(session) val base = deps(session) - val hierarchy = deps.sessions_structure.hierarchy(session) + val hierarchy = deps.sessions_structure.build_hierarchy(session) new Context(info, base, hierarchy, db_context, progress) } @@ -218,31 +176,31 @@ def session_theories: List[Document.Node.Name] = base.session_theories def document_theories: List[Document.Node.Name] = session_theories ::: base.document_theories - lazy val document_latex: List[Content_XML] = + lazy val document_latex: List[File.Content_XML] = for (name <- document_theories) yield { val path = Path.basic(tex_name(name)) val content = YXML.parse_body(get_export(name.theory, Export.DOCUMENT_LATEX).text) - Content(path, content) + File.Content(path, content) } - lazy val session_graph: Content = + lazy val session_graph: File.Content = { val path = Presentation.session_graph_path val content = graphview.Graph_File.make_pdf(options, base.session_graph_display) - Content(path, content) + File.Content(path, content) } - lazy val session_tex: Content = + lazy val session_tex: File.Content = { val path = Path.basic("session.tex") val content = Library.terminate_lines( base.session_theories.map(name => "\\input{" + tex_name(name) + "}")) - Content(path, content) + File.Content(path, content) } - lazy val isabelle_logo: Option[Content] = + lazy val isabelle_logo: Option[File.Content] = { document_logo.map(logo_name => Isabelle_System.with_tmp_file("logo", ext = "pdf")(tmp_path => @@ -250,7 +208,7 @@ Logo.create_logo(logo_name, output_file = tmp_path, quiet = true) val path = Path.basic("isabelle_logo.pdf") val content = Bytes.read(tmp_path) - Content(path, content) + File.Content(path, content) })) } @@ -265,7 +223,12 @@ /* actual sources: with SHA1 digest */ isabelle_styles.foreach(Isabelle_System.copy_file(_, doc_dir)) - doc.isabelletags.write(doc_dir) + + val comment_latex = options.bool("document_comment_latex") + if (!comment_latex) { + Isabelle_System.copy_file(texinputs + Path.basic("comment.sty"), doc_dir) + } + doc.tags.sty(comment_latex).write(doc_dir) for ((base_dir, src) <- info.document_files) { Isabelle_System.copy_file_base(info.dir + base_dir, src, doc_dir) @@ -360,7 +323,7 @@ abstract class Bash_Engine(name: String) extends Engine(name) { def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory = - context.prepare_directory(dir, doc, new Latex.Output) + context.prepare_directory(dir, doc, new Latex.Output(context.options)) def use_pdflatex: Boolean = false def latex_script(context: Context, directory: Directory): String = diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Thy/document_output.ML --- a/src/Pure/Thy/document_output.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Thy/document_output.ML Fri Nov 26 19:44:21 2021 +0100 @@ -8,6 +8,8 @@ sig val document_reports: Input.source -> Position.report list val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text + val document_output: {markdown: bool, markup: Latex.text -> Latex.text} -> + (xstring * Position.T) option * Input.source -> Toplevel.transition -> Toplevel.transition val check_comments: Proof.context -> Symbol_Pos.T list -> unit val output_token: Proof.context -> Token.T -> Latex.text val output_source: Proof.context -> string -> Latex.text @@ -111,6 +113,22 @@ in output_antiquotes ants end end; +fun document_output {markdown, markup} (loc, txt) = + let + fun output st = + let + val ctxt = Toplevel.presentation_context st; + val _ = Context_Position.reports ctxt (document_reports txt); + in txt |> output_document ctxt {markdown = markdown} |> markup end; + in + Toplevel.present (fn st => + (case loc of + NONE => output st + | SOME (_, pos) => + error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o + Toplevel.present_local_theory loc output + end; + (* output tokens with formal comments *) @@ -184,9 +202,7 @@ datatype token = Ignore | Token of Token.T - | Heading of string * Input.source - | Body of string * Input.source - | Raw of Input.source; + | Output of Latex.text; fun token_with pred (Token tok) = pred tok | token_with _ _ = false; @@ -200,13 +216,7 @@ (case tok of Ignore => [] | Token tok => output_token ctxt tok - | Heading (cmd, source) => - XML.enclose ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n" - (output_document ctxt {markdown = false} source) - | Body (cmd, source) => - Latex.environment_text ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source) - | Raw source => - Latex.string "%\n" @ output_document ctxt {markdown = true} source @ Latex.string "\n"); + | Output output => output); (* command spans *) @@ -242,10 +252,15 @@ if x = y then I else (case which (x, y) of NONE => I | SOME txt => fold cons (Latex.string (f txt))); -val begin_tag = edge #2 Latex.begin_tag; -val end_tag = edge #1 Latex.end_tag; -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; +val markup_tag = YXML.output_markup o Markup.latex_tag; +val markup_delim = YXML.output_markup o Markup.latex_delim; +val bg_delim = #1 o markup_delim; +val en_delim = #2 o markup_delim; + +val begin_tag = edge #2 (#1 o markup_tag); +val end_tag = edge #1 (#2 o markup_tag); +fun open_delim delim e = edge #2 bg_delim e #> delim #> edge #2 en_delim e; +fun close_delim delim e = edge #1 bg_delim e #> delim #> edge #1 en_delim e; fun document_tag cmd_pos state state' tagging_stack = let @@ -343,11 +358,39 @@ (* present_thy *) +type segment = + {span: Command_Span.span, command: Toplevel.transition, + prev_state: Toplevel.state, state: Toplevel.state}; + local val markup_true = "\\isamarkuptrue%\n"; val markup_false = "\\isamarkupfalse%\n"; +fun command_output output tok = + if Token.is_command tok then SOME (Token.put_output output tok) else NONE; + +fun segment_content (segment: segment) = + let val toks = Command_Span.content (#span segment) in + (case Toplevel.output_of (#state segment) of + NONE => toks + | SOME output => map_filter (command_output output) toks) + end; + +fun output_command keywords = Scan.some (fn tok => + if Token.is_command tok then + let + val name = Token.content_of tok; + val is_document = Keyword.is_document keywords name; + val is_document_raw = Keyword.is_document_raw keywords name; + val flag = if is_document andalso not is_document_raw then markup_true else ""; + in + if is_document andalso is_some (Token.get_output tok) + then SOME ((name, Token.pos_of tok), the (Token.get_output tok), flag) + else NONE + end + else NONE); + val opt_newline = Scan.option (Scan.one Token.is_newline); val ignore = @@ -357,17 +400,8 @@ (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline) >> pair (d - 1)); -val locale = - Scan.option ((Parse.$$$ "(" -- Document_Source.improper -- Parse.$$$ "in") |-- - Parse.!!! - (Document_Source.improper |-- Parse.name --| (Document_Source.improper -- Parse.$$$ ")"))); - in -type segment = - {span: Command_Span.span, command: Toplevel.transition, - prev_state: Toplevel.state, state: Toplevel.state}; - fun present_thy options thy (segments: segment list) = let val keywords = Thy_Header.get_keywords thy; @@ -376,18 +410,11 @@ (* tokens *) val ignored = Scan.state --| ignore - >> (fn d => (NONE, (Ignore, ("", d)))); + >> (fn d => [(NONE, (Ignore, ("", d)))]); - fun markup pred mk flag = Scan.peek (fn d => - Document_Source.improper |-- - Parse.position (Scan.one (fn tok => - Token.is_command tok andalso pred keywords (Token.content_of tok))) -- - (Document_Source.annotation |-- - Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |-- - Parse.document_source --| Document_Source.improper_end)) - >> (fn ((tok, pos'), source) => - let val name = Token.content_of tok - in (SOME (name, pos'), (mk (name, source), (flag, d))) end)); + val output = Scan.peek (fn d => + Document_Source.improper |-- output_command keywords --| Document_Source.improper_end + >> (fn (kind, body, flag) => [(SOME kind, (Output body, (flag, d)))])); val command = Scan.peek (fn d => Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] -- @@ -398,18 +425,12 @@ (Token cmd, (markup_false, d)))])); val cmt = Scan.peek (fn d => - Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Token tok, ("", d))))); + Scan.one Document_Source.is_black_comment >> (fn tok => [(NONE, (Token tok, ("", d)))])); val other = Scan.peek (fn d => - Parse.not_eof >> (fn tok => (NONE, (Token tok, ("", d))))); + Parse.not_eof >> (fn tok => [(NONE, (Token tok, ("", d)))])); - val tokens = - (ignored || - markup Keyword.is_document_heading Heading markup_true || - markup Keyword.is_document_body Body markup_true || - markup Keyword.is_document_raw (Raw o #2) "") >> single || - command || - (cmt || other) >> single; + val tokens = ignored || output || command || cmt || other; (* spans *) @@ -436,7 +457,7 @@ make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4)))); val spans = segments - |> maps (Command_Span.content o #span) + |> maps segment_content |> drop_suffix Token.is_space |> Source.of_list |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat)) diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Thy/export_theory.scala Fri Nov 26 19:44:21 2021 +0100 @@ -94,15 +94,6 @@ locale_dependencies.iterator.map(_.no_content) ++ (for { (_, xs) <- others; x <- xs.iterator } yield x.no_content) - lazy val entity_by_range: Map[Symbol.Range, List[Entity[No_Content]]] = - entity_iterator.toList.groupBy(_.range) - - lazy val entity_by_kind_name: Map[(String, String), Entity[No_Content]] = - entity_iterator.map(entity => ((entity.kind, entity.name), entity)).toMap - - lazy val entity_kinds: Set[String] = - entity_iterator.map(_.kind).toSet - def cache(cache: Term.Cache): Theory = Theory(cache.string(name), parents.map(cache.string), diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Thy/latex.ML Fri Nov 26 19:44:21 2021 +0100 @@ -22,10 +22,6 @@ val output_syms: string -> string val symbols: Symbol_Pos.T list -> text val symbols_output: Symbol_Pos.T list -> text - val begin_delim: string -> string - val end_delim: string -> string - val begin_tag: string -> string - val end_tag: string -> string val environment_text: string -> text -> text val isabelle_body: string -> text -> text val theory_entry: string -> string @@ -196,14 +192,6 @@ text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms)); -(* tags *) - -val begin_delim = enclose_name "%\n\\isadelim" "\n"; -val end_delim = enclose_name "%\n\\endisadelim" "\n"; -val begin_tag = enclose_name "%\n\\isatag" "\n"; -fun end_tag tg = enclose_name "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg; - - (* theory presentation *) fun environment_text name = diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Thy/latex.scala --- a/src/Pure/Thy/latex.scala Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Thy/latex.scala Fri Nov 26 19:44:21 2021 +0100 @@ -11,11 +11,42 @@ import scala.annotation.tailrec import scala.collection.mutable +import scala.collection.immutable.TreeMap import scala.util.matching.Regex object Latex { + /* output name for LaTeX macros */ + + private val output_name_map: Map[Char, String] = + Map('_' -> "UNDERSCORE", + '\'' -> "PRIME", + '0' -> "ZERO", + '1' -> "ONE", + '2' -> "TWO", + '3' -> "THREE", + '4' -> "FOUR", + '5' -> "FIVE", + '6' -> "SIX", + '7' -> "SEVEN", + '8' -> "EIGHT", + '9' -> "NINE") + + def output_name(name: String): String = + if (name.exists(output_name_map.keySet)) { + val res = new StringBuilder + for (c <- name) { + output_name_map.get(c) match { + case None => res += c + case Some(s) => res ++= s + } + } + res.toString + } + else name + + /* index entries */ def index_escape(str: String): String = @@ -63,6 +94,67 @@ } + /* tags */ + + object Tags + { + object Op extends Enumeration + { + val fold, drop, keep = Value + } + + val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant" + + private def explode(spec: String): List[String] = + Library.space_explode(',', spec) + + def apply(spec: String): Tags = + new Tags(spec, + (explode(standard) ::: explode(spec)).foldLeft(TreeMap.empty[String, Op.Value]) { + case (m, tag) => + tag.toList match { + case '/' :: cs => m + (cs.mkString -> Op.fold) + case '-' :: cs => m + (cs.mkString -> Op.drop) + case '+' :: cs => m + (cs.mkString -> Op.keep) + case cs => m + (cs.mkString -> Op.keep) + } + }) + + val empty: Tags = apply("") + } + + class Tags private(spec: String, map: TreeMap[String, Tags.Op.Value]) + { + override def toString: String = spec + + def get(name: String): Option[Tags.Op.Value] = map.get(name) + + def sty(comment_latex: Boolean): File.Content = + { + val path = Path.explode("isabelletags.sty") + val comment = + if (comment_latex) """\usepackage{comment}""" + else """%plain TeX version of comment package -- much faster! +\let\isafmtname\fmtname\def\fmtname{plain} +\usepackage{comment} +\let\fmtname\isafmtname""" + val tags = + (for ((name, op) <- map.iterator) + yield "\\isa" + op + "tag{" + name + "}").toList + File.Content(path, comment + """ + +\newcommand{\isakeeptag}[1]% +{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}} +\newcommand{\isadroptag}[1]% +{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}} +\newcommand{\isafoldtag}[1]% +{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}} + +""" + Library.terminate_lines(tags)) + } + } + + /* output text and positions */ type Text = XML.Body @@ -73,18 +165,45 @@ if (file_pos.isEmpty) Nil else List("\\endinput\n", position(Markup.FILE, file_pos)) - class Output + class Output(options: Options) { def latex_output(latex_text: Text): String = apply(latex_text) - def latex_macro0(name: String): Text = - XML.string("\\" + name) + def latex_macro0(name: String, optional_argument: String = ""): Text = + XML.string("\\" + name + optional_argument) + + def latex_macro(name: String, body: Text, optional_argument: String = ""): Text = + XML.enclose("\\" + name + optional_argument + "{", "}", body) + + def latex_environment(name: String, body: Text, optional_argument: String = ""): Text = + XML.enclose( + "%\n\\begin{" + name + "}" + optional_argument + "%\n", + "%\n\\end{" + name + "}", body) + + def latex_heading(kind: String, body: Text, optional_argument: String = ""): Text = + XML.enclose( + "%\n\\" + options.string("document_heading_prefix") + kind + optional_argument + "{", + "%\n}\n", body) - def latex_macro(name: String, body: Text): Text = - XML.enclose("\\" + name + "{", "}", body) + def latex_body(kind: String, body: Text, optional_argument: String = ""): Text = + latex_environment("isamarkup" + kind, body, optional_argument) - def latex_environment(name: String, body: Text): Text = - XML.enclose("%\n\\begin{" + name + "}%\n", "%\n\\end{" + name + "}", body) + def latex_tag(name: String, body: Text, delim: Boolean = false): Text = + { + val s = output_name(name) + val kind = if (delim) "delim" else "tag" + val end = if (delim) "" else "{\\isafold" + s + "}%\n" + if (options.bool("document_comment_latex")) { + XML.enclose( + "%\n\\begin{isa" + kind + s + "}\n", + "%\n\\end{isa" + kind + s + "}\n" + end, body) + } + else { + XML.enclose( + "%\n\\isa" + kind + s + "\n", + "%\n\\endisa" + kind + s + "\n" + end, body) + } + } def index_item(item: Index_Item.Value): String = { @@ -103,38 +222,50 @@ /* standard output of text with per-line positions */ + def unknown_elem(elem: XML.Elem, pos: Position.T): XML.Body = + error("Unknown latex markup element " + quote(elem.name) + Position.here(pos) + + ":\n" + XML.string_of_tree(elem)) + def apply(latex_text: Text, file_pos: String = ""): String = { var line = 1 val result = new mutable.ListBuffer[String] val positions = new mutable.ListBuffer[String] ++= init_position(file_pos) - def traverse(body: XML.Body): Unit = + val file_position = if (file_pos.isEmpty) Position.none else Position.File(file_pos) + + def traverse(xml: XML.Body): Unit = { - body.foreach { + xml.foreach { case XML.Text(s) => line += s.count(_ == '\n') result += s - case XML.Elem(Markup.Document_Latex(props), body) => - for { l <- Position.Line.unapply(props) if positions.nonEmpty } { - val s = position(Value.Int(line), Value.Int(l)) - if (positions.last != s) positions += s + case elem @ XML.Elem(markup, body) => + val a = Markup.Optional_Argument.get(markup.properties) + traverse { + markup match { + case Markup.Document_Latex(props) => + for (l <- Position.Line.unapply(props) if positions.nonEmpty) { + val s = position(Value.Int(line), Value.Int(l)) + if (positions.last != s) positions += s + } + body + case Markup.Latex_Output(_) => XML.string(latex_output(body)) + case Markup.Latex_Macro0(name) if body.isEmpty => latex_macro0(name, a) + case Markup.Latex_Macro(name) => latex_macro(name, body, a) + case Markup.Latex_Environment(name) => latex_environment(name, body, a) + case Markup.Latex_Heading(kind) => latex_heading(kind, body, a) + case Markup.Latex_Body(kind) => latex_body(kind, body, a) + case Markup.Latex_Delim(name) => latex_tag(name, body, delim = true) + case Markup.Latex_Tag(name) => latex_tag(name, body) + case Markup.Latex_Index_Entry(_) => + elem match { + case Index_Entry(entry) => index_entry(entry) + case _ => unknown_elem(elem, file_position) + } + case _ => unknown_elem(elem, file_position) + } } - traverse(body) - case XML.Elem(Markup.Latex_Output(_), body) => - traverse(XML.string(latex_output(body))) - case XML.Elem(Markup.Latex_Macro0(name), Nil) => - traverse(latex_macro0(name)) - case XML.Elem(Markup.Latex_Macro(name), body) => - traverse(latex_macro(name, body)) - case XML.Elem(Markup.Latex_Environment(name), body) => - traverse(latex_environment(name, body)) - case Index_Entry(entry) => - traverse(index_entry(entry)) - case t: XML.Tree => - error("Bad latex markup" + - (if (file_pos.isEmpty) "" else Position.here(Position.File(file_pos))) + ":\n" + - XML.string_of_tree(t)) } } traverse(latex_text) diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Thy/presentation.scala Fri Nov 26 19:44:21 2021 +0100 @@ -22,7 +22,7 @@ abstract class HTML_Context { - /* directory structure */ + /* directory structure and resources */ def root_dir: Path def theory_session(name: Document.Node.Name): Sessions.Info @@ -34,6 +34,11 @@ def files_path(name: Document.Node.Name, path: Path): Path = theory_path(name).dir + Path.explode("files") + path.squash.html + type Theory_Exports = Map[String, Entity_Context.Theory_Export] + def theory_exports: Theory_Exports = Map.empty + def theory_export(name: String): Entity_Context.Theory_Export = + theory_exports.getOrElse(name, Entity_Context.no_theory_export) + /* HTML content */ @@ -64,40 +69,6 @@ } - /* presentation state */ - - class State - { - /* already presented theories */ - - private val already_presented = Synchronized(Set.empty[String]) - - def register_presented(nodes: List[Document.Node.Name]): List[Document.Node.Name] = - already_presented.change_result(presented => - (nodes.filterNot(name => presented.contains(name.theory)), - presented ++ nodes.iterator.map(_.theory))) - - - /* cached theory exports */ - - val cache: Term.Cache = Term.Cache.make() - - private val theory_cache = Synchronized(Map.empty[String, Export_Theory.Theory]) - def cache_theory(thy_name: String, make_thy: => Export_Theory.Theory): Export_Theory.Theory = - { - theory_cache.change_result(thys => - { - thys.get(thy_name) match { - case Some(thy) => (thy, thys) - case None => - val thy = make_thy - (thy, thys + (thy_name -> thy)) - } - }) - } - } - - /* presentation elements */ sealed case class Elements( @@ -124,6 +95,13 @@ object Entity_Context { + sealed case class Theory_Export( + entity_by_range: Map[Symbol.Range, List[Export_Theory.Entity[Export_Theory.No_Content]]], + entity_by_kind_name: Map[(String, String), Export_Theory.Entity[Export_Theory.No_Content]], + others: List[String]) + + val no_theory_export: Theory_Export = Theory_Export(Map.empty, Map.empty, Nil) + object Theory_Ref { def unapply(props: Properties.T): Option[Document.Node.Name] = @@ -152,7 +130,7 @@ session: String, deps: Sessions.Deps, node: Document.Node.Name, - theory_exports: Map[String, Export_Theory.Theory]): Entity_Context = + html_context: HTML_Context): Entity_Context = new Entity_Context { private val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty @@ -163,7 +141,8 @@ case _ => Some { val entities = - theory_exports.get(node.theory).flatMap(_.entity_by_range.get(range)) + html_context.theory_exports.get(node.theory) + .flatMap(_.entity_by_range.get(range)) .getOrElse(Nil) val body1 = if (seen_ranges.contains(range)) { @@ -193,7 +172,7 @@ private def logical_ref(thy_name: String, kind: String, name: String): Option[String] = for { - thy <- theory_exports.get(thy_name) + thy <- html_context.theory_exports.get(thy_name) entity <- thy.entity_by_kind_name.get((kind, name)) } yield entity.kname @@ -203,7 +182,7 @@ case Theory_Ref(node_name) => node_relative(deps, session, node_name).map(html_dir => HTML.link(html_dir + html_name(node_name), body)) - case Entity_Ref(file_path, def_theory, kind, name) => + case Entity_Ref(file_path, def_theory, kind, name) if file_path.get_ext == "thy" => for { thy_name <- def_theory orElse (if (File.eq(node.path, file_path)) Some(node.theory) else None) @@ -497,6 +476,40 @@ else None } + def read_exports( + sessions: List[String], + deps: Sessions.Deps, + db_context: Sessions.Database_Context): Map[String, Entity_Context.Theory_Export] = + { + type Batch = (String, List[String]) + val batches = + sessions.foldLeft((Set.empty[String], List.empty[Batch]))( + { case ((seen, batches), session) => + val thys = deps(session).loaded_theories.keys.filterNot(seen) + (seen ++ thys, (session, thys) :: batches) + })._2 + Par_List.map[Batch, List[(String, Entity_Context.Theory_Export)]]( + { case (session, thys) => + for (thy_name <- thys) yield { + val theory = + if (thy_name == Thy_Header.PURE) Export_Theory.no_theory + else { + val provider = Export.Provider.database_context(db_context, List(session), thy_name) + if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) { + Export_Theory.read_theory(provider, session, thy_name, cache = db_context.cache) + } + else Export_Theory.no_theory + } + val entity_by_range = + theory.entity_iterator.toList.groupBy(_.range) + val entity_by_kind_name = + theory.entity_iterator.map(entity => ((entity.kind, entity.name), entity)).toMap + val others = theory.others.keySet.toList + thy_name -> Entity_Context.Theory_Export(entity_by_range, entity_by_kind_name, others) + } + }, batches).flatten.toMap + } + def session_html( session: String, deps: Sessions.Deps, @@ -504,14 +517,13 @@ progress: Progress = new Progress, verbose: Boolean = false, html_context: HTML_Context, - state: State, session_elements: Elements): Unit = { val info = deps.sessions_structure(session) val options = info.options val base = deps(session) - val hierarchy = deps.sessions_structure.hierarchy(session) + val hierarchy = deps.sessions_structure.build_hierarchy(session) val hierarchy_theories = hierarchy.reverse.flatMap(a => deps(a).used_theories.map(_._1)) val session_dir = Isabelle_System.make_directory(html_context.session_dir(info)) @@ -551,27 +563,8 @@ map(link => HTML.text("View ") ::: List(link))).flatten } - val theory_exports: Map[String, Export_Theory.Theory] = - (for (node <- hierarchy_theories.iterator) yield { - val thy_name = node.theory - val theory = - if (thy_name == Thy_Header.PURE) Export_Theory.no_theory - else { - state.cache_theory(thy_name, - { - val provider = Export.Provider.database_context(db_context, hierarchy, thy_name) - if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) { - Export_Theory.read_theory( - provider, session, thy_name, cache = state.cache) - } - else Export_Theory.no_theory - }) - } - thy_name -> theory - }).toMap - def entity_context(name: Document.Node.Name): Entity_Context = - Entity_Context.make(session, deps, name, theory_exports) + Entity_Context.make(session, deps, name, html_context) sealed case class Seen_File( @@ -598,7 +591,8 @@ val thy_elements = session_elements.copy(entity = - theory_exports(name.theory).others.keySet.foldLeft(session_elements.entity)(_ + _)) + html_context.theory_export(name.theory).others + .foldLeft(session_elements.entity)(_ + _)) val files_html = for { @@ -610,7 +604,7 @@ if (verbose) progress.echo("Presenting file " + src_path) (src_path, html_context.source( - make_html(entity_context(name), thy_elements, xml))) + make_html(Entity_Context.empty, thy_elements, xml))) } val thy_html = @@ -655,7 +649,7 @@ }) } - val theories = state.register_presented(hierarchy_theories).flatMap(present_theory) + val theories = base.session_theories.flatMap(present_theory) val title = "Session " + session HTML.write_document(session_dir, "index.html", diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Thy/sessions.scala Fri Nov 26 19:44:21 2021 +0100 @@ -267,9 +267,9 @@ info.document_theories.flatMap( { case (thy, pos) => - val parent_sessions = + val build_hierarchy = if (sessions_structure.build_graph.defined(session_name)) { - sessions_structure.build_requirements(List(session_name)) + sessions_structure.build_hierarchy(session_name) } else Nil @@ -283,7 +283,7 @@ if (session_theories.contains(name)) { err("Redundant document theory from this session:") } - else if (parent_sessions.contains(qualifier)) None + else if (build_hierarchy.contains(qualifier)) None else if (dependencies.theories.contains(name)) None else err("Document theory from other session not imported properly:") } @@ -781,8 +781,7 @@ else { (for { (name, (info, _)) <- graph.iterator - if info.dir_selected || select_session(name) || - graph.get_node(name).groups.exists(select_group) + if info.dir_selected || select_session(name) || info.groups.exists(select_group) } yield name).toList } @@ -837,17 +836,17 @@ deps } - def hierarchy(session: String): List[String] = build_graph.all_preds(List(session)) - def build_selection(sel: Selection): List[String] = selected(build_graph, sel) def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss) def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss) def build_topological_order: List[String] = build_graph.topological_order + def build_hierarchy(session: String): List[String] = build_graph.all_preds(List(session)) def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel) def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss) def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss) def imports_topological_order: List[String] = imports_graph.topological_order + def imports_hierarchy(session: String): List[String] = imports_graph.all_preds(List(session)) def bibtex_entries: List[(String, List[String])] = build_topological_order.flatMap(name => diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Tools/build.ML Fri Nov 26 19:44:21 2021 +0100 @@ -60,7 +60,7 @@ else (Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ " (undefined " ^ commas conds ^ ")\n"); []) - in apply_hooks qualifier loaded_theories end; + in loaded_theories end; (* build session *) @@ -81,11 +81,16 @@ fun build () = let - val res1 = + val res = theories |> - (List.app (build_theories session_name) + (map (build_theories session_name) |> session_timing |> Exn.capture); + val res1 = + (case res of + Exn.Res loaded_theories => + Exn.capture (apply_hooks session_name) (flat loaded_theories) + | Exn.Exn exn => Exn.Exn exn); val res2 = Exn.capture Session.finish (); val _ = Resources.finish_session_base (); diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Tools/build.scala Fri Nov 26 19:44:21 2021 +0100 @@ -191,7 +191,6 @@ options + "completion_limit=0" + "editor_tracing_messages=0" + - "kodkod_scala=false" + ("pide_reports=" + options.bool("build_pide_reports")) val store = Sessions.store(build_options) @@ -205,6 +204,7 @@ Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos) val full_sessions_selection = full_sessions.imports_selection(selection) + val full_sessions_selected = full_sessions_selection.toSet def sources_stamp(deps: Sessions.Deps, session_name: String): String = { @@ -242,15 +242,11 @@ } val presentation_sessions = - { - val sessions = deps.sessions_structure - val selected = full_sessions_selection.toSet (for { - session_name <- sessions.imports_topological_order.iterator - info <- sessions.get(session_name) - if selected(session_name) && presentation.enabled(info) } + session_name <- deps.sessions_structure.build_topological_order.iterator + info <- deps.sessions_structure.get(session_name) + if full_sessions_selected(session_name) && presentation.enabled(info) } yield info).toList - } /* check unknown files */ @@ -308,7 +304,7 @@ val log = build_options.string("system_log") match { case "" => No_Logger - case "true" => Logger.make(progress) + case "-" => Logger.make(progress) case log_file => Logger.make(Some(Path.explode(log_file))) } @@ -509,10 +505,13 @@ Presentation.update_chapter(presentation_dir, chapter, entries) } - val state = new Presentation.State { override val cache: Term.Cache = store.cache } + using(store.open_database_context())(db_context => + { + val exports = + Presentation.read_exports(presentation_sessions.map(_.name), deps, db_context) - using(store.open_database_context())(db_context => - for (session <- presentation_sessions.map(_.name)) { + Par_List.map((session: String) => + { progress.expose_interrupt() progress.echo("Presenting " + session + " ...") @@ -521,12 +520,14 @@ override def root_dir: Path = presentation_dir override def theory_session(name: Document.Node.Name): Sessions.Info = deps.sessions_structure(deps(session).theory_qualifier(name)) + override def theory_exports: Theory_Exports = exports } Presentation.session_html( session, deps, db_context, progress = progress, - verbose = verbose, html_context = html_context, state = state, + verbose = verbose, html_context = html_context, Presentation.elements1) - }) + }, presentation_sessions.map(_.name)) + }) } } diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/Tools/scala_project.scala --- a/src/Pure/Tools/scala_project.scala Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/Tools/scala_project.scala Fri Nov 26 19:44:21 2021 +0100 @@ -143,7 +143,7 @@ def package_name(source_file: Path): Option[String] = { - val lines = split_lines(File.read(source_file)) + val lines = Library.trim_split_lines(File.read(source_file)) val Package = """\s*\bpackage\b\s*(?:object\b\s*)?((?:\w|\.)+)\b.*""".r lines.collectFirst({ case Package(name) => name }) } diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/ex/Alternative_Headings.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ex/Alternative_Headings.thy Fri Nov 26 19:44:21 2021 +0100 @@ -0,0 +1,34 @@ +(* Title: Pure/ex/Alternative_Headings.thy + Author: Makarius +*) + +chapter \Alternative document headings\ + +theory Alternative_Headings + imports Pure + keywords + "chapter*" "section*" "subsection*" "subsubsection*" :: document_heading +begin + +ML \ +local + +fun alternative_heading name body = + [XML.Elem (Markup.latex_heading (unsuffix "*" name) |> Markup.optional_argument "*", body)]; + +fun document_heading (name, pos) = + Outer_Syntax.command (name, pos) (name ^ " heading") + (Parse.opt_target -- Parse.document_source --| Scan.option (Parse.$$$ ";") >> + Document_Output.document_output + {markdown = false, markup = alternative_heading name}); + +val _ = + List.app document_heading + [\<^command_keyword>\chapter*\, + \<^command_keyword>\section*\, + \<^command_keyword>\subsection*\, + \<^command_keyword>\subsubsection*\]; + +in end\ + +end diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/ex/Alternative_Headings_Examples.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ex/Alternative_Headings_Examples.thy Fri Nov 26 19:44:21 2021 +0100 @@ -0,0 +1,23 @@ +(* Title: Pure/ex/Alternative_Headings_Examples.thy + Author: Makarius +*) + +chapter \Some examples of alternative document headings\ + +theory Alternative_Headings_Examples + imports Alternative_Headings +begin + +section \Regular section\ + +subsection \Regular subsection\ + +subsubsection \Regular subsubsection\ + +subsubsection* \Alternative subsubsection\ + +subsection* \Alternative subsection\ + +section* \Alternative section\ + +end diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/ex/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ex/document/root.tex Fri Nov 26 19:44:21 2021 +0100 @@ -0,0 +1,20 @@ +\documentclass[10pt,a4paper]{report} +\usepackage[T1]{fontenc} +\usepackage{ifthen,proof,amssymb,isabelle,isabellesym} + +\isabellestyle{sltt} +\usepackage{pdfsetup}\urlstyle{rm} + + +\hyphenation{Isabelle} + +\begin{document} + +\title{Miscellaneous examples and experiments for Isabelle/Pure} +\maketitle + +\parindent 0pt \parskip 0.5ex + +\input{session} + +\end{document} diff -r ba59c691b3ee -r 5280c02f29dc src/Pure/pure_syn.ML --- a/src/Pure/pure_syn.ML Thu Nov 25 14:02:51 2021 +0100 +++ b/src/Pure/pure_syn.ML Fri Nov 26 19:44:21 2021 +0100 @@ -7,66 +7,43 @@ signature PURE_SYN = sig - val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source -> - Toplevel.transition -> Toplevel.transition val bootstrap_thy: theory end; structure Pure_Syn: PURE_SYN = struct -val semi = Scan.option (Parse.$$$ ";"); - -fun output_document state markdown txt = - let - val ctxt = Toplevel.presentation_context state; - val _ = Context_Position.reports ctxt (Document_Output.document_reports txt); - in Document_Output.output_document ctxt markdown txt end; +fun document_heading (name, pos) = + Outer_Syntax.command (name, pos) (name ^ " heading") + (Parse.opt_target -- Parse.document_source --| Scan.option (Parse.$$$ ";") >> + Document_Output.document_output + {markdown = false, markup = fn body => [XML.Elem (Markup.latex_heading name, body)]}); -fun document_command markdown (loc, txt) = - Toplevel.keep (fn state => - (case loc of - NONE => ignore (output_document state markdown txt) - | SOME (_, pos) => - error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o - Toplevel.present_local_theory loc (fn state => - ignore (output_document state markdown txt)); - -val _ = - Outer_Syntax.command ("chapter", \<^here>) "chapter heading" - (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); +fun document_body ((name, pos), description) = + Outer_Syntax.command (name, pos) description + (Parse.opt_target -- Parse.document_source >> + Document_Output.document_output + {markdown = true, markup = fn body => [XML.Elem (Markup.latex_body name, body)]}); val _ = - Outer_Syntax.command ("section", \<^here>) "section heading" - (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); - -val _ = - Outer_Syntax.command ("subsection", \<^here>) "subsection heading" - (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); - -val _ = - Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading" - (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); + List.app document_heading + [("chapter", \<^here>), + ("section", \<^here>), + ("subsection", \<^here>), + ("subsubsection", \<^here>), + ("paragraph", \<^here>), + ("subparagraph", \<^here>)]; val _ = - Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading" - (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); - -val _ = - Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading" - (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false}); - -val _ = - Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)" - (Parse.opt_target -- Parse.document_source >> document_command {markdown = true}); - -val _ = - Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)" - (Parse.opt_target -- Parse.document_source >> document_command {markdown = true}); + List.app document_body + [(("text", \<^here>), "formal comment (primary style)"), + (("txt", \<^here>), "formal comment (secondary style)")]; val _ = Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)" - (Parse.opt_target -- Parse.document_source >> document_command {markdown = true}); + (Parse.opt_target -- Parse.document_source >> + Document_Output.document_output + {markdown = true, markup = Latex.enclose_text "%\n" "\n"}); val _ = Outer_Syntax.command ("theory", \<^here>) "begin theory"