explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
authorwenzelm
Tue Aug 14 15:42:58 2012 +0200 (2012-08-14)
changeset 48805c3ea910b3581
parent 48804 6348e5fca42e
child 48806 559c1d80e129
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
doc-src/System/Thy/Sessions.thy
doc-src/System/Thy/document/Sessions.tex
etc/options
lib/Tools/mkroot
src/Pure/System/build.ML
src/Pure/System/session.ML
src/Pure/Thy/present.ML
     1.1 --- a/doc-src/System/Thy/Sessions.thy	Tue Aug 14 13:40:49 2012 +0200
     1.2 +++ b/doc-src/System/Thy/Sessions.thy	Tue Aug 14 15:42:58 2012 +0200
     1.3 @@ -356,19 +356,16 @@
     1.4  
     1.5  subsubsection {* Examples *}
     1.6  
     1.7 -text {* The following produces an example session as separate
     1.8 -  directory called @{verbatim Test}:
     1.9 +text {* Produce session @{verbatim Test} within a separate directory
    1.10 +  of the same name:
    1.11  \begin{ttbox}
    1.12 -isabelle mkroot Test && isabelle build -v -D Test
    1.13 +isabelle mkroot Test && isabelle build -D Test
    1.14  \end{ttbox}
    1.15  
    1.16 -  Option @{verbatim "-v"} is not required, but useful to reveal the
    1.17 -  the location of generated documents.
    1.18 -
    1.19 -  \medskip The subsequent example turns the current directory to a
    1.20 -  session directory with document and builds it:
    1.21 +  \medskip Upgrade the current directory into a session ROOT with
    1.22 +  document preparation, and build it:
    1.23  \begin{ttbox}
    1.24 -isabelle mkroot -d && isabelle build -D.
    1.25 +isabelle mkroot -d && isabelle build -D .
    1.26  \end{ttbox}
    1.27  *}
    1.28  
     2.1 --- a/doc-src/System/Thy/document/Sessions.tex	Tue Aug 14 13:40:49 2012 +0200
     2.2 +++ b/doc-src/System/Thy/document/Sessions.tex	Tue Aug 14 15:42:58 2012 +0200
     2.3 @@ -471,19 +471,16 @@
     2.4  \isamarkuptrue%
     2.5  %
     2.6  \begin{isamarkuptext}%
     2.7 -The following produces an example session as separate
     2.8 -  directory called \verb|Test|:
     2.9 +Produce session \verb|Test| within a separate directory
    2.10 +  of the same name:
    2.11  \begin{ttbox}
    2.12 -isabelle mkroot Test && isabelle build -v -D Test
    2.13 +isabelle mkroot Test && isabelle build -D Test
    2.14  \end{ttbox}
    2.15  
    2.16 -  Option \verb|-v| is not required, but useful to reveal the
    2.17 -  the location of generated documents.
    2.18 -
    2.19 -  \medskip The subsequent example turns the current directory to a
    2.20 -  session directory with document and builds it:
    2.21 +  \medskip Upgrade the current directory into a session ROOT with
    2.22 +  document preparation, and build it:
    2.23  \begin{ttbox}
    2.24 -isabelle mkroot -d && isabelle build -D.
    2.25 +isabelle mkroot -d && isabelle build -D .
    2.26  \end{ttbox}%
    2.27  \end{isamarkuptext}%
    2.28  \isamarkuptrue%
     3.1 --- a/etc/options	Tue Aug 14 13:40:49 2012 +0200
     3.2 +++ b/etc/options	Tue Aug 14 15:42:58 2012 +0200
     3.3 @@ -5,7 +5,9 @@
     3.4  
     3.5  option document : string = ""
     3.6    -- "build document in given format: pdf, dvi, dvi.gz, ps, ps.gz, or false"
     3.7 -option document_variants : string = "outline=/proof,/ML"
     3.8 +option document_output : string = ""
     3.9 +  -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
    3.10 +option document_variants : string = "document"
    3.11    -- "option alternative document variants (separated by colons)"
    3.12  option document_graph : bool = false
    3.13    -- "generate session graph image for document"
     4.1 --- a/lib/Tools/mkroot	Tue Aug 14 13:40:49 2012 +0200
     4.2 +++ b/lib/Tools/mkroot	Tue Aug 14 15:42:58 2012 +0200
     4.3 @@ -89,7 +89,7 @@
     4.4  if [ "$DOC" = true ]; then
     4.5    cat > "$DIR/ROOT" <<EOF
     4.6  session "$NAME" = "$ISABELLE_LOGIC" +
     4.7 -  options [document = $ISABELLE_DOC_FORMAT]
     4.8 +  options [document = $ISABELLE_DOC_FORMAT, document_output = "output"]
     4.9    theories [document = false]
    4.10      (* Foo Bar *)
    4.11    theories
    4.12 @@ -192,7 +192,7 @@
    4.13  
    4.14  Now use the following command line to build the session:
    4.15  
    4.16 -  isabelle build -v $OPT_DIR
    4.17 +  isabelle build $OPT_DIR
    4.18  
    4.19  EOF
    4.20  
     5.1 --- a/src/Pure/System/build.ML	Tue Aug 14 13:40:49 2012 +0200
     5.2 +++ b/src/Pure/System/build.ML	Tue Aug 14 15:42:58 2012 +0200
     5.3 @@ -68,10 +68,15 @@
     5.4        val document_variants =
     5.5          map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
     5.6        val _ =
     5.7 +        (case duplicates (op =) (map fst document_variants) of
     5.8 +          [] => ()
     5.9 +        | dups => error ("Duplicate document variants: " ^ commas_quote dups));
    5.10 +      val _ =
    5.11          Session.init do_output false
    5.12            (Options.bool options "browser_info") browser_info
    5.13            (Options.string options "document")
    5.14            (Options.bool options "document_graph")
    5.15 +          (Options.string options "document_output")
    5.16            document_variants
    5.17            parent_name name
    5.18            (Options.string options "document_dump",
     6.1 --- a/src/Pure/System/session.ML	Tue Aug 14 13:40:49 2012 +0200
     6.2 +++ b/src/Pure/System/session.ML	Tue Aug 14 15:42:58 2012 +0200
     6.3 @@ -10,7 +10,7 @@
     6.4    val name: unit -> string
     6.5    val welcome: unit -> string
     6.6    val finish: unit -> unit
     6.7 -  val init: bool -> bool -> bool -> string -> string -> bool -> (string * string) list ->
     6.8 +  val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
     6.9      string -> string -> string * Present.dump_mode -> string -> bool -> unit
    6.10    val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
    6.11    val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
    6.12 @@ -102,10 +102,11 @@
    6.13         remote_path := SOME (Url.explode rpath);
    6.14     (! remote_path, rpath <> ""));
    6.15  
    6.16 -fun init build reset info info_path doc doc_graph doc_variants parent name doc_dump rpath verbose =
    6.17 +fun init build reset info info_path doc doc_graph doc_output doc_variants
    6.18 +    parent name doc_dump rpath verbose =
    6.19   (init_name reset parent name;
    6.20 -  Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants
    6.21 -    (path ()) name doc_dump (get_rpath rpath) verbose
    6.22 +  Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output
    6.23 +    doc_variants (path ()) name doc_dump (get_rpath rpath) verbose
    6.24      (map Thy_Info.get_theory (Thy_Info.get_names ())));
    6.25  
    6.26  local
    6.27 @@ -122,7 +123,7 @@
    6.28      name dump rpath level timing verbose max_threads trace_threads
    6.29      parallel_proofs parallel_proofs_threshold =
    6.30    ((fn () =>
    6.31 -     (init build reset info info_path doc doc_graph (read_variants doc_variants) parent name
    6.32 +     (init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
    6.33          (doc_dump dump) rpath verbose;
    6.34        with_timing item timing use root;
    6.35        finish ()))
     7.1 --- a/src/Pure/Thy/present.ML	Tue Aug 14 13:40:49 2012 +0200
     7.2 +++ b/src/Pure/Thy/present.ML	Tue Aug 14 15:42:58 2012 +0200
     7.3 @@ -20,8 +20,8 @@
     7.4    datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty
     7.5    val dump_mode: string -> dump_mode
     7.6    val read_variant: string -> string * string
     7.7 -  val init: bool -> bool -> string -> string -> bool -> (string * string) list -> string list ->
     7.8 -    string -> string * dump_mode -> Url.T option * bool -> bool ->
     7.9 +  val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
    7.10 +    string list -> string -> string * dump_mode -> Url.T option * bool -> bool ->
    7.11      theory list -> unit  (*not thread-safe!*)
    7.12    val finish: unit -> unit  (*not thread-safe!*)
    7.13    val init_theory: string -> unit
    7.14 @@ -220,17 +220,17 @@
    7.15  
    7.16  type session_info =
    7.17    {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
    7.18 -    info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
    7.19 -    doc_dump: (string * dump_mode), remote_path: Url.T option, verbose: bool,
    7.20 -    readme: Path.T option};
    7.21 +    info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option,
    7.22 +    documents: (string * string) list, doc_dump: (string * dump_mode), remote_path: Url.T option,
    7.23 +    verbose: bool, readme: Path.T option};
    7.24  
    7.25  fun make_session_info
    7.26 -  (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents,
    7.27 -    doc_dump, remote_path, verbose, readme) =
    7.28 +  (name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_output,
    7.29 +    documents, doc_dump, remote_path, verbose, readme) =
    7.30    {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
    7.31 -    info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents,
    7.32 -    doc_dump = doc_dump, remote_path = remote_path, verbose = verbose,
    7.33 -    readme = readme}: session_info;
    7.34 +    info = info, doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
    7.35 +    documents = documents, doc_dump = doc_dump, remote_path = remote_path,
    7.36 +    verbose = verbose, readme = readme}: session_info;
    7.37  
    7.38  
    7.39  (* state *)
    7.40 @@ -280,7 +280,7 @@
    7.41  
    7.42  fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
    7.43  
    7.44 -fun init build info info_path doc doc_graph doc_variants path name
    7.45 +fun init build info info_path doc doc_graph document_output doc_variants path name
    7.46      (doc_dump as (dump_prefix, _)) (remote_path, first_time) verbose thys =
    7.47    if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
    7.48      (browser_info := empty_browser_info; session_info := NONE)
    7.49 @@ -290,6 +290,7 @@
    7.50        val session_name = name_of_session path;
    7.51        val sess_prefix = Path.make path;
    7.52        val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix;
    7.53 +      val doc_output = if document_output = "" then NONE else SOME (Path.explode document_output);
    7.54  
    7.55        val documents =
    7.56          if doc = "" then []
    7.57 @@ -315,8 +316,8 @@
    7.58          (Url.File index_path, session_name) docs (Url.explode "medium.html");
    7.59      in
    7.60        session_info :=
    7.61 -        SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
    7.62 -          info, doc, doc_graph, documents, doc_dump, remote_path, verbose, readme));
    7.63 +        SOME (make_session_info (name, parent_name, session_name, path, html_prefix, info, doc,
    7.64 +          doc_graph, doc_output, documents, doc_dump, remote_path, verbose, readme));
    7.65        browser_info := init_browser_info remote_path path thys;
    7.66        add_html_index (0, index_text)
    7.67      end;
    7.68 @@ -324,11 +325,11 @@
    7.69  
    7.70  (* isabelle tool wrappers *)
    7.71  
    7.72 -fun isabelle_document verbose format name tags path result_path =
    7.73 +fun isabelle_document {verbose, purge} format name tags dir =
    7.74    let
    7.75 -    val s = "\"$ISABELLE_TOOL\" document -c -o '" ^ format ^ "' \
    7.76 -      \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1";
    7.77 -    val doc_path = Path.append result_path (Path.ext format (Path.basic name));
    7.78 +    val s = "\"$ISABELLE_TOOL\" document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
    7.79 +      \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path dir ^ " 2>&1";
    7.80 +    val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
    7.81      val _ = if verbose then writeln s else ();
    7.82      val (out, rc) = Isabelle_System.bash_output s;
    7.83      val _ =
    7.84 @@ -366,8 +367,8 @@
    7.85  
    7.86  
    7.87  fun finish () =
    7.88 -  session_default () (fn {name, info, html_prefix, doc_format,
    7.89 -    doc_graph, documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} =>
    7.90 +  session_default () (fn {name, info, html_prefix, doc_format, doc_graph, doc_output,
    7.91 +    documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} =>
    7.92    let
    7.93      val {theories, files, tex_index, html_index, graph} = ! browser_info;
    7.94      val thys = Symtab.dest theories;
    7.95 @@ -430,11 +431,19 @@
    7.96      val doc_paths =
    7.97        documents |> Par_List.map (fn (name, tags) =>
    7.98          let
    7.99 -          val path = Path.append html_prefix (Path.basic name);
   7.100 -          val _ = prepare_sources path Dump_all;
   7.101 -        in isabelle_document true doc_format name tags path html_prefix end);
   7.102 +          val (doc_prefix, purge) =
   7.103 +            (case doc_output of
   7.104 +              SOME path => (path, false)
   7.105 +            | NONE => (html_prefix, true));
   7.106 +          val _ =
   7.107 +            File.eq (document_path, doc_prefix) andalso
   7.108 +              error ("Overlap of document input and output directory " ^ Path.print doc_prefix);
   7.109 +          val dir = Path.append doc_prefix (Path.basic name);
   7.110 +          val mode = if File.eq (document_path, dir) then Dump_tex_sty else Dump_all;
   7.111 +          val _ = prepare_sources dir mode;
   7.112 +        in isabelle_document {verbose = true, purge = purge} doc_format name tags dir end);
   7.113      val _ =
   7.114 -      if verbose then
   7.115 +      if verbose orelse is_some doc_output then
   7.116          doc_paths
   7.117          |> List.app (fn doc => Output.physical_stderr ("Document at " ^ show_path doc ^ "\n"))
   7.118        else ();
   7.119 @@ -540,7 +549,8 @@
   7.120        |> File.write (Path.append doc_path (tex_path name)));
   7.121      val _ = write_tex_index tex_index doc_path;
   7.122  
   7.123 -    val result = isabelle_document false doc_format documentN "" doc_path dir;
   7.124 +    val result =
   7.125 +      isabelle_document {verbose = false, purge = true} doc_format documentN "" doc_path;
   7.126      val result' = Isabelle_System.create_tmp_path documentN doc_format;
   7.127      val _ = File.copy result result';
   7.128    in result' end);