explicit 'document_files' in session ROOT specifications;
authorwenzelm
Fri Apr 11 11:52:28 2014 +0200 (2014-04-11)
changeset 56533cd8b6d849b6a
parent 56532 3da244bc02bd
child 56534 3ff16a7f0b2e
explicit 'document_files' in session ROOT specifications;
clarified Isabelle_System.copy_file(_base): preserve file-attributes and local directory hierarchy;
NEWS
src/Doc/System/Sessions.thy
src/Pure/General/file.ML
src/Pure/General/path.ML
src/Pure/PIDE/session.ML
src/Pure/System/isabelle_system.ML
src/Pure/Thy/present.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Fri Apr 11 09:36:38 2014 +0200
     1.2 +++ b/NEWS	Fri Apr 11 11:52:28 2014 +0200
     1.3 @@ -658,6 +658,11 @@
     1.4  
     1.5  *** System ***
     1.6  
     1.7 +* Session ROOT specifications support explicit 'document_files' for
     1.8 +robust dependencies on LaTeX sources.  Only these explicitly given
     1.9 +files are copied to the document output directory, before document
    1.10 +processing is started.
    1.11 +
    1.12  * Simplified "isabelle display" tool.  Settings variables DVI_VIEWER
    1.13  and PDF_VIEWER now refer to the actual programs, not shell
    1.14  command-lines.  Discontinued option -c: invocation may be asynchronous
     2.1 --- a/src/Doc/System/Sessions.thy	Fri Apr 11 09:36:38 2014 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Fri Apr 11 11:52:28 2014 +0200
     2.3 @@ -54,7 +54,7 @@
     2.4  
     2.5      @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
     2.6      ;
     2.7 -    body: description? options? ( theories + ) files?
     2.8 +    body: description? options? (theories+) \<newline> files? (document_files*)
     2.9      ;
    2.10      spec: @{syntax name} groups? dir?
    2.11      ;
    2.12 @@ -72,7 +72,9 @@
    2.13      ;
    2.14      theories: @'theories' opts? ( @{syntax name} * )
    2.15      ;
    2.16 -    files: @'files' ( @{syntax name} + )
    2.17 +    files: @'files' (@{syntax name}+)
    2.18 +    ;
    2.19 +    document_files: @'document_files' ('(' dir ')')? (@{syntax name}+)
    2.20    \<close>}
    2.21  
    2.22    \begin{description}
    2.23 @@ -123,11 +125,24 @@
    2.24    \item \isakeyword{files}~@{text "files"} lists additional source
    2.25    files that are involved in the processing of this session.  This
    2.26    should cover anything outside the formal content of the theory
    2.27 -  sources, say some auxiliary {\TeX} files that are required for
    2.28 -  document processing.  In contrast, files that are loaded formally
    2.29 +  sources.  In contrast, files that are loaded formally
    2.30    within a theory, e.g.\ via @{keyword "ML_file"}, need not be
    2.31    declared again.
    2.32  
    2.33 +  \item \isakeyword{document_files}~@{text "("}\isakeyword{in}~@{text
    2.34 +  "base_dir) files"} lists source files for document preparation,
    2.35 +  typically @{verbatim ".tex"} and @{verbatim ".sty"} for {\LaTeX}.
    2.36 +  Only these explicitly given files are copied from the base directory
    2.37 +  to the document output directory, before formal document processing
    2.38 +  is started (see also \secref{sec:tool-document}).  The local path
    2.39 +  structure of the @{text files} is preserved, which allows to
    2.40 +  reconstruct the original directory hierarchy of @{text "base_dir"}.
    2.41 +
    2.42 +  \item \isakeyword{document_files}~@{text "files"} abbreviates
    2.43 +  \isakeyword{document_files}~@{text "("}\isakeyword{in}~@{text
    2.44 +  "document) files"}, i.e.\ document sources are taken from the base
    2.45 +  directory @{verbatim document} within the session root directory.
    2.46 +
    2.47    \end{description}
    2.48  *}
    2.49  
     3.1 --- a/src/Pure/General/file.ML	Fri Apr 11 09:36:38 2014 +0200
     3.2 +++ b/src/Pure/General/file.ML	Fri Apr 11 11:52:28 2014 +0200
     3.3 @@ -35,7 +35,6 @@
     3.4    val append_list: Path.T -> string list -> unit
     3.5    val write_buffer: Path.T -> Buffer.T -> unit
     3.6    val eq: Path.T * Path.T -> bool
     3.7 -  val copy: Path.T -> Path.T -> unit
     3.8  end;
     3.9  
    3.10  structure File: FILE =
    3.11 @@ -165,17 +164,11 @@
    3.12  fun write_buffer path buf = open_output (Buffer.output buf) path;
    3.13  
    3.14  
    3.15 -(* copy *)
    3.16 +(* eq *)
    3.17  
    3.18  fun eq paths =
    3.19    (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
    3.20      SOME ids => is_equal (OS.FileSys.compare ids)
    3.21    | NONE => false);
    3.22  
    3.23 -fun copy src dst =
    3.24 -  if eq (src, dst) then ()
    3.25 -  else
    3.26 -    let val target = if is_dir dst then Path.append dst (Path.base src) else dst
    3.27 -    in write target (read src) end;
    3.28 -
    3.29  end;
     4.1 --- a/src/Pure/General/path.ML	Fri Apr 11 09:36:38 2014 +0200
     4.2 +++ b/src/Pure/General/path.ML	Fri Apr 11 11:52:28 2014 +0200
     4.3 @@ -17,6 +17,7 @@
     4.4    val variable: string -> T
     4.5    val is_absolute: T -> bool
     4.6    val is_basic: T -> bool
     4.7 +  val starts_basic: T -> bool
     4.8    val append: T -> T -> T
     4.9    val appends: T list -> T
    4.10    val make: string list -> T
    4.11 @@ -93,6 +94,11 @@
    4.12  fun is_basic (Path [Basic _]) = true
    4.13    | is_basic _ = false;
    4.14  
    4.15 +fun starts_basic (Path xs) =
    4.16 +  (case try List.last xs of
    4.17 +    SOME (Basic _) => true
    4.18 +  | _ => false);
    4.19 +
    4.20  
    4.21  (* append and norm *)
    4.22  
     5.1 --- a/src/Pure/PIDE/session.ML	Fri Apr 11 09:36:38 2014 +0200
     5.2 +++ b/src/Pure/PIDE/session.ML	Fri Apr 11 11:52:28 2014 +0200
     5.3 @@ -9,7 +9,7 @@
     5.4    val name: unit -> string
     5.5    val welcome: unit -> string
     5.6    val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     5.7 -    string -> string * string -> bool -> unit
     5.8 +    (Path.T * Path.T) list -> string -> string * string -> bool -> unit
     5.9    val finish: unit -> unit
    5.10    val protocol_handler: string -> unit
    5.11    val init_protocol_handlers: unit -> unit
    5.12 @@ -33,7 +33,7 @@
    5.13  
    5.14  (* init *)
    5.15  
    5.16 -fun init build info info_path doc doc_graph doc_output doc_variants
    5.17 +fun init build info info_path doc doc_graph doc_output doc_variants doc_files
    5.18      parent (chapter, name) verbose =
    5.19    if #name (! session) <> parent orelse not (! session_finished) then
    5.20      error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    5.21 @@ -43,7 +43,7 @@
    5.22        val _ = session_finished := false;
    5.23      in
    5.24        Present.init build info info_path (if doc = "false" then "" else doc)
    5.25 -        doc_graph doc_output doc_variants (chapter, name)
    5.26 +        doc_graph doc_output doc_variants doc_files (chapter, name)
    5.27          verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
    5.28      end;
    5.29  
     6.1 --- a/src/Pure/System/isabelle_system.ML	Fri Apr 11 09:36:38 2014 +0200
     6.2 +++ b/src/Pure/System/isabelle_system.ML	Fri Apr 11 11:52:28 2014 +0200
     6.3 @@ -10,6 +10,8 @@
     6.4    val mkdirs: Path.T -> unit
     6.5    val mkdir: Path.T -> unit
     6.6    val copy_dir: Path.T -> Path.T -> unit
     6.7 +  val copy_file: Path.T -> Path.T -> unit
     6.8 +  val copy_file_base: Path.T * Path.T -> Path.T -> unit
     6.9    val create_tmp_path: string -> string -> Path.T
    6.10    val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
    6.11    val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
    6.12 @@ -66,6 +68,30 @@
    6.13    if File.eq (src, dst) then ()
    6.14    else (system_command ("cp -p -R -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
    6.15  
    6.16 +fun copy_file src0 dst0 =
    6.17 +  let
    6.18 +    val src = Path.expand src0;
    6.19 +    val dst = Path.expand dst0;
    6.20 +    val (target_dir, target) =
    6.21 +      if File.is_dir dst then (dst, Path.append dst (Path.base src))
    6.22 +      else (Path.dir dst, dst);
    6.23 +  in
    6.24 +    if File.eq (src, target) then ()
    6.25 +    else
    6.26 +      (ignore o system_command)
    6.27 +        ("cp -p -f " ^ File.shell_path src ^ " " ^ File.shell_path target_dir ^ "/.")
    6.28 +  end;
    6.29 +
    6.30 +fun copy_file_base (base_dir, src0) target_dir =
    6.31 +  let
    6.32 +    val src = Path.expand src0;
    6.33 +    val src_dir = Path.dir src;
    6.34 +    val _ =
    6.35 +      if Path.starts_basic src then ()
    6.36 +      else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory");
    6.37 +    val _ = mkdirs (Path.append target_dir src_dir);
    6.38 +  in copy_file (Path.append base_dir src) (Path.append target_dir src) end;
    6.39 +
    6.40  
    6.41  (* tmp files *)
    6.42  
     7.1 --- a/src/Pure/Thy/present.ML	Fri Apr 11 09:36:38 2014 +0200
     7.2 +++ b/src/Pure/Thy/present.ML	Fri Apr 11 11:52:28 2014 +0200
     7.3 @@ -9,7 +9,7 @@
     7.4    val session_name: theory -> string
     7.5    val read_variant: string -> string * string
     7.6    val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     7.7 -    string * string -> bool -> theory list -> unit  (*not thread-safe!*)
     7.8 +    (Path.T * Path.T) list -> string * string -> bool -> theory list -> unit  (*not thread-safe!*)
     7.9    val finish: unit -> unit  (*not thread-safe!*)
    7.10    val theory_output: string -> string -> unit
    7.11    val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
    7.12 @@ -170,15 +170,15 @@
    7.13  type session_info =
    7.14    {name: string, chapter: string, info_path: Path.T, info: bool,
    7.15      doc_format: string, doc_graph: bool, doc_output: Path.T option,
    7.16 -    documents: (string * string) list, verbose: bool,
    7.17 -    readme: Path.T option};
    7.18 +    doc_files: (Path.T * Path.T) list, documents: (string * string) list,
    7.19 +    verbose: bool, readme: Path.T option};
    7.20  
    7.21  fun make_session_info
    7.22    (name, chapter, info_path, info, doc_format, doc_graph, doc_output,
    7.23 -    documents, verbose, readme) =
    7.24 +    doc_files, documents, verbose, readme) =
    7.25    {name = name, chapter = chapter, info_path = info_path, info = info,
    7.26      doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
    7.27 -    documents = documents, verbose = verbose,
    7.28 +    doc_files = doc_files, documents = documents, verbose = verbose,
    7.29      readme = readme}: session_info;
    7.30  
    7.31  
    7.32 @@ -203,7 +203,7 @@
    7.33  
    7.34  (* init session *)
    7.35  
    7.36 -fun init build info info_path doc doc_graph document_output doc_variants
    7.37 +fun init build info info_path doc doc_graph document_output doc_variants doc_files
    7.38      (chapter, name) verbose thys =
    7.39    if not build andalso not info andalso doc = "" then
    7.40      (browser_info := empty_browser_info; session_info := NONE)
    7.41 @@ -214,7 +214,7 @@
    7.42  
    7.43        val documents =
    7.44          if doc = "" then []
    7.45 -        else if not (can File.check_dir document_path) then
    7.46 +        else if null doc_files andalso not (can File.check_dir document_path) then
    7.47            (if verbose then Output.physical_stderr "Warning: missing document directory\n"
    7.48             else (); [])
    7.49          else doc_variants;
    7.50 @@ -227,7 +227,7 @@
    7.51      in
    7.52        session_info :=
    7.53          SOME (make_session_info (name, chapter, info_path, info, doc,
    7.54 -          doc_graph, doc_output, documents, verbose, readme));
    7.55 +          doc_graph, doc_output, doc_files, documents, verbose, readme));
    7.56        browser_info := init_browser_info (chapter, name) thys;
    7.57        add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html"))
    7.58      end;
    7.59 @@ -275,10 +275,9 @@
    7.60  fun write_tex_index tex_index path =
    7.61    write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
    7.62  
    7.63 -
    7.64  fun finish () =
    7.65 -  with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, doc_output,
    7.66 -    documents, verbose, readme, ...} =>
    7.67 +  with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph,
    7.68 +    doc_output, doc_files, documents, verbose, readme, ...} =>
    7.69    let
    7.70      val {theories, tex_index, html_index, graph} = ! browser_info;
    7.71      val thys = Symtab.dest theories;
    7.72 @@ -300,33 +299,30 @@
    7.73         (Isabelle_System.mkdirs session_prefix;
    7.74          File.write_buffer (Path.append session_prefix index_path)
    7.75            (index_buffer html_index |> Buffer.add HTML.end_document);
    7.76 -        (case readme of NONE => () | SOME path => File.copy path session_prefix);
    7.77 +        (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix);
    7.78          Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_graph;
    7.79          Isabelle_System.isabelle_tool "browser" "-b";
    7.80 -        File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix;
    7.81 +        Isabelle_System.copy_file (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix;
    7.82          List.app (fn (a, txt) => File.write (Path.append session_prefix (Path.basic a)) txt)
    7.83            (HTML.applet_pages name (Url.File index_path, name));
    7.84 -        File.copy (Path.explode "~~/etc/isabelle.css") session_prefix;
    7.85 +        Isabelle_System.copy_file (Path.explode "~~/etc/isabelle.css") session_prefix;
    7.86          List.app finish_html thys;
    7.87          if verbose
    7.88          then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n")
    7.89          else ())
    7.90        else ();
    7.91  
    7.92 -    fun document_job doc_prefix backdrop (name, tags) =
    7.93 +    fun document_job doc_prefix backdrop (doc_name, tags) =
    7.94        let
    7.95 -        val _ =
    7.96 -          File.eq (document_path, doc_prefix) andalso
    7.97 -            error ("Overlap of document input and output directory " ^ Path.print doc_prefix);
    7.98 -        val doc_dir = Path.append doc_prefix (Path.basic name);
    7.99 +        val doc_dir = Path.append doc_prefix (Path.basic doc_name);
   7.100          val _ = Isabelle_System.mkdirs doc_dir;
   7.101          val _ =
   7.102 -          if File.eq (document_path, doc_dir) then ()
   7.103 -          else Isabelle_System.copy_dir document_path doc_dir;
   7.104 -        val _ =
   7.105            Isabelle_System.isabelle_tool "latex"
   7.106              ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")));
   7.107          val _ =
   7.108 +          if null doc_files then Isabelle_System.copy_dir document_path doc_dir
   7.109 +          else List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
   7.110 +        val _ =
   7.111            (case opt_graphs of
   7.112              NONE => ()
   7.113            | SOME (pdf, eps) =>
   7.114 @@ -338,7 +334,7 @@
   7.115              write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys;
   7.116        in
   7.117          fn () =>
   7.118 -          (isabelle_document {verbose = true, purge = backdrop} doc_format name tags doc_dir,
   7.119 +          (isabelle_document {verbose = true, purge = backdrop} doc_format doc_name tags doc_dir,
   7.120              fn doc =>
   7.121                if verbose orelse not backdrop then
   7.122                  Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")
   7.123 @@ -353,6 +349,12 @@
   7.124          NONE => []
   7.125        | SOME path => map (document_job path false) documents);
   7.126  
   7.127 +    val _ =
   7.128 +      if not (null jobs) andalso null doc_files then
   7.129 +        Output.physical_stderr ("### Document preparation for session " ^ quote name ^
   7.130 +          " without 'document_files'\n")
   7.131 +      else ();
   7.132 +
   7.133      val _ = jobs |> Par_List.map (fn job => job ()) |> List.app (op |>);
   7.134    in
   7.135      browser_info := empty_browser_info;
   7.136 @@ -416,7 +418,7 @@
   7.137      val doc_path = Path.append dir document_path;
   7.138      val _ = Isabelle_System.mkdirs doc_path;
   7.139      val root_path = Path.append doc_path (Path.basic "root.tex");
   7.140 -    val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
   7.141 +    val _ = Isabelle_System.copy_file (Path.explode "~~/lib/texinputs/draft.tex") root_path;
   7.142      val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
   7.143      val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
   7.144  
   7.145 @@ -438,7 +440,7 @@
   7.146      val target_dir = Path.explode "$ISABELLE_HOME_USER/tmp";
   7.147      val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf"
   7.148      val _ = Isabelle_System.mkdirs target_dir;
   7.149 -    val _ = File.copy result target;
   7.150 +    val _ = Isabelle_System.copy_file result target;
   7.151    in
   7.152      Isabelle_System.isabelle_tool "display" (File.shell_path target ^ " &")
   7.153    end);
     8.1 --- a/src/Pure/Tools/build.ML	Fri Apr 11 09:36:38 2014 +0200
     8.2 +++ b/src/Pure/Tools/build.ML	Fri Apr 11 11:52:28 2014 +0200
     8.3 @@ -130,12 +130,12 @@
     8.4        val _ = SHA1_Samples.test ();
     8.5  
     8.6        val (command_timings, (do_output, (options, (verbose, (browser_info,
     8.7 -          (parent_name, (chapter, (name, theories)))))))) =
     8.8 +          (document_files, (parent_name, (chapter, (name, theories))))))))) =
     8.9          File.read (Path.explode args_file) |> YXML.parse_body |>
    8.10            let open XML.Decode in
    8.11              pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
    8.12 -              (pair string (pair string (pair string
    8.13 -                ((list (pair Options.decode (list string)))))))))))
    8.14 +              (pair (list (pair string string)) (pair string (pair string (pair string
    8.15 +                ((list (pair Options.decode (list string))))))))))))
    8.16            end;
    8.17  
    8.18        val _ = Options.set_default options;
    8.19 @@ -156,6 +156,7 @@
    8.20            (Options.bool options "document_graph")
    8.21            (Options.string options "document_output")
    8.22            document_variants
    8.23 +          (map (pairself Path.explode) document_files)
    8.24            parent_name (chapter, name)
    8.25            verbose;
    8.26  
     9.1 --- a/src/Pure/Tools/build.scala	Fri Apr 11 09:36:38 2014 +0200
     9.2 +++ b/src/Pure/Tools/build.scala	Fri Apr 11 11:52:28 2014 +0200
     9.3 @@ -58,7 +58,8 @@
     9.4      description: String,
     9.5      options: List[Options.Spec],
     9.6      theories: List[(List[Options.Spec], List[String])],
     9.7 -    files: List[String]) extends Entry
     9.8 +    files: List[String],
     9.9 +    document_files: List[(String, String)]) extends Entry
    9.10  
    9.11    // internal version
    9.12    sealed case class Session_Info(
    9.13 @@ -72,6 +73,7 @@
    9.14      options: Options,
    9.15      theories: List[(Options, List[Path])],
    9.16      files: List[Path],
    9.17 +    document_files: List[(Path, Path)],
    9.18      entry_digest: SHA1.Digest)
    9.19  
    9.20    def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
    9.21 @@ -91,12 +93,17 @@
    9.22          entry.theories.map({ case (opts, thys) =>
    9.23            (session_options ++ opts, thys.map(Path.explode(_))) })
    9.24        val files = entry.files.map(Path.explode(_))
    9.25 +      val document_files =
    9.26 +        entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
    9.27 +
    9.28        val entry_digest =
    9.29 -        SHA1.digest((chapter, name, entry.parent, entry.options, entry.theories).toString)
    9.30 +        SHA1.digest((chapter, name, entry.parent, entry.options,
    9.31 +          entry.theories, entry.files, entry.document_files).toString)
    9.32  
    9.33        val info =
    9.34          Session_Info(chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
    9.35 -          entry.parent, entry.description, session_options, theories, files, entry_digest)
    9.36 +          entry.parent, entry.description, session_options, theories, files,
    9.37 +          document_files, entry_digest)
    9.38  
    9.39        (name, info)
    9.40      }
    9.41 @@ -195,11 +202,12 @@
    9.42    private val OPTIONS = "options"
    9.43    private val THEORIES = "theories"
    9.44    private val FILES = "files"
    9.45 +  private val DOCUMENT_FILES = "document_files"
    9.46  
    9.47    lazy val root_syntax =
    9.48      Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
    9.49        (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
    9.50 -      IN + DESCRIPTION + OPTIONS + THEORIES + FILES
    9.51 +      IN + DESCRIPTION + OPTIONS + THEORIES + FILES + DOCUMENT_FILES
    9.52  
    9.53    private object Parser extends Parse.Parser
    9.54    {
    9.55 @@ -222,6 +230,12 @@
    9.56          keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^
    9.57            { case _ ~ (x ~ y) => (x, y) }
    9.58  
    9.59 +      val document_files =
    9.60 +        keyword(DOCUMENT_FILES) ~!
    9.61 +          ((keyword("(") ~! (keyword(IN) ~! (path ~ keyword(")"))) ^^
    9.62 +              { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
    9.63 +            rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
    9.64 +
    9.65        command(SESSION) ~!
    9.66          (session_name ~
    9.67            ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
    9.68 @@ -231,9 +245,10 @@
    9.69                ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
    9.70                ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
    9.71                rep1(theories) ~
    9.72 -              ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^
    9.73 -        { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
    9.74 -            Session_Entry(pos, a, b, c, d, e, f, g, h) }
    9.75 +              ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
    9.76 +              (rep(document_files) ^^ (x => x.flatten))))) ^^
    9.77 +        { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
    9.78 +            Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
    9.79      }
    9.80  
    9.81      def parse_entries(root: Path): List[(String, Session_Entry)] =
    9.82 @@ -445,7 +460,8 @@
    9.83  
    9.84              val all_files =
    9.85                (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: loaded_files :::
    9.86 -                info.files.map(file => info.dir + file)).map(_.expand)
    9.87 +                info.files.map(file => info.dir + file) :::
    9.88 +                info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
    9.89  
    9.90              if (list_files) {
    9.91                progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
    9.92 @@ -513,10 +529,10 @@
    9.93          {
    9.94            import XML.Encode._
    9.95                pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
    9.96 -                pair(string, pair(string, pair(string,
    9.97 -                  list(pair(Options.encode, list(Path.encode)))))))))))(
    9.98 +                pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string,
    9.99 +                  list(pair(Options.encode, list(Path.encode))))))))))))(
   9.100                (command_timings, (do_output, (info.options, (verbose, (browser_info,
   9.101 -                (parent, (info.chapter, (name, info.theories)))))))))
   9.102 +                (info.document_files, (parent, (info.chapter, (name, info.theories))))))))))
   9.103          }))
   9.104  
   9.105      private val env =