# HG changeset patch # User wenzelm # Date 1397209948 -7200 # Node ID cd8b6d849b6a7b9957fecddf03c63c08ec3e1554 # Parent 3da244bc02bde8375c39bfe991669f48bb9994a3 explicit 'document_files' in session ROOT specifications; clarified Isabelle_System.copy_file(_base): preserve file-attributes and local directory hierarchy; diff -r 3da244bc02bd -r cd8b6d849b6a NEWS --- 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 diff -r 3da244bc02bd -r cd8b6d849b6a src/Doc/System/Sessions.thy --- 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+) \ 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 3da244bc02bd -r cd8b6d849b6a src/Pure/General/file.ML --- 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; diff -r 3da244bc02bd -r cd8b6d849b6a src/Pure/General/path.ML --- 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 *) diff -r 3da244bc02bd -r cd8b6d849b6a src/Pure/PIDE/session.ML --- 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; diff -r 3da244bc02bd -r cd8b6d849b6a src/Pure/System/isabelle_system.ML --- 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 *) diff -r 3da244bc02bd -r cd8b6d849b6a src/Pure/Thy/present.ML --- 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); diff -r 3da244bc02bd -r cd8b6d849b6a src/Pure/Tools/build.ML --- 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; diff -r 3da244bc02bd -r cd8b6d849b6a src/Pure/Tools/build.scala --- 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 =