--- 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
--- 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;
--- 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 _ =