src/Pure/Thy/present.ML
changeset 48933 d25e47e32bc0
parent 48805 c3ea910b3581
child 48935 4c92a2f310b6
     1.1 --- a/src/Pure/Thy/present.ML	Sun Aug 19 17:45:07 2012 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Mon Aug 27 14:34:54 2012 +0200
     1.3 @@ -383,19 +383,6 @@
     1.4          SOME (isabelle_browser sorted_graph)
     1.5        else NONE;
     1.6  
     1.7 -    fun prepare_sources doc_dir doc_mode =
     1.8 -     (Isabelle_System.mkdirs doc_dir;
     1.9 -      (case doc_mode of
    1.10 -        Dump_all => Isabelle_System.copy_dir document_path doc_dir
    1.11 -      | Dump_tex_sty =>
    1.12 -          ignore (Isabelle_System.isabelle_tool "latex"
    1.13 -            ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))))
    1.14 -      | Dump_tex => ());
    1.15 -      (case opt_graphs of NONE => () | SOME (pdf, eps) =>
    1.16 -        (File.write (Path.append doc_dir graph_pdf_path) pdf;
    1.17 -          File.write (Path.append doc_dir graph_eps_path) eps));
    1.18 -      write_tex_index tex_index doc_dir;
    1.19 -      List.app (fn (a, {tex_source, ...}) => write_tex tex_source a doc_dir) thys);
    1.20      val _ =
    1.21        if info then
    1.22         (Isabelle_System.mkdirs (Path.append html_prefix session_path);
    1.23 @@ -416,6 +403,20 @@
    1.24          else ())
    1.25        else ();
    1.26  
    1.27 +    fun prepare_sources doc_dir doc_mode =
    1.28 +     (Isabelle_System.mkdirs doc_dir;
    1.29 +      (case doc_mode of
    1.30 +        Dump_all => Isabelle_System.copy_dir document_path doc_dir
    1.31 +      | Dump_tex_sty =>
    1.32 +          ignore (Isabelle_System.isabelle_tool "latex"
    1.33 +            ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))))
    1.34 +      | Dump_tex => ());
    1.35 +      (case opt_graphs of NONE => () | SOME (pdf, eps) =>
    1.36 +        (File.write (Path.append doc_dir graph_pdf_path) pdf;
    1.37 +          File.write (Path.append doc_dir graph_eps_path) eps));
    1.38 +      write_tex_index tex_index doc_dir;
    1.39 +      List.app (fn (a, {tex_source, ...}) => write_tex tex_source a doc_dir) thys);
    1.40 +
    1.41      val _ =
    1.42        if dump_prefix = "" then ()
    1.43        else