# HG changeset patch # User wenzelm # Date 1344951778 -7200 # Node ID c3ea910b3581111b2e2c6ad52080e3d62dd55c9b # Parent 6348e5fca42e89d3a8dc7454472303a16c0a5378 explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO; diff -r 6348e5fca42e -r c3ea910b3581 doc-src/System/Thy/Sessions.thy --- a/doc-src/System/Thy/Sessions.thy Tue Aug 14 13:40:49 2012 +0200 +++ b/doc-src/System/Thy/Sessions.thy Tue Aug 14 15:42:58 2012 +0200 @@ -356,19 +356,16 @@ subsubsection {* Examples *} -text {* The following produces an example session as separate - directory called @{verbatim Test}: +text {* Produce session @{verbatim Test} within a separate directory + of the same name: \begin{ttbox} -isabelle mkroot Test && isabelle build -v -D Test +isabelle mkroot Test && isabelle build -D Test \end{ttbox} - Option @{verbatim "-v"} is not required, but useful to reveal the - the location of generated documents. - - \medskip The subsequent example turns the current directory to a - session directory with document and builds it: + \medskip Upgrade the current directory into a session ROOT with + document preparation, and build it: \begin{ttbox} -isabelle mkroot -d && isabelle build -D. +isabelle mkroot -d && isabelle build -D . \end{ttbox} *} diff -r 6348e5fca42e -r c3ea910b3581 doc-src/System/Thy/document/Sessions.tex --- a/doc-src/System/Thy/document/Sessions.tex Tue Aug 14 13:40:49 2012 +0200 +++ b/doc-src/System/Thy/document/Sessions.tex Tue Aug 14 15:42:58 2012 +0200 @@ -471,19 +471,16 @@ \isamarkuptrue% % \begin{isamarkuptext}% -The following produces an example session as separate - directory called \verb|Test|: +Produce session \verb|Test| within a separate directory + of the same name: \begin{ttbox} -isabelle mkroot Test && isabelle build -v -D Test +isabelle mkroot Test && isabelle build -D Test \end{ttbox} - Option \verb|-v| is not required, but useful to reveal the - the location of generated documents. - - \medskip The subsequent example turns the current directory to a - session directory with document and builds it: + \medskip Upgrade the current directory into a session ROOT with + document preparation, and build it: \begin{ttbox} -isabelle mkroot -d && isabelle build -D. +isabelle mkroot -d && isabelle build -D . \end{ttbox}% \end{isamarkuptext}% \isamarkuptrue% diff -r 6348e5fca42e -r c3ea910b3581 etc/options --- a/etc/options Tue Aug 14 13:40:49 2012 +0200 +++ b/etc/options Tue Aug 14 15:42:58 2012 +0200 @@ -5,7 +5,9 @@ option document : string = "" -- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false" -option document_variants : string = "outline=/proof,/ML" +option document_output : string = "" + -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)" +option document_variants : string = "document" -- "option alternative document variants (separated by colons)" option document_graph : bool = false -- "generate session graph image for document" diff -r 6348e5fca42e -r c3ea910b3581 lib/Tools/mkroot --- a/lib/Tools/mkroot Tue Aug 14 13:40:49 2012 +0200 +++ b/lib/Tools/mkroot Tue Aug 14 15:42:58 2012 +0200 @@ -89,7 +89,7 @@ if [ "$DOC" = true ]; then cat > "$DIR/ROOT" < () + | dups => error ("Duplicate document variants: " ^ commas_quote dups)); + val _ = Session.init do_output false (Options.bool options "browser_info") browser_info (Options.string options "document") (Options.bool options "document_graph") + (Options.string options "document_output") document_variants parent_name name (Options.string options "document_dump", diff -r 6348e5fca42e -r c3ea910b3581 src/Pure/System/session.ML --- a/src/Pure/System/session.ML Tue Aug 14 13:40:49 2012 +0200 +++ b/src/Pure/System/session.ML Tue Aug 14 15:42:58 2012 +0200 @@ -10,7 +10,7 @@ val name: unit -> string val welcome: unit -> string val finish: unit -> unit - val init: bool -> bool -> bool -> string -> string -> bool -> (string * string) list -> + val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list -> string -> string -> string * Present.dump_mode -> string -> bool -> unit val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b val use_dir: string -> string -> bool -> string list -> bool -> bool -> string -> @@ -102,10 +102,11 @@ remote_path := SOME (Url.explode rpath); (! remote_path, rpath <> "")); -fun init build reset info info_path doc doc_graph doc_variants parent name doc_dump rpath verbose = +fun init build reset info info_path doc doc_graph doc_output doc_variants + parent name doc_dump rpath verbose = (init_name reset parent name; - Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants - (path ()) name doc_dump (get_rpath rpath) verbose + Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output + doc_variants (path ()) name doc_dump (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))); local @@ -122,7 +123,7 @@ name dump rpath level timing verbose max_threads trace_threads parallel_proofs parallel_proofs_threshold = ((fn () => - (init build reset info info_path doc doc_graph (read_variants doc_variants) parent name + (init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name (doc_dump dump) rpath verbose; with_timing item timing use root; finish ())) diff -r 6348e5fca42e -r c3ea910b3581 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Tue Aug 14 13:40:49 2012 +0200 +++ b/src/Pure/Thy/present.ML Tue Aug 14 15:42:58 2012 +0200 @@ -20,8 +20,8 @@ datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty val dump_mode: string -> dump_mode val read_variant: string -> string * string - val init: bool -> bool -> string -> string -> bool -> (string * string) list -> string list -> - string -> string * dump_mode -> Url.T option * bool -> bool -> + val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list -> + string list -> string -> string * dump_mode -> Url.T option * bool -> bool -> theory list -> unit (*not thread-safe!*) val finish: unit -> unit (*not thread-safe!*) val init_theory: string -> unit @@ -220,17 +220,17 @@ type session_info = {name: string, parent: string, session: string, path: string list, html_prefix: Path.T, - info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list, - doc_dump: (string * dump_mode), remote_path: Url.T option, verbose: bool, - readme: Path.T option}; + info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option, + documents: (string * string) list, doc_dump: (string * dump_mode), remote_path: Url.T option, + verbose: bool, readme: Path.T option}; fun make_session_info - (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents, - doc_dump, remote_path, verbose, readme) = + (name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_output, + documents, doc_dump, remote_path, verbose, readme) = {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix, - info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents, - doc_dump = doc_dump, remote_path = remote_path, verbose = verbose, - readme = readme}: session_info; + info = info, doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output, + documents = documents, doc_dump = doc_dump, remote_path = remote_path, + verbose = verbose, readme = readme}: session_info; (* state *) @@ -280,7 +280,7 @@ fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); -fun init build info info_path doc doc_graph doc_variants path name +fun init build info info_path doc doc_graph document_output doc_variants path name (doc_dump as (dump_prefix, _)) (remote_path, first_time) verbose thys = if not build andalso not info andalso doc = "" andalso dump_prefix = "" then (browser_info := empty_browser_info; session_info := NONE) @@ -290,6 +290,7 @@ val session_name = name_of_session path; val sess_prefix = Path.make path; val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix; + val doc_output = if document_output = "" then NONE else SOME (Path.explode document_output); val documents = if doc = "" then [] @@ -315,8 +316,8 @@ (Url.File index_path, session_name) docs (Url.explode "medium.html"); in session_info := - SOME (make_session_info (name, parent_name, session_name, path, html_prefix, - info, doc, doc_graph, documents, doc_dump, remote_path, verbose, readme)); + SOME (make_session_info (name, parent_name, session_name, path, html_prefix, info, doc, + doc_graph, doc_output, documents, doc_dump, remote_path, verbose, readme)); browser_info := init_browser_info remote_path path thys; add_html_index (0, index_text) end; @@ -324,11 +325,11 @@ (* isabelle tool wrappers *) -fun isabelle_document verbose format name tags path result_path = +fun isabelle_document {verbose, purge} format name tags dir = let - val s = "\"$ISABELLE_TOOL\" document -c -o '" ^ format ^ "' \ - \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1"; - val doc_path = Path.append result_path (Path.ext format (Path.basic name)); + val s = "\"$ISABELLE_TOOL\" document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \ + \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path dir ^ " 2>&1"; + val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format]; val _ = if verbose then writeln s else (); val (out, rc) = Isabelle_System.bash_output s; val _ = @@ -366,8 +367,8 @@ fun finish () = - session_default () (fn {name, info, html_prefix, doc_format, - doc_graph, documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} => + session_default () (fn {name, info, html_prefix, doc_format, doc_graph, doc_output, + documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} => let val {theories, files, tex_index, html_index, graph} = ! browser_info; val thys = Symtab.dest theories; @@ -430,11 +431,19 @@ val doc_paths = documents |> Par_List.map (fn (name, tags) => let - val path = Path.append html_prefix (Path.basic name); - val _ = prepare_sources path Dump_all; - in isabelle_document true doc_format name tags path html_prefix end); + val (doc_prefix, purge) = + (case doc_output of + SOME path => (path, false) + | NONE => (html_prefix, true)); + val _ = + File.eq (document_path, doc_prefix) andalso + error ("Overlap of document input and output directory " ^ Path.print doc_prefix); + val dir = Path.append doc_prefix (Path.basic name); + val mode = if File.eq (document_path, dir) then Dump_tex_sty else Dump_all; + val _ = prepare_sources dir mode; + in isabelle_document {verbose = true, purge = purge} doc_format name tags dir end); val _ = - if verbose then + if verbose orelse is_some doc_output then doc_paths |> List.app (fn doc => Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")) else (); @@ -540,7 +549,8 @@ |> File.write (Path.append doc_path (tex_path name))); val _ = write_tex_index tex_index doc_path; - val result = isabelle_document false doc_format documentN "" doc_path dir; + val result = + isabelle_document {verbose = false, purge = true} doc_format documentN "" doc_path; val result' = Isabelle_System.create_tmp_path documentN doc_format; val _ = File.copy result result'; in result' end);