1.1 --- a/doc-src/System/Thy/Sessions.thy	Sat Jul 28 19:49:09 2012 +0200
     1.2 +++ b/doc-src/System/Thy/Sessions.thy	Sat Jul 28 20:07:21 2012 +0200
     1.3 @@ -2,9 +2,30 @@
     1.4  imports Base
     1.5  begin
     1.6  
     1.7 -chapter {* Isabelle sessions and build management *}
     1.8 +chapter {* Isabelle sessions and build management \label{ch:session} *}
     1.9  
    1.10 -text {* FIXME *}
    1.11 +text {* An Isabelle \emph{session} consists of a collection of related
    1.12 +  theories that are associated with an optional formal document (see
    1.13 +  also \chref{ch:present}).  There is also a notion of persistent
    1.14 +  \emph{heap image} to capture the state of a session, similar to
    1.15 +  object-code in compiled programming languages.
    1.16 +
    1.17 +  Thus the concept of session resembles that of a ``project'' in
    1.18 +  common IDE environments, but our specific name emphasizes the
    1.19 +  connection to interactive theorem proving: the session wraps-up the
    1.20 +  results of user-interaction with the prover in a persistent form.
    1.21 +
    1.22 +  \medskip Application sessions are built on a given parent session.
    1.23 +  The resulting hierarchy eventually leads to some major object-logic
    1.24 +  session, notably @{text "HOL"}, which itself is based on @{text
    1.25 +  "Pure"} as the common root.
    1.26 +
    1.27 +  Processing sessions may take considerable time.  The tools for
    1.28 +  Isabelle build management help to organize this efficiently,
    1.29 +  including support for parallel build jobs --- in addition to the
    1.30 +  multithreaded theory and proof checking that is already provided by
    1.31 +  the prover process.
    1.32 +*}
    1.33  
    1.34  section {* Session ROOT specifications \label{sec:session-root} *}
    1.35  

     2.1 --- a/doc-src/System/Thy/document/Sessions.tex	Sat Jul 28 19:49:09 2012 +0200
     2.2 +++ b/doc-src/System/Thy/document/Sessions.tex	Sat Jul 28 20:07:21 2012 +0200
     2.3 @@ -18,12 +18,31 @@
     2.4  %
     2.5  \endisadelimtheory
     2.6  %
     2.7 -\isamarkupchapter{Isabelle sessions and build management%
     2.8 +\isamarkupchapter{Isabelle sessions and build management \label{ch:session}%
     2.9  }
    2.10  \isamarkuptrue%
    2.11  %
    2.12  \begin{isamarkuptext}%
    2.13 -FIXME%
    2.14 +An Isabelle \emph{session} consists of a collection of related
    2.15 +  theories that are associated with an optional formal document (see
    2.16 +  also \chref{ch:present}).  There is also a notion of persistent
    2.17 +  \emph{heap image} to capture the state of a session, similar to
    2.18 +  object-code in compiled programming languages.
    2.19 +
    2.20 +  Thus the concept of session resembles that of a ``project'' in
    2.21 +  common IDE environments, but our specific name emphasizes the
    2.22 +  connection to interactive theorem proving: the session wraps-up the
    2.23 +  results of user-interaction with the prover in a persistent form.
    2.24 +
    2.25 +  \medskip Application sessions are built on a given parent session.
    2.26 +  The resulting hierarchy eventually leads to some major object-logic
    2.27 +  session, notably \isa{{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{22}{\isachardoublequote}}}, which itself is based on \isa{{\isaliteral{22}{\isachardoublequote}}Pure{\isaliteral{22}{\isachardoublequote}}} as the common root.
    2.28 +
    2.29 +  Processing sessions may take considerable time.  The tools for
    2.30 +  Isabelle build management help to organize this efficiently,
    2.31 +  including support for parallel build jobs --- in addition to the
    2.32 +  multithreaded theory and proof checking that is already provided by
    2.33 +  the prover process.%
    2.34  \end{isamarkuptext}%
    2.35  \isamarkuptrue%
    2.36  %