src/Doc/System/Sessions.thy
changeset 68734 c14a2cc9b5ef
parent 68523 ccacc84e0251
child 68808 5467858e9419
     1.1 --- a/src/Doc/System/Sessions.thy	Wed Aug 01 19:48:58 2018 +0200
     1.2 +++ b/src/Doc/System/Sessions.thy	Wed Aug 01 20:58:41 2018 +0200
     1.3 @@ -333,14 +333,14 @@
     1.4    completed by including all ancestors.
     1.5  
     1.6    \<^medskip>
     1.7 -  One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions. All descendants
     1.8 -  are included.
     1.9 +  One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions to be included (all
    1.10 +  descendants wrt.\ the session parent or import graph).
    1.11  
    1.12    \<^medskip>
    1.13 -  One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded. All
    1.14 -  descendents of excluded sessions are removed from the selection as specified
    1.15 -  above. Option \<^verbatim>\<open>-X\<close> is analogous to this, but excluded sessions are
    1.16 -  specified by session group membership.
    1.17 +  One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded (all
    1.18 +  descendants wrt.\ the session parent or import graph). Option \<^verbatim>\<open>-X\<close> is
    1.19 +  analogous to this, but excluded sessions are specified by session group
    1.20 +  membership.
    1.21  
    1.22    \<^medskip>
    1.23    Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense that it refers to its
    1.24 @@ -373,8 +373,8 @@
    1.25    of sessions, as required for other sessions to continue later on.
    1.26  
    1.27    \<^medskip>
    1.28 -  Option \<^verbatim>\<open>-c\<close> cleans all descendants of the selected sessions before
    1.29 -  performing the specified build operation.
    1.30 +  Option \<^verbatim>\<open>-c\<close> cleans the selected sessions (all descendants wrt.\ the session
    1.31 +  parent or import graph) before performing the specified build operation.
    1.32  
    1.33    \<^medskip>
    1.34    Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their