add document options to build_sync, since Sessions.Info is read from export database for document generation (amending 6e5397fcc41b);
authorFabian Huch <huch@in.tum.de>
Wed, 12 Feb 2025 18:22:55 +0100
changeset 82138 b840b9f5d687
parent 82137 7281e57085ab
child 82159 f3a5a7c64412
add document options to build_sync, since Sessions.Info is read from export database for document generation (amending 6e5397fcc41b);
etc/options
--- a/etc/options	Wed Feb 12 16:27:24 2025 +0000
+++ b/etc/options	Wed Feb 12 18:22:55 2025 +0100
@@ -5,27 +5,27 @@
 option browser_info : bool = false for build
   -- "generate theory browser information"
 
-option document : string = "" (standard "true") for build
+option document : string = "" (standard "true") for build build_sync
   -- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")"
-option document_output : string = "" (standard "output") for build
+option document_output : string = "" (standard "output") for build build_sync
   -- "document output directory"
-option document_echo : bool = false for build
+option document_echo : bool = false for build build_sync
   -- "inform about document file names during session presentation"
-option document_variants : string = "document" for build document
+option document_variants : string = "document" for build document build_sync
   -- "alternative document variants (separated by colons)"
-option document_tags : string = "" for document
+option document_tags : string = "" for document build_sync
   -- "default command tags (separated by commas)"
-option document_bibliography : bool = false for document
+option document_bibliography : bool = false for document build_sync
   -- "explicitly enable use of bibtex (default: according to presence of root.bib)"
-option document_build : string = "lualatex" (standard "build") for document
+option document_build : string = "lualatex" (standard "build") for document build_sync
   -- "document build engine (e.g. build, lualatex, pdflatex)"
-option document_logo : string = "" (standard "_") for document
+option document_logo : string = "" (standard "_") for document build_sync
   -- "generate named instance of Isabelle logo (underscore means unnamed variant)"
-option document_heading_prefix : string = "isamarkup" (standard) for document
+option document_heading_prefix : string = "isamarkup" (standard) for document build_sync
   -- "prefix for LaTeX macros generated from 'chapter', 'section' etc."
-option document_comment_latex : bool = false for document
+option document_comment_latex : bool = false for document build_sync
   -- "use regular LaTeX version of comment.sty, instead of historic plain TeX version"
-option document_cite_commands : string = "cite,nocite,citet,citep" for document
+option document_cite_commands : string = "cite,nocite,citet,citep" for document build_sync
   -- "antiquotation commands to determine the structure of bibliography"
 
 option thy_output_display : bool = false for content