doc-src/System/Thy/Sessions.thy
changeset 48805 c3ea910b3581
parent 48739 3a6c03b15916
child 48814 d488a5f25bf6
     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