--- 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
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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+) \<newline> 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}+)
\<close>}
\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}
*}
--- 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"
--- 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
--- 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;
--- 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 *)
--- 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
--- 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 _ => ""
+ }
}
--- 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]
--- 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;
--- 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 *)
--- 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);
--- 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);
--- 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 =