1.1 --- a/src/Pure/Thy/present.ML Thu Jul 26 14:24:27 2012 +0200
1.2 +++ b/src/Pure/Thy/present.ML Thu Jul 26 14:29:54 2012 +0200
1.3 @@ -18,7 +18,7 @@
1.4 val display_graph: {name: string, ID: string, dir: string, unfold: bool,
1.5 path: string, parents: string list} list -> unit
1.6 val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
1.7 - string -> (bool * Path.T) option -> Url.T option * bool -> bool ->
1.8 + string -> string * string -> Url.T option * bool -> bool ->
1.9 theory list -> unit (*not thread-safe!*)
1.10 val finish: unit -> unit (*not thread-safe!*)
1.11 val init_theory: string -> unit
1.12 @@ -210,15 +210,15 @@
1.13 type session_info =
1.14 {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
1.15 info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
1.16 - dump_prefix: (bool * Path.T) option, remote_path: Url.T option, verbose: bool,
1.17 + doc_dump: (string * string), remote_path: Url.T option, verbose: bool,
1.18 readme: Path.T option};
1.19
1.20 fun make_session_info
1.21 (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents,
1.22 - dump_prefix, remote_path, verbose, readme) =
1.23 + doc_dump, remote_path, verbose, readme) =
1.24 {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
1.25 info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents,
1.26 - dump_prefix = dump_prefix, remote_path = remote_path, verbose = verbose,
1.27 + doc_dump = doc_dump, remote_path = remote_path, verbose = verbose,
1.28 readme = readme}: session_info;
1.29
1.30
1.31 @@ -273,9 +273,9 @@
1.32
1.33 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
1.34
1.35 -fun init build info info_path doc doc_graph doc_variants path name dump_prefix
1.36 - (remote_path, first_time) verbose thys =
1.37 - if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
1.38 +fun init build info info_path doc doc_graph doc_variants path name
1.39 + (doc_dump as (dump_prefix, _)) (remote_path, first_time) verbose thys =
1.40 + if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
1.41 (browser_info := empty_browser_info; session_info := NONE)
1.42 else
1.43 let
1.44 @@ -309,7 +309,7 @@
1.45 in
1.46 session_info :=
1.47 SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
1.48 - info, doc, doc_graph, documents, dump_prefix, remote_path, verbose, readme));
1.49 + info, doc, doc_graph, documents, doc_dump, remote_path, verbose, readme));
1.50 browser_info := init_browser_info remote_path path thys;
1.51 add_html_index (0, index_text)
1.52 end;
1.53 @@ -360,32 +360,34 @@
1.54
1.55 fun finish () =
1.56 session_default () (fn {name, info, html_prefix, doc_format,
1.57 - doc_graph, documents, dump_prefix, path, verbose, readme, ...} =>
1.58 + doc_graph, documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} =>
1.59 let
1.60 val {theories, files, tex_index, html_index, graph} = ! browser_info;
1.61 val thys = Symtab.dest theories;
1.62 val parent_html_prefix = Path.append html_prefix Path.parent;
1.63
1.64 - fun finish_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path;
1.65 fun finish_html (a, {html, ...}: theory_info) =
1.66 File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
1.67
1.68 val sorted_graph = sorted_index graph;
1.69 val opt_graphs =
1.70 - if doc_graph andalso (not (null documents) orelse is_some dump_prefix) then
1.71 + if doc_graph andalso (not (null documents) orelse dump_prefix <> "") then
1.72 SOME (isabelle_browser sorted_graph)
1.73 else NONE;
1.74
1.75 - fun prepare_sources cp path =
1.76 - (Isabelle_System.mkdirs path;
1.77 - if cp then Isabelle_System.copy_dir document_path path else ();
1.78 - Isabelle_System.isabelle_tool "latex"
1.79 - ("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
1.80 + fun prepare_sources doc_dir doc_mode =
1.81 + (Isabelle_System.mkdirs doc_dir;
1.82 + if doc_mode = "all" then Isabelle_System.copy_dir document_path doc_dir
1.83 + else if doc_mode = "tex+sty" then
1.84 + ignore (Isabelle_System.isabelle_tool "latex"
1.85 + ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))))
1.86 + else if doc_mode = "tex" then ()
1.87 + else error ("Illegal document dump mode: " ^ quote doc_mode);
1.88 (case opt_graphs of NONE => () | SOME (pdf, eps) =>
1.89 - (File.write (Path.append path graph_pdf_path) pdf;
1.90 - File.write (Path.append path graph_eps_path) eps));
1.91 - write_tex_index tex_index path;
1.92 - List.app (finish_tex path) thys);
1.93 + (File.write (Path.append doc_dir graph_pdf_path) pdf;
1.94 + File.write (Path.append doc_dir graph_eps_path) eps));
1.95 + write_tex_index tex_index doc_dir;
1.96 + List.app (fn (a, {tex_source, ...}) => write_tex tex_source a doc_dir) thys);
1.97 val _ =
1.98 if info then
1.99 (Isabelle_System.mkdirs (Path.append html_prefix session_path);
1.100 @@ -407,16 +409,22 @@
1.101 else ();
1.102
1.103 val _ =
1.104 - (case dump_prefix of NONE => () | SOME (cp, path) =>
1.105 - (prepare_sources cp path;
1.106 - if verbose then Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
1.107 - else ()));
1.108 + if dump_prefix = "" then ()
1.109 + else
1.110 + let
1.111 + val path = Path.explode dump_prefix;
1.112 + val _ = prepare_sources path dump_mode;
1.113 + in
1.114 + if verbose then
1.115 + Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
1.116 + else ()
1.117 + end;
1.118
1.119 val doc_paths =
1.120 documents |> Par_List.map (fn (name, tags) =>
1.121 let
1.122 val path = Path.append html_prefix (Path.basic name);
1.123 - val _ = prepare_sources true path;
1.124 + val _ = prepare_sources path "all";
1.125 in isabelle_document true doc_format name tags path html_prefix end);
1.126 val _ =
1.127 if verbose then