explicit 'document_files' in session ROOT specifications;
clarified Isabelle_System.copy_file(_base): preserve file-attributes and local directory hierarchy;
--- a/NEWS Fri Apr 11 09:36:38 2014 +0200
+++ b/NEWS Fri Apr 11 11:52:28 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/System/Sessions.thy Fri Apr 11 09:36:38 2014 +0200
+++ b/src/Doc/System/Sessions.thy Fri Apr 11 11:52:28 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/Pure/General/file.ML Fri Apr 11 09:36:38 2014 +0200
+++ b/src/Pure/General/file.ML Fri Apr 11 11:52:28 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 Fri Apr 11 09:36:38 2014 +0200
+++ b/src/Pure/General/path.ML Fri Apr 11 11:52:28 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/PIDE/session.ML Fri Apr 11 09:36:38 2014 +0200
+++ b/src/Pure/PIDE/session.ML Fri Apr 11 11:52:28 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 -> 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,7 +33,7 @@
(* init *)
-fun init build info info_path doc doc_graph doc_output doc_variants
+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)
@@ -43,7 +43,7 @@
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_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 Fri Apr 11 09:36:38 2014 +0200
+++ b/src/Pure/System/isabelle_system.ML Fri Apr 11 11:52:28 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 Fri Apr 11 09:36:38 2014 +0200
+++ b/src/Pure/Thy/present.ML Fri Apr 11 11:52:28 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 -> 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
@@ -170,15 +170,15 @@
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, verbose: bool,
- readme: 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, 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, verbose = verbose,
+ doc_files = doc_files, documents = documents, verbose = verbose,
readme = readme}: session_info;
@@ -203,7 +203,7 @@
(* init session *)
-fun init build info info_path doc doc_graph document_output doc_variants
+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)
@@ -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, 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, 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;
@@ -300,33 +299,30 @@
(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 document_job doc_prefix backdrop (name, tags) =
+ fun document_job doc_prefix backdrop (doc_name, tags) =
let
- val _ =
- File.eq (document_path, doc_prefix) andalso
- error ("Overlap of document input and output directory " ^ Path.print doc_prefix);
- val doc_dir = Path.append doc_prefix (Path.basic name);
+ val doc_dir = Path.append doc_prefix (Path.basic doc_name);
val _ = Isabelle_System.mkdirs doc_dir;
val _ =
- if File.eq (document_path, doc_dir) then ()
- else Isabelle_System.copy_dir document_path doc_dir;
- val _ =
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) =>
@@ -338,7 +334,7 @@
write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys;
in
fn () =>
- (isabelle_document {verbose = true, purge = backdrop} doc_format name tags doc_dir,
+ (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")
@@ -353,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;
@@ -416,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);
@@ -438,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 Fri Apr 11 09:36:38 2014 +0200
+++ b/src/Pure/Tools/build.ML Fri Apr 11 11:52:28 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,6 +156,7 @@
(Options.bool options "document_graph")
(Options.string options "document_output")
document_variants
+ (map (pairself Path.explode) document_files)
parent_name (chapter, name)
verbose;
--- a/src/Pure/Tools/build.scala Fri Apr 11 09:36:38 2014 +0200
+++ b/src/Pure/Tools/build.scala Fri Apr 11 11:52:28 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 =