# HG changeset patch
# User wenzelm
# Date 1407679152 -7200
# Node ID 0835aa55ba21291a86936f4f502c232862b9ce28
# Parent  36b5691b81a542f66cf9522d148bc49a83a8df50
insist in proper 'document_files';

diff -r 36b5691b81a5 -r 0835aa55ba21 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun Aug 10 15:45:06 2014 +0200
+++ b/src/Pure/Thy/present.ML	Sun Aug 10 15:59:12 2014 +0200
@@ -330,9 +330,7 @@
         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 _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
         val _ =
           (case opt_graphs of
             NONE => ()
@@ -360,12 +358,6 @@
         NONE => []
       | SOME path => map (document_job path false) documents);
 
-    val _ =
-      if not (null jobs) andalso null doc_files then
-        Output.physical_stderr ("### Legacy feature! 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;