--- a/src/Doc/System/Presentation.thy Mon Oct 12 17:10:36 2015 +0200
+++ b/src/Doc/System/Presentation.thy Mon Oct 12 17:11:17 2015 +0200
@@ -71,8 +71,7 @@
such as generating Postscript files, which are not available in the
applet version. See \secref{sec:browse} for further information.
- \medskip
-
+ \<^medskip>
The easiest way to let Isabelle generate theory browsing information
for existing sessions is to invoke @{tool build} with suitable
options:
@@ -98,13 +97,15 @@
information as well, see \secref{sec:tool-document} for further
details.
- \bigskip The theory browsing information is stored in a
+ \<^bigskip>
+ The theory browsing information is stored in a
sub-directory directory determined by the @{setting_ref
ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the
session chapter and identifier. In order to present Isabelle
applications on the web, the corresponding subdirectory from
@{setting ISABELLE_BROWSER_INFO} can be put on a WWW server.\<close>
+
section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close>
text \<open>The @{tool_def mkroot} tool configures a given directory as
@@ -126,7 +127,8 @@
files or directories. Earlier attempts to generate a session root
need to be deleted manually.
- \medskip Option @{verbatim "-d"} indicates that the session shall be
+ \<^medskip>
+ Option @{verbatim "-d"} indicates that the session shall be
accompanied by a formal document, with @{text DIR}@{verbatim
"/document/root.tex"} as its {\LaTeX} entry point (see also
\chref{ch:present}).
@@ -134,7 +136,8 @@
Option @{verbatim "-n"} allows to specify an alternative session
name; otherwise the base name of the given directory is used.
- \medskip The implicit Isabelle settings variable @{setting
+ \<^medskip>
+ The implicit Isabelle settings variable @{setting
ISABELLE_LOGIC} specifies the parent session, and @{setting
ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled
into the generated @{verbatim ROOT} file.\<close>
@@ -148,7 +151,8 @@
isabelle mkroot -d Test && isabelle build -D Test
\end{ttbox}
- \medskip Upgrade the current directory into a session ROOT with
+ \<^medskip>
+ Upgrade the current directory into a session ROOT with
document preparation, and build it:
\begin{ttbox}
isabelle mkroot -d && isabelle build -D .
@@ -180,17 +184,20 @@
information document output as well, e.g.\ in case of errors
encountered in the batch run.
- \medskip The @{verbatim "-c"} option tells @{tool document} to
+ \<^medskip>
+ The @{verbatim "-c"} option tells @{tool document} to
dispose the document sources after successful operation! This is
the right thing to do for sources generated by an Isabelle process,
but take care of your files in manual document preparation!
- \medskip The @{verbatim "-n"} and @{verbatim "-o"} option specify
+ \<^medskip>
+ The @{verbatim "-n"} and @{verbatim "-o"} option specify
the final output file name and format, the default is ``@{verbatim
document.dvi}''. Note that the result will appear in the parent of
the target @{verbatim DIR}.
- \medskip The @{verbatim "-t"} option tells {\LaTeX} how to interpret
+ \<^medskip>
+ The @{verbatim "-t"} option tells {\LaTeX} how to interpret
tagged Isabelle command regions. Tags are specified as a comma
separated list of modifier/name pairs: ``@{verbatim "+"}@{text
foo}'' (or just ``@{text foo}'') means to keep, ``@{verbatim
@@ -202,12 +209,14 @@
@{verbatim "\\isafoldtag"}, in @{file
"~~/lib/texinputs/isabelle.sty"}.
- \medskip Document preparation requires a @{verbatim document}
+ \<^medskip>
+ Document preparation requires a @{verbatim document}
directory within the session sources. This directory is supposed to
contain all the files needed to produce the final document --- apart
from the actual theories which are generated by Isabelle.
- \medskip For most practical purposes, @{tool document} is smart
+ \<^medskip>
+ For most practical purposes, @{tool document} is smart
enough to create any of the specified output formats, taking
@{verbatim root.tex} supplied by the user as a starting point. This
even includes multiple runs of {\LaTeX} to accommodate references
@@ -223,7 +232,8 @@
but it is also possible to harvest generated {\LaTeX} sources and
copy them elsewhere.
- \medskip When running the session, Isabelle copies the content of
+ \<^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}
@@ -254,7 +264,8 @@
bookmarks), we recommend to include @{file
"~~/lib/texinputs/pdfsetup.sty"} as well.
- \medskip As a final step of Isabelle document preparation, @{tool
+ \<^medskip>
+ As a final step of Isabelle document preparation, @{tool
document}~@{verbatim "-c"} is run on the resulting copy of the
@{verbatim document} directory. Thus the actual output document is
built and installed in its proper place. The generated sources are