src/Doc/System/Sessions.thy

 imports Base
 begin
 
 chapter \<open>Isabelle sessions and build management \label{ch:session}\<close>
 
-text \<open>An Isabelle \emph{session} consists of a collection of related
+text \<open>An Isabelle \<^emph>\<open>session\<close> consists of a collection of related
   theories that may be associated with formal documents
-  (\chref{ch:present}).  There is also a notion of \emph{persistent
-  heap} image to capture the state of a session, similar to
+  (\chref{ch:present}).  There is also a notion of \<^emph>\<open>persistent
+  heap\<close> image to capture the state of a session, similar to
   object-code in compiled programming languages.  Thus the concept of
   session resembles that of a ``project'' in common IDE environments,
   but the specific name emphasizes the connection to interactive
   theorem proving: the session wraps-up the results of
   user-interaction with the prover in a persistent form.

   within certain directories, such as the home locations of registered
   Isabelle components or additional project directories given by the
   user.
 
   The ROOT file format follows the lexical conventions of the
-  \emph{outer syntax} of Isabelle/Isar, see also
+  \<^emph>\<open>outer syntax\<close> of Isabelle/Isar, see also
   @{cite "isabelle-isar-ref"}.  This defines common forms like
   identifiers, names, quoted strings, verbatim text, nested comments
   etc.  The grammar for @{syntax session_chapter} and @{syntax
   session_entry} is given as syntax diagram below; each ROOT file may
   contain multiple specifications like this.  Chapters help to

   \<^descr> \isakeyword{description}~@{text "text"} is a free-form
   annotation for this session.
 
   \<^descr> \isakeyword{options}~@{text "[x = a, y = b, z]"} defines
   separate options (\secref{sec:system-options}) that are used when
-  processing this session, but \emph{without} propagation to child
+  processing this session, but \<^emph>\<open>without\<close> propagation to child
   sessions.  Note that @{text "z"} abbreviates @{text "z = true"} for
   Boolean options.
 
   \<^descr> \isakeyword{theories}~@{text "options names"} specifies a
   block of theories that are processed within an environment that is

   parallel build jobs (prover processes).  Each prover process is
   subject to a separate limit of parallel worker threads, cf.\ system
   option @{system_option_ref threads}.
 
   \<^medskip>
-  Option @{verbatim "-s"} enables \emph{system mode}, which
+  Option @{verbatim "-s"} enables \<^emph>\<open>system mode\<close>, which
   means that resulting heap images and log files are stored in
   @{file_unchecked "$ISABELLE_HOME/heaps"} instead of the default location
   @{setting ISABELLE_OUTPUT} (which is normally in @{setting
   ISABELLE_HOME_USER}, i.e.\ the user's home directory).