# HG changeset patch # User wenzelm # Date 1397213002 -7200 # Node ID 34023a586608dc7fcf21a927cd8c5a62dc79cd37 # Parent aff193f53a64b92de5502e46a9a519f930c9f052# Parent 3ff16a7f0b2ebd1567c7ee8e78776710544485a1 merged diff -r aff193f53a64 -r 34023a586608 NEWS --- a/NEWS Wed Apr 09 14:08:25 2014 +0200 +++ b/NEWS Fri Apr 11 12:43:22 2014 +0200 @@ -658,6 +658,11 @@ *** System *** +* Session ROOT specifications support explicit 'document_files' for +robust dependencies on LaTeX sources. Only these explicitly given +files are copied to the document output directory, before document +processing is started. + * Simplified "isabelle display" tool. Settings variables DVI_VIEWER and PDF_VIEWER now refer to the actual programs, not shell command-lines. Discontinued option -c: invocation may be asynchronous diff -r aff193f53a64 -r 34023a586608 src/Doc/Classes/document/build --- a/src/Doc/Classes/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/Classes/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -6,11 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo Isar - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/Codegen/document/build --- a/src/Doc/Codegen/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/Codegen/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -6,11 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo Isar - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/Datatypes/document/build --- a/src/Doc/Datatypes/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/Datatypes/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -5,10 +5,5 @@ FORMAT="$1" VARIANT="$2" -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/Functions/document/build --- a/src/Doc/Functions/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/Functions/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -5,10 +5,5 @@ FORMAT="$1" VARIANT="$2" -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/Implementation/document/build --- a/src/Doc/Implementation/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/Implementation/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -6,13 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo Isar - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/underscore.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/Intro/document/build --- a/src/Doc/Intro/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/Intro/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -6,11 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/Isar_Ref/document/build --- a/src/Doc/Isar_Ref/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/Isar_Ref/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -6,15 +6,6 @@ VARIANT="$2" "$ISABELLE_TOOL" logo Isar - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/underscore.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - ./showsymbols "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > syms.tex - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/JEdit/document/build --- a/src/Doc/JEdit/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/JEdit/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -6,14 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo jEdit - -cp "$ISABELLE_HOME/src/Doc/Isar_Ref/document/style.sty" . -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/underscore.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/Logics/document/build --- a/src/Doc/Logics/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/Logics/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -6,11 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/Logics_ZF/document/build --- a/src/Doc/Logics_ZF/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/Logics_ZF/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -6,11 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo ZF - -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . -cp "$ISABELLE_HOME/src/Doc/Logics/document/syntax.tex" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/Main/document/build --- a/src/Doc/Main/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/Main/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -5,9 +5,6 @@ FORMAT="$1" VARIANT="$2" -"$ISABELLE_TOOL" latex -o sty -cp "$ISABELLE_HOME/src/Doc/pdfsetup.sty" . - "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/Nitpick/document/build --- a/src/Doc/Nitpick/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/Nitpick/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -6,9 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo Nitpick - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/Prog_Prove/document/build --- a/src/Doc/Prog_Prove/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/Prog_Prove/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -6,8 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo HOL - -cp "$ISABELLE_HOME/src/Doc/Prog_Prove/MyList.thy" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/ROOT --- a/src/Doc/ROOT Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/ROOT Fri Apr 11 12:43:22 2014 +0200 @@ -4,16 +4,17 @@ options [document_variants = "classes", quick_and_dirty] theories [document = false] Setup theories Classes - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../isar.sty" - "../manual.bib" - "document/build" - "document/root.tex" - "document/style.sty" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "manual.bib" + document_files + "build" + "root.tex" + "style.sty" session Codegen (doc) in "Codegen" = "HOL-Library" + options [document_variants = "codegen", print_mode = "no_brackets,iff"] @@ -26,61 +27,68 @@ Evaluation Adaptation Further - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../isar.sty" - "../manual.bib" - "document/build" - "document/root.tex" - "document/style.sty" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "manual.bib" + document_files + "build" + "root.tex" + "style.sty" session Datatypes (doc) in "Datatypes" = HOL + options [document_variants = "datatypes"] theories [document = false] Setup theories Datatypes - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../isar.sty" - "../manual.bib" - "document/build" - "document/root.tex" - "document/style.sty" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "manual.bib" + document_files + "build" + "root.tex" + "style.sty" session Functions (doc) in "Functions" = HOL + options [document_variants = "functions", skip_proofs = false, quick_and_dirty] theories Functions - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../isar.sty" - "../manual.bib" - "document/build" - "document/conclusion.tex" - "document/intro.tex" - "document/mathpartir.sty" - "document/root.tex" - "document/style.sty" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "manual.bib" + document_files + "build" + "conclusion.tex" + "intro.tex" + "mathpartir.sty" + "root.tex" + "style.sty" session Intro (doc) in "Intro" = Pure + options [document_variants = "intro"] theories - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../ttbox.sty" - "../manual.bib" - "document/build" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "ttbox.sty" + "manual.bib" + document_files + "advanced.tex" + "build" + "foundations.tex" + "getting.tex" + "root.tex" session Implementation (doc) in "Implementation" = "HOL-Proofs" + options [document_variants = "implementation"] @@ -96,18 +104,19 @@ Tactic theories [parallel_proofs = 0] Logic - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../isar.sty" - "../ttbox.sty" - "../underscore.sty" - "../manual.bib" - "document/build" - "document/root.tex" - "document/style.sty" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "ttbox.sty" + "underscore.sty" + "manual.bib" + document_files + "build" + "root.tex" + "style.sty" session Isar_Ref (doc) in "Isar_Ref" = HOL + options [document_variants = "isar-ref", quick_and_dirty, thy_output_source] @@ -127,41 +136,48 @@ Quick_Reference Symbols ML_Tactic - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../isar.sty" - "../ttbox.sty" - "../underscore.sty" - "../manual.bib" - "document/build" - "document/isar-vm.pdf" - "document/isar-vm.svg" - "document/root.tex" - "document/showsymbols" - "document/style.sty" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "ttbox.sty" + "underscore.sty" + "manual.bib" + document_files + "build" + "isar-vm.pdf" + "isar-vm.svg" + "root.tex" + "showsymbols" + "style.sty" session JEdit (doc) in "JEdit" = HOL + options [document_variants = "jedit", thy_output_source] theories JEdit - files - "../Isar_Ref/document/style.sty" - "../extra.sty" - "../iman.sty" - "../isar.sty" - "../manual.bib" - "../pdfsetup.sty" - "../prepare_document" - "../ttbox.sty" - "../underscore.sty" - "document/build" - "document/isabelle-jedit.png" - "document/popup1.png" - "document/popup2.png" - "document/root.tex" + document_files (in "..") + "extra.sty" + "iman.sty" + "isar.sty" + "manual.bib" + "pdfsetup.sty" + "prepare_document" + "ttbox.sty" + "underscore.sty" + document_files (in "../Isar_Ref/document") + "style.sty" + document_files + "auto-tools.png" + "build" + "find.png" + "isabelle-jedit.png" + "output.png" + "popup1.png" + "popup2.png" + "root.tex" + "sledgehammer.png" session Sugar (doc) in "Sugar" = HOL + options [document_variants = "sugar"] @@ -169,13 +185,14 @@ "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar" theories Sugar - files - "../prepare_document" - "../pdfsetup.sty" - "document/build" - "document/mathpartir.sty" - "document/root.bib" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + document_files + "build" + "mathpartir.sty" + "root.bib" + "root.tex" session Locales (doc) in "Locales" = HOL + options [document_variants = "locales", pretty_margin = 65, skip_proofs = false] @@ -183,30 +200,33 @@ Examples1 Examples2 Examples3 - files - "../prepare_document" - "../pdfsetup.sty" - "document/build" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + document_files + "build" + "root.bib" + "root.tex" session Logics (doc) in "Logics" = Pure + options [document_variants = "logics"] theories - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../ttbox.sty" - "../manual.bib" - "document/CTT.tex" - "document/HOL.tex" - "document/LK.tex" - "document/Sequents.tex" - "document/build" - "document/preface.tex" - "document/root.tex" - "document/syntax.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "ttbox.sty" + "manual.bib" + document_files + "CTT.tex" + "HOL.tex" + "LK.tex" + "Sequents.tex" + "build" + "preface.tex" + "root.tex" + "syntax.tex" session Logics_ZF (doc) in "Logics_ZF" = ZF + options [document_variants = "logics-ZF", print_mode = "brackets", @@ -217,35 +237,42 @@ ZF_examples If ZF_Isar - files - "../prepare_document" - "../pdfsetup.sty" - "../isar.sty" - "../ttbox.sty" - "../manual.bib" - "../Logics/document/syntax.tex" - "document/build" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "isar.sty" + "ttbox.sty" + "manual.bib" + document_files (in "../Logics/document") + "syntax.tex" + document_files + "FOL.tex" + "ZF.tex" + "build" + "logics.sty" + "root.tex" session Main (doc) in "Main" = HOL + options [document_variants = "main"] theories Main_Doc - files - "../prepare_document" - "../pdfsetup.sty" - "document/build" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + document_files + "build" + "root.tex" session Nitpick (doc) in "Nitpick" = Pure + options [document_variants = "nitpick"] theories - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../manual.bib" - "document/build" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "manual.bib" + document_files + "build" + "root.tex" session Prog_Prove (doc) in "Prog_Prove" = HOL + options [document_variants = "prog-prove", show_question_marks = false] @@ -256,28 +283,32 @@ Types_and_funs Logic Isar - files - "../prepare_document" - "../pdfsetup.sty" - "document/bang.pdf" - "document/build" - "document/intro-isabelle.tex" - "document/mathpartir.sty" - "document/prelude.tex" - "document/root.bib" - "document/root.tex" - "document/svmono.cls" + document_files (in ".") + "MyList.thy" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + document_files + "bang.pdf" + "build" + "intro-isabelle.tex" + "mathpartir.sty" + "prelude.tex" + "root.bib" + "root.tex" + "svmono.cls" session Sledgehammer (doc) in "Sledgehammer" = Pure + options [document_variants = "sledgehammer"] theories - files - "../prepare_document" - "../pdfsetup.sty" - "../iman.sty" - "../manual.bib" - "document/build" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "manual.bib" + document_files + "build" + "root.tex" session System (doc) in "System" = Pure + options [document_variants = "system", thy_output_source] @@ -288,19 +319,21 @@ Presentation Scala Misc - files - "../prepare_document" - "../Isar_Ref/document/style.sty" - "../pdfsetup.sty" - "../iman.sty" - "../extra.sty" - "../isar.sty" - "../ttbox.sty" - "../underscore.sty" - "../manual.bib" - "document/browser_screenshot.png" - "document/build" - "document/root.tex" + document_files (in "..") + "prepare_document" + "pdfsetup.sty" + "iman.sty" + "extra.sty" + "isar.sty" + "ttbox.sty" + "underscore.sty" + "manual.bib" + document_files (in "../Isar_Ref/document") + "style.sty" + document_files + "browser_screenshot.png" + "build" + "root.tex" session Tutorial (doc) in "Tutorial" = HOL + options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false] @@ -363,31 +396,33 @@ "Sets/Functions" "Sets/Relations" "Sets/Recur" - files - "ToyList/ToyList1" - "ToyList/ToyList2" - "../pdfsetup.sty" - "../ttbox.sty" - "../manual.bib" - "document/advanced0.tex" - "document/appendix0.tex" - "document/basics.tex" - "document/build" - "document/cl2emono-modified.sty" - "document/ctl0.tex" - "document/documents0.tex" - "document/fp.tex" - "document/inductive0.tex" - "document/isa-index" - "document/Isa-logics.pdf" - "document/numerics.tex" - "document/pghead.pdf" - "document/preface.tex" - "document/protocol.tex" - "document/root.tex" - "document/rules.tex" - "document/sets.tex" - "document/tutorial.sty" - "document/typedef.pdf" - "document/types0.tex" + document_files (in "ToyList") + "ToyList1" + "ToyList2" + document_files (in "..") + "pdfsetup.sty" + "ttbox.sty" + "manual.bib" + document_files + "advanced0.tex" + "appendix0.tex" + "basics.tex" + "build" + "cl2emono-modified.sty" + "ctl0.tex" + "documents0.tex" + "fp.tex" + "inductive0.tex" + "isa-index" + "Isa-logics.pdf" + "numerics.tex" + "pghead.pdf" + "preface.tex" + "protocol.tex" + "root.tex" + "rules.tex" + "sets.tex" + "tutorial.sty" + "typedef.pdf" + "types0.tex" diff -r aff193f53a64 -r 34023a586608 src/Doc/Sledgehammer/document/build --- a/src/Doc/Sledgehammer/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/Sledgehammer/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -6,9 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo -n isabelle_sledgehammer "S/H" - -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/System/Sessions.thy Fri Apr 11 12:43:22 2014 +0200 @@ -54,7 +54,7 @@ @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body ; - body: description? options? ( theories + ) files? + body: description? options? (theories+) \ files? (document_files*) ; spec: @{syntax name} groups? dir? ; @@ -72,7 +72,9 @@ ; theories: @'theories' opts? ( @{syntax name} * ) ; - files: @'files' ( @{syntax name} + ) + files: @'files' (@{syntax name}+) + ; + document_files: @'document_files' ('(' dir ')')? (@{syntax name}+) \} \begin{description} @@ -123,11 +125,24 @@ \item \isakeyword{files}~@{text "files"} lists additional source files that are involved in the processing of this session. This should cover anything outside the formal content of the theory - sources, say some auxiliary {\TeX} files that are required for - document processing. In contrast, files that are loaded formally + sources. In contrast, files that are loaded formally within a theory, e.g.\ via @{keyword "ML_file"}, need not be declared again. + \item \isakeyword{document_files}~@{text "("}\isakeyword{in}~@{text + "base_dir) files"} lists source files for document preparation, + typically @{verbatim ".tex"} and @{verbatim ".sty"} for {\LaTeX}. + Only these explicitly given files are copied from the base directory + to the document output directory, before formal document processing + is started (see also \secref{sec:tool-document}). The local path + structure of the @{text files} is preserved, which allows to + reconstruct the original directory hierarchy of @{text "base_dir"}. + + \item \isakeyword{document_files}~@{text "files"} abbreviates + \isakeyword{document_files}~@{text "("}\isakeyword{in}~@{text + "document) files"}, i.e.\ document sources are taken from the base + directory @{verbatim document} within the session root directory. + \end{description} *} diff -r aff193f53a64 -r 34023a586608 src/Doc/System/document/build --- a/src/Doc/System/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/System/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -6,14 +6,5 @@ VARIANT="$2" "$ISABELLE_TOOL" logo - -cp "$ISABELLE_HOME/src/Doc/Isar_Ref/document/style.sty" . -cp "$ISABELLE_HOME/src/Doc/iman.sty" . -cp "$ISABELLE_HOME/src/Doc/extra.sty" . -cp "$ISABELLE_HOME/src/Doc/isar.sty" . -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/underscore.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" diff -r aff193f53a64 -r 34023a586608 src/Doc/Tutorial/document/build --- a/src/Doc/Tutorial/document/build Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Doc/Tutorial/document/build Fri Apr 11 12:43:22 2014 +0200 @@ -6,16 +6,6 @@ VARIANT="$2" "$ISABELLE_TOOL" logo HOL - -cp "$ISABELLE_HOME/src/Doc/ttbox.sty" . -cp "$ISABELLE_HOME/src/Doc/manual.bib" . - -cp "$ISABELLE_HOME/src/Doc/Tutorial/ToyList/ToyList1" . -cp "$ISABELLE_HOME/src/Doc/Tutorial/ToyList/ToyList2" . - -"$ISABELLE_TOOL" latex -o sty -cp "$ISABELLE_HOME/src/Doc/pdfsetup.sty" . - "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o bbl ./isa-index root diff -r aff193f53a64 -r 34023a586608 src/Pure/General/file.ML --- a/src/Pure/General/file.ML Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Pure/General/file.ML Fri Apr 11 12:43:22 2014 +0200 @@ -35,7 +35,6 @@ val append_list: Path.T -> string list -> unit val write_buffer: Path.T -> Buffer.T -> unit val eq: Path.T * Path.T -> bool - val copy: Path.T -> Path.T -> unit end; structure File: FILE = @@ -165,17 +164,11 @@ fun write_buffer path buf = open_output (Buffer.output buf) path; -(* copy *) +(* eq *) fun eq paths = (case try (pairself (OS.FileSys.fileId o platform_path)) paths of SOME ids => is_equal (OS.FileSys.compare ids) | NONE => false); -fun copy src dst = - if eq (src, dst) then () - else - let val target = if is_dir dst then Path.append dst (Path.base src) else dst - in write target (read src) end; - end; diff -r aff193f53a64 -r 34023a586608 src/Pure/General/path.ML --- a/src/Pure/General/path.ML Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Pure/General/path.ML Fri Apr 11 12:43:22 2014 +0200 @@ -17,6 +17,7 @@ val variable: string -> T val is_absolute: T -> bool val is_basic: T -> bool + val starts_basic: T -> bool val append: T -> T -> T val appends: T list -> T val make: string list -> T @@ -93,6 +94,11 @@ fun is_basic (Path [Basic _]) = true | is_basic _ = false; +fun starts_basic (Path xs) = + (case try List.last xs of + SOME (Basic _) => true + | _ => false); + (* append and norm *) diff -r aff193f53a64 -r 34023a586608 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Pure/General/position.ML Fri Apr 11 12:43:22 2014 +0200 @@ -191,7 +191,7 @@ Unsynchronized.change r (append (map (rpair "") reports)); -(* here: inlined formal markup *) +(* here: user output *) fun here pos = let diff -r aff193f53a64 -r 34023a586608 src/Pure/General/position.scala --- a/src/Pure/General/position.scala Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Pure/General/position.scala Fri Apr 11 12:43:22 2014 +0200 @@ -99,7 +99,7 @@ def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1)) - /* here: inlined formal markup */ + /* here: user output */ def here(pos: T): String = (Line.unapply(pos), File.unapply(pos)) match { @@ -108,4 +108,12 @@ case (None, Some(name)) => " (file " + quote(name) + ")" case _ => "" } + + def here_undelimited(pos: T): String = + (Line.unapply(pos), File.unapply(pos)) match { + case (Some(i), None) => "line " + i.toString + case (Some(i), Some(name)) => "line " + i.toString + " of " + quote(name) + case (None, Some(name)) => "file " + quote(name) + case _ => "" + } } diff -r aff193f53a64 -r 34023a586608 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Pure/Isar/token.scala Fri Apr 11 12:43:22 2014 +0200 @@ -140,7 +140,7 @@ } def position: Position.T = Position.Line_File(line, file) - override def toString: String = Position.here(position) + override def toString: String = Position.here_undelimited(position) } abstract class Reader extends scala.util.parsing.input.Reader[Token] diff -r aff193f53a64 -r 34023a586608 src/Pure/PIDE/session.ML --- a/src/Pure/PIDE/session.ML Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Pure/PIDE/session.ML Fri Apr 11 12:43:22 2014 +0200 @@ -9,7 +9,7 @@ val name: unit -> string val welcome: unit -> string val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> - string -> string * string -> bool * string -> bool -> unit + (Path.T * Path.T) list -> string -> string * string -> bool -> unit val finish: unit -> unit val protocol_handler: string -> unit val init_protocol_handlers: unit -> unit @@ -33,8 +33,8 @@ (* init *) -fun init build info info_path doc doc_graph doc_output doc_variants - parent (chapter, name) doc_dump verbose = +fun init build info info_path doc doc_graph doc_output doc_variants doc_files + parent (chapter, name) verbose = if #name (! session) <> parent orelse not (! session_finished) then error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) else @@ -43,8 +43,8 @@ val _ = session_finished := false; in Present.init build info info_path (if doc = "false" then "" else doc) - doc_graph doc_output doc_variants (chapter, name) - doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ())) + doc_graph doc_output doc_variants doc_files (chapter, name) + verbose (map Thy_Info.get_theory (Thy_Info.get_names ())) end; diff -r aff193f53a64 -r 34023a586608 src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Pure/System/isabelle_system.ML Fri Apr 11 12:43:22 2014 +0200 @@ -10,6 +10,8 @@ val mkdirs: Path.T -> unit val mkdir: Path.T -> unit val copy_dir: Path.T -> Path.T -> unit + val copy_file: Path.T -> Path.T -> unit + val copy_file_base: Path.T * Path.T -> Path.T -> unit val create_tmp_path: string -> string -> Path.T val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a val with_tmp_dir: string -> (Path.T -> 'a) -> 'a @@ -66,6 +68,30 @@ if File.eq (src, dst) then () else (system_command ("cp -p -R -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ()); +fun copy_file src0 dst0 = + let + val src = Path.expand src0; + val dst = Path.expand dst0; + val (target_dir, target) = + if File.is_dir dst then (dst, Path.append dst (Path.base src)) + else (Path.dir dst, dst); + in + if File.eq (src, target) then () + else + (ignore o system_command) + ("cp -p -f " ^ File.shell_path src ^ " " ^ File.shell_path target_dir ^ "/.") + end; + +fun copy_file_base (base_dir, src0) target_dir = + let + val src = Path.expand src0; + val src_dir = Path.dir src; + val _ = + if Path.starts_basic src then () + else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory"); + val _ = mkdirs (Path.append target_dir src_dir); + in copy_file (Path.append base_dir src) (Path.append target_dir src) end; + (* tmp files *) diff -r aff193f53a64 -r 34023a586608 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Pure/Thy/present.ML Fri Apr 11 12:43:22 2014 +0200 @@ -9,7 +9,7 @@ val session_name: theory -> string val read_variant: string -> string * string val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> - string * string -> bool * string -> bool -> theory list -> unit (*not thread-safe!*) + (Path.T * Path.T) list -> string * string -> bool -> theory list -> unit (*not thread-safe!*) val finish: unit -> unit (*not thread-safe!*) val theory_output: string -> string -> unit val begin_theory: int -> (unit -> HTML.text) -> theory -> theory @@ -168,17 +168,17 @@ (* session_info *) type session_info = - {name: string, chapter: string, info_path: Path.T, - info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option, - documents: (string * string) list, doc_dump: (bool * string), verbose: bool, - readme: Path.T option}; + {name: string, chapter: string, info_path: Path.T, info: bool, + doc_format: string, doc_graph: bool, doc_output: Path.T option, + doc_files: (Path.T * Path.T) list, documents: (string * string) list, + verbose: bool, readme: Path.T option}; fun make_session_info (name, chapter, info_path, info, doc_format, doc_graph, doc_output, - documents, doc_dump, verbose, readme) = + doc_files, documents, verbose, readme) = {name = name, chapter = chapter, info_path = info_path, info = info, doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output, - documents = documents, doc_dump = doc_dump, verbose = verbose, + doc_files = doc_files, documents = documents, verbose = verbose, readme = readme}: session_info; @@ -203,9 +203,9 @@ (* init session *) -fun init build info info_path doc doc_graph document_output doc_variants - (chapter, name) (doc_dump as (_, dump_prefix)) verbose thys = - if not build andalso not info andalso doc = "" andalso dump_prefix = "" then +fun init build info info_path doc doc_graph document_output doc_variants doc_files + (chapter, name) verbose thys = + if not build andalso not info andalso doc = "" then (browser_info := empty_browser_info; session_info := NONE) else let @@ -214,7 +214,7 @@ val documents = if doc = "" then [] - else if not (can File.check_dir document_path) then + else if null doc_files andalso not (can File.check_dir document_path) then (if verbose then Output.physical_stderr "Warning: missing document directory\n" else (); []) else doc_variants; @@ -227,7 +227,7 @@ in session_info := SOME (make_session_info (name, chapter, info_path, info, doc, - doc_graph, doc_output, documents, doc_dump, verbose, readme)); + doc_graph, doc_output, doc_files, documents, verbose, readme)); browser_info := init_browser_info (chapter, name) thys; add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html")) end; @@ -275,10 +275,9 @@ fun write_tex_index tex_index path = write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path; - fun finish () = - with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, doc_output, - documents, doc_dump = (dump_copy, dump_prefix), verbose, readme, ...} => + with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, + doc_output, doc_files, documents, verbose, readme, ...} => let val {theories, tex_index, html_index, graph} = ! browser_info; val thys = Symtab.dest theories; @@ -291,7 +290,7 @@ val sorted_graph = sorted_index graph; val opt_graphs = - if doc_graph andalso (not (null documents) orelse dump_prefix <> "") then + if doc_graph andalso not (null documents) then SOME (isabelle_browser sorted_graph) else NONE; @@ -300,58 +299,46 @@ (Isabelle_System.mkdirs session_prefix; File.write_buffer (Path.append session_prefix index_path) (index_buffer html_index |> Buffer.add HTML.end_document); - (case readme of NONE => () | SOME path => File.copy path session_prefix); + (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix); Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_graph; Isabelle_System.isabelle_tool "browser" "-b"; - File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix; + Isabelle_System.copy_file (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix; List.app (fn (a, txt) => File.write (Path.append session_prefix (Path.basic a)) txt) (HTML.applet_pages name (Url.File index_path, name)); - File.copy (Path.explode "~~/etc/isabelle.css") session_prefix; + Isabelle_System.copy_file (Path.explode "~~/etc/isabelle.css") session_prefix; List.app finish_html thys; if verbose then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n") else ()) else (); - fun prepare_sources doc_copy doc_dir = - (Isabelle_System.mkdirs doc_dir; - if doc_copy then Isabelle_System.copy_dir document_path doc_dir else (); - Isabelle_System.isabelle_tool "latex" - ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))); - (case opt_graphs of NONE => () | SOME (pdf, eps) => - (File.write (Path.append doc_dir graph_pdf_path) pdf; - File.write (Path.append doc_dir graph_eps_path) eps)); - write_tex_index tex_index doc_dir; - List.app (fn (a, {tex_source, ...}) => - write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys); - - val _ = - if dump_prefix = "" then () - else - let - val path = Path.explode dump_prefix; - val _ = prepare_sources dump_copy path; - in - if verbose then - Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n") - else () - end; - - fun document_job doc_prefix backdrop (name, tags) = + fun document_job doc_prefix backdrop (doc_name, tags) = let + val doc_dir = Path.append doc_prefix (Path.basic doc_name); + val _ = Isabelle_System.mkdirs doc_dir; val _ = - File.eq (document_path, doc_prefix) andalso - error ("Overlap of document input and output directory " ^ Path.print doc_prefix); - val dir = Path.append doc_prefix (Path.basic name); - val copy = not (File.eq (document_path, dir)); - val _ = prepare_sources copy dir; - fun inform doc = - if verbose orelse not backdrop then - Output.physical_stderr ("Document at " ^ show_path doc ^ "\n") - else (); + Isabelle_System.isabelle_tool "latex" + ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))); + val _ = + if null doc_files then Isabelle_System.copy_dir document_path doc_dir + else List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files; + val _ = + (case opt_graphs of + NONE => () + | SOME (pdf, eps) => + (File.write (Path.append doc_dir graph_pdf_path) pdf; + File.write (Path.append doc_dir graph_eps_path) eps)); + val _ = write_tex_index tex_index doc_dir; + val _ = + List.app (fn (a, {tex_source, ...}) => + write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys; in fn () => - (isabelle_document {verbose = true, purge = backdrop} doc_format name tags dir, inform) + (isabelle_document {verbose = true, purge = backdrop} doc_format doc_name tags doc_dir, + fn doc => + if verbose orelse not backdrop then + Output.physical_stderr ("Document at " ^ show_path doc ^ "\n") + else ()) end; val jobs = @@ -362,6 +349,12 @@ NONE => [] | SOME path => map (document_job path false) documents); + val _ = + if not (null jobs) andalso null doc_files then + Output.physical_stderr ("### Document preparation for session " ^ quote name ^ + " without 'document_files'\n") + else (); + val _ = jobs |> Par_List.map (fn job => job ()) |> List.app (op |>); in browser_info := empty_browser_info; @@ -425,7 +418,7 @@ val doc_path = Path.append dir document_path; val _ = Isabelle_System.mkdirs doc_path; val root_path = Path.append doc_path (Path.basic "root.tex"); - val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path; + val _ = Isabelle_System.copy_file (Path.explode "~~/lib/texinputs/draft.tex") root_path; val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path); val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path); @@ -447,7 +440,7 @@ val target_dir = Path.explode "$ISABELLE_HOME_USER/tmp"; val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf" val _ = Isabelle_System.mkdirs target_dir; - val _ = File.copy result target; + val _ = Isabelle_System.copy_file result target; in Isabelle_System.isabelle_tool "display" (File.shell_path target ^ " &") end); diff -r aff193f53a64 -r 34023a586608 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Pure/Tools/build.ML Fri Apr 11 12:43:22 2014 +0200 @@ -130,12 +130,12 @@ val _ = SHA1_Samples.test (); val (command_timings, (do_output, (options, (verbose, (browser_info, - (parent_name, (chapter, (name, theories)))))))) = + (document_files, (parent_name, (chapter, (name, theories))))))))) = File.read (Path.explode args_file) |> YXML.parse_body |> let open XML.Decode in pair (list properties) (pair bool (pair Options.decode (pair bool (pair string - (pair string (pair string (pair string - ((list (pair Options.decode (list string))))))))))) + (pair (list (pair string string)) (pair string (pair string (pair string + ((list (pair Options.decode (list string)))))))))))) end; val _ = Options.set_default options; @@ -156,8 +156,8 @@ (Options.bool options "document_graph") (Options.string options "document_output") document_variants + (map (pairself Path.explode) document_files) parent_name (chapter, name) - (false, "") verbose; val last_timing = lookup_timings (fold update_timings command_timings empty_timings); diff -r aff193f53a64 -r 34023a586608 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Apr 09 14:08:25 2014 +0200 +++ b/src/Pure/Tools/build.scala Fri Apr 11 12:43:22 2014 +0200 @@ -58,7 +58,8 @@ description: String, options: List[Options.Spec], theories: List[(List[Options.Spec], List[String])], - files: List[String]) extends Entry + files: List[String], + document_files: List[(String, String)]) extends Entry // internal version sealed case class Session_Info( @@ -72,6 +73,7 @@ options: Options, theories: List[(Options, List[Path])], files: List[Path], + document_files: List[(Path, Path)], entry_digest: SHA1.Digest) def is_pure(name: String): Boolean = name == "RAW" || name == "Pure" @@ -91,12 +93,17 @@ entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(Path.explode(_))) }) val files = entry.files.map(Path.explode(_)) + val document_files = + entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) }) + val entry_digest = - SHA1.digest((chapter, name, entry.parent, entry.options, entry.theories).toString) + SHA1.digest((chapter, name, entry.parent, entry.options, + entry.theories, entry.files, entry.document_files).toString) val info = Session_Info(chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path), - entry.parent, entry.description, session_options, theories, files, entry_digest) + entry.parent, entry.description, session_options, theories, files, + document_files, entry_digest) (name, info) } @@ -195,11 +202,12 @@ private val OPTIONS = "options" private val THEORIES = "theories" private val FILES = "files" + private val DOCUMENT_FILES = "document_files" lazy val root_syntax = Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) + - IN + DESCRIPTION + OPTIONS + THEORIES + FILES + IN + DESCRIPTION + OPTIONS + THEORIES + FILES + DOCUMENT_FILES private object Parser extends Parse.Parser { @@ -222,6 +230,12 @@ keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^ { case _ ~ (x ~ y) => (x, y) } + val document_files = + keyword(DOCUMENT_FILES) ~! + ((keyword("(") ~! (keyword(IN) ~! (path ~ keyword(")"))) ^^ + { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~ + rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) } + command(SESSION) ~! (session_name ~ ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~ @@ -231,9 +245,10 @@ ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~ ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~ rep1(theories) ~ - ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^ - { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) => - Session_Entry(pos, a, b, c, d, e, f, g, h) } + ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~ + (rep(document_files) ^^ (x => x.flatten))))) ^^ + { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) => + Session_Entry(pos, a, b, c, d, e, f, g, h, i) } } def parse_entries(root: Path): List[(String, Session_Entry)] = @@ -445,7 +460,8 @@ val all_files = (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: loaded_files ::: - info.files.map(file => info.dir + file)).map(_.expand) + info.files.map(file => info.dir + file) ::: + info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) if (list_files) { progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _))) @@ -513,10 +529,10 @@ { import XML.Encode._ pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, - pair(string, pair(string, pair(string, - list(pair(Options.encode, list(Path.encode)))))))))))( + pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, + list(pair(Options.encode, list(Path.encode))))))))))))( (command_timings, (do_output, (info.options, (verbose, (browser_info, - (parent, (info.chapter, (name, info.theories))))))))) + (info.document_files, (parent, (info.chapter, (name, info.theories)))))))))) })) private val env =