--- 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
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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}}{}
--- 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>\<open>Output.system_message\<close> in
- Isabelle/ML; the value ``\<^verbatim>\<open>true\<close>'' refers to console progress of the build
- job.
+ Isabelle/ML; the standard value ``\<^verbatim>\<open>-\<close>'' refers to console progress of the
+ build job.
\<^item> @{system_option_def "system_heaps"} determines the directories for
session heap images: \<^path>\<open>$ISABELLE_HEAPS\<close> is the user directory and
--- 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>\<open>'a::len word\<close>
--- 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 \<open>() |> getenv "KODKODI" <> "" ? Nitpick_Tests.run_all_tests\<close>
+ML \<open>if getenv "KODKODI" = "" then () else Nitpick_Tests.run_all_tests \<^context>\<close>
end
--- 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"
--- 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>\<open>kodkod_max_threads\<close>
else max_threads0
- val external_process =
- not (Options.default_bool \<^system_option>\<open>kodkod_scala\<close>) 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>\<open>kodkod_scala\<close>, \<^here>)
+
end;
--- 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;
--- 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
--- 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
--- 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>\<open>smt_monomorph_instances\<close> (K 500)
val explicit_application = Attrib.setup_config_int \<^binding>\<open>smt_explicit_application\<close> (K 1)
val higher_order = Attrib.setup_config_bool \<^binding>\<open>smt_higher_order\<close> (K false)
+val native_bv = Attrib.setup_config_bool \<^binding>\<open>native_bv\<close> (K true)
val nat_as_int = Attrib.setup_config_bool \<^binding>\<open>smt_nat_as_int\<close> (K false)
val infer_triggers = Attrib.setup_config_bool \<^binding>\<open>smt_infer_triggers\<close> (K false)
val debug_files = Attrib.setup_config_string \<^binding>\<open>smt_debug_files\<close> (K "")
--- 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>\<open>real\<close>))) ts
then SOME "AUFLIRA"
else NONE
--- 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
--- 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 = {
--- 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
--- 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 *)
--- 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 {
--- 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)}
--- 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
--- 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 \<open>Some examples with text cartouches\<close>
theory Cartouche_Examples
-imports Main
-keywords
- "cartouche" :: diag and
- "text_cartouche" :: thy_decl
+ imports Main
+ keywords "cartouche" :: diag
begin
subsection \<open>Regular outer syntax\<close>
@@ -135,14 +133,7 @@
subsubsection \<open>Uniform nesting of sub-languages: document source, ML, term, string literals\<close>
-ML \<open>
- Outer_Syntax.command
- \<^command_keyword>\<open>text_cartouche\<close> ""
- (Parse.opt_target -- Parse.input Parse.cartouche
- >> Pure_Syn.document_command {markdown = true})
-\<close>
-
-text_cartouche
+text
\<open>
\<^ML>\<open>
(
--- 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 =>
--- 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
--- 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 */
--- 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))
+ }
}
--- 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 *)
--- 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 *)
--- 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 *)
--- 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))))
--- 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"
--- 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)
}
}
--- 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 =
--- 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))
--- 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),
--- 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 =
--- 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)
--- 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",
--- 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 =>
--- 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 ();
--- 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))
+ })
}
}
--- 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 })
}
--- /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 \<open>Alternative document headings\<close>
+
+theory Alternative_Headings
+ imports Pure
+ keywords
+ "chapter*" "section*" "subsection*" "subsubsection*" :: document_heading
+begin
+
+ML \<open>
+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>\<open>chapter*\<close>,
+ \<^command_keyword>\<open>section*\<close>,
+ \<^command_keyword>\<open>subsection*\<close>,
+ \<^command_keyword>\<open>subsubsection*\<close>];
+
+in end\<close>
+
+end
--- /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 \<open>Some examples of alternative document headings\<close>
+
+theory Alternative_Headings_Examples
+ imports Alternative_Headings
+begin
+
+section \<open>Regular section\<close>
+
+subsection \<open>Regular subsection\<close>
+
+subsubsection \<open>Regular subsubsection\<close>
+
+subsubsection* \<open>Alternative subsubsection\<close>
+
+subsection* \<open>Alternative subsection\<close>
+
+section* \<open>Alternative section\<close>
+
+end
--- /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}
--- 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"