parallel preparation of document variants, within separate directories;
authorwenzelm
Sun Mar 20 20:05:43 2011 +0100 (2011-03-20)
changeset 42009b008525c4399
parent 42008 7423e833a880
child 42010 04f8c4851219
parallel preparation of document variants, within separate directories;
doc-src/System/Thy/Presentation.thy
doc-src/System/Thy/document/Presentation.tex
src/Pure/Thy/present.ML
     1.1 --- a/doc-src/System/Thy/Presentation.thy	Sun Mar 20 19:47:26 2011 +0100
     1.2 +++ b/doc-src/System/Thy/Presentation.thy	Sun Mar 20 20:05:43 2011 +0100
     1.3 @@ -682,15 +682,15 @@
     1.4    corresponding output files named after @{verbatim root} as well,
     1.5    e.g.\ @{verbatim root.dvi} for target format @{verbatim dvi}.
     1.6  
     1.7 -  \medskip When running the session, Isabelle copies the original
     1.8 -  @{verbatim document} directory into its proper place within
     1.9 -  @{setting ISABELLE_BROWSER_INFO} according to the session path.
    1.10 -  Then, for any processed theory @{text A} some {\LaTeX} source is
    1.11 -  generated and put there as @{text A}@{verbatim ".tex"}.
    1.12 -  Furthermore, a list of all generated theory files is put into
    1.13 -  @{verbatim session.tex}.  Typically, the root {\LaTeX} file provided
    1.14 -  by the user would include @{verbatim session.tex} to get a document
    1.15 -  containing all the theories.
    1.16 +  \medskip When running the session, Isabelle copies the content of
    1.17 +  the original @{verbatim document} directory into its proper place
    1.18 +  within @{setting ISABELLE_BROWSER_INFO}, according to the session
    1.19 +  path and document variant.  Then, for any processed theory @{text A}
    1.20 +  some {\LaTeX} source is generated and put there as @{text
    1.21 +  A}@{verbatim ".tex"}.  Furthermore, a list of all generated theory
    1.22 +  files is put into @{verbatim session.tex}.  Typically, the root
    1.23 +  {\LaTeX} file provided by the user would include @{verbatim
    1.24 +  session.tex} to get a document containing all the theories.
    1.25  
    1.26    The {\LaTeX} versions of the theories require some macros defined in
    1.27    @{file "~~/lib/texinputs/isabelle.sty"}.  Doing @{verbatim
     2.1 --- a/doc-src/System/Thy/document/Presentation.tex	Sun Mar 20 19:47:26 2011 +0100
     2.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Sun Mar 20 20:05:43 2011 +0100
     2.3 @@ -693,15 +693,13 @@
     2.4    corresponding output files named after \verb|root| as well,
     2.5    e.g.\ \verb|root.dvi| for target format \verb|dvi|.
     2.6  
     2.7 -  \medskip When running the session, Isabelle copies the original
     2.8 -  \verb|document| directory into its proper place within
     2.9 -  \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}} according to the session path.
    2.10 -  Then, for any processed theory \isa{A} some {\LaTeX} source is
    2.11 -  generated and put there as \isa{A}\verb|.tex|.
    2.12 -  Furthermore, a list of all generated theory files is put into
    2.13 -  \verb|session.tex|.  Typically, the root {\LaTeX} file provided
    2.14 -  by the user would include \verb|session.tex| to get a document
    2.15 -  containing all the theories.
    2.16 +  \medskip When running the session, Isabelle copies the content of
    2.17 +  the original \verb|document| directory into its proper place
    2.18 +  within \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}BROWSER{\isaliteral{5F}{\isacharunderscore}}INFO}}}}, according to the session
    2.19 +  path and document variant.  Then, for any processed theory \isa{A}
    2.20 +  some {\LaTeX} source is generated and put there as \isa{A}\verb|.tex|.  Furthermore, a list of all generated theory
    2.21 +  files is put into \verb|session.tex|.  Typically, the root
    2.22 +  {\LaTeX} file provided by the user would include \verb|session.tex| to get a document containing all the theories.
    2.23  
    2.24    The {\LaTeX} versions of the theories require some macros defined in
    2.25    \verb|~~/lib/texinputs/isabelle.sty|.  Doing \verb|\usepackage{isabelle}| in \verb|root.tex| should be fine;
     3.1 --- a/src/Pure/Thy/present.ML	Sun Mar 20 19:47:26 2011 +0100
     3.2 +++ b/src/Pure/Thy/present.ML	Sun Mar 20 20:05:43 2011 +0100
     3.3 @@ -420,9 +420,9 @@
     3.4          else ()));
     3.5  
     3.6      val doc_paths =
     3.7 -      documents |> map (fn (name, tags) =>
     3.8 +      documents |> Par_List.map (fn (name, tags) =>
     3.9          let
    3.10 -          val path = Path.append html_prefix document_path;
    3.11 +          val path = Path.append html_prefix (Path.basic name);
    3.12            val _ = prepare_sources true path;
    3.13          in isabelle_document true doc_format name tags path html_prefix end);
    3.14      val _ =