diff -r fd6dc1a4b9ca -r 1cbac4ae934d src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Wed Nov 18 13:14:01 2020 +0100 +++ b/src/Doc/System/Sessions.thy Wed Nov 18 13:16:08 2020 +0100 @@ -317,6 +317,7 @@ -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -N cyclic shuffling of NUMA CPU nodes (performance tuning) + -P DIR enable HTML/PDF presentation in directory (":" for default) -R refer to requirements of selected sessions -S soft build: only observe changes of sources, not heap images -X NAME exclude sessions from group NAME and all descendants @@ -402,6 +403,11 @@ the command-line are applied in the given order. \<^medskip> + Option \<^verbatim>\-P\ enables PDF/HTML presentation in the given directory, where + ``\<^verbatim>\-P:\'' refers to the default @{setting_ref ISABELLE_BROWSER_INFO} (or + @{setting_ref ISABELLE_BROWSER_INFO_SYSTEM}). + + \<^medskip> Option \<^verbatim>\-b\ ensures that heap images are produced for all selected sessions. By default, images are only saved for inner nodes of the hierarchy of sessions, as required for other sessions to continue later on.