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 =