# HG changeset patch
# User wenzelm
# Date 1300647943 -3600
# Node ID b008525c43995e42b1439683df908751b5523d8b
# Parent  7423e833a88099374eca943f2918464dd57fd73d
parallel preparation of document variants, within separate directories;

diff -r 7423e833a880 -r b008525c4399 doc-src/System/Thy/Presentation.thy
--- a/doc-src/System/Thy/Presentation.thy	Sun Mar 20 19:47:26 2011 +0100
+++ b/doc-src/System/Thy/Presentation.thy	Sun Mar 20 20:05:43 2011 +0100
@@ -682,15 +682,15 @@
   corresponding output files named after @{verbatim root} as well,
   e.g.\ @{verbatim root.dvi} for target format @{verbatim dvi}.
 
-  \medskip When running the session, Isabelle copies the original
-  @{verbatim document} directory into its proper place within
-  @{setting ISABELLE_BROWSER_INFO} according to the session path.
-  Then, for any processed theory @{text A} some {\LaTeX} source is
-  generated and put there as @{text A}@{verbatim ".tex"}.
-  Furthermore, a list of all generated theory files is put into
-  @{verbatim session.tex}.  Typically, the root {\LaTeX} file provided
-  by the user would include @{verbatim session.tex} to get a document
-  containing all the theories.
+  \medskip When running the session, Isabelle copies the content of
+  the original @{verbatim document} directory into its proper place
+  within @{setting ISABELLE_BROWSER_INFO}, according to the session
+  path and document variant.  Then, for any processed theory @{text A}
+  some {\LaTeX} source is generated and put there as @{text
+  A}@{verbatim ".tex"}.  Furthermore, a list of all generated theory
+  files is put into @{verbatim session.tex}.  Typically, the root
+  {\LaTeX} file provided by the user would include @{verbatim
+  session.tex} to get a document containing all the theories.
 
   The {\LaTeX} versions of the theories require some macros defined in
   @{file "~~/lib/texinputs/isabelle.sty"}.  Doing @{verbatim
diff -r 7423e833a880 -r b008525c4399 doc-src/System/Thy/document/Presentation.tex
--- a/doc-src/System/Thy/document/Presentation.tex	Sun Mar 20 19:47:26 2011 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex	Sun Mar 20 20:05:43 2011 +0100
@@ -693,15 +693,13 @@
   corresponding output files named after \verb|root| as well,
   e.g.\ \verb|root.dvi| for target format \verb|dvi|.
 
-  \medskip When running the session, Isabelle copies the original
-  \verb|document| directory into its proper place within
-  \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}} according to the session path.
-  Then, for any processed theory \isa{A} some {\LaTeX} source is
-  generated and put there as \isa{A}\verb|.tex|.
-  Furthermore, a list of all generated theory files is put into
-  \verb|session.tex|.  Typically, the root {\LaTeX} file provided
-  by the user would include \verb|session.tex| to get a document
-  containing all the theories.
+  \medskip When running the session, Isabelle copies the content of
+  the original \verb|document| directory into its proper place
+  within \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}, according to the session
+  path and document variant.  Then, for any processed theory \isa{A}
+  some {\LaTeX} source is generated and put there as \isa{A}\verb|.tex|.  Furthermore, a list of all generated theory
+  files is put into \verb|session.tex|.  Typically, the root
+  {\LaTeX} file provided by the user would include \verb|session.tex| to get a document containing all the theories.
 
   The {\LaTeX} versions of the theories require some macros defined in
   \verb|~~/lib/texinputs/isabelle.sty|.  Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
diff -r 7423e833a880 -r b008525c4399 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun Mar 20 19:47:26 2011 +0100
+++ b/src/Pure/Thy/present.ML	Sun Mar 20 20:05:43 2011 +0100
@@ -420,9 +420,9 @@
         else ()));
 
     val doc_paths =
-      documents |> map (fn (name, tags) =>
+      documents |> Par_List.map (fn (name, tags) =>
         let
-          val path = Path.append html_prefix document_path;
+          val path = Path.append html_prefix (Path.basic name);
           val _ = prepare_sources true path;
         in isabelle_document true doc_format name tags path html_prefix end);
     val _ =