src/Doc/System/Sessions.thy
changeset 72769 4dcd05a26795
parent 72648 1cbac4ae934d
child 72876 626fcaebd049
equal deleted inserted replaced
72768:4ab04bafae35 72769:4dcd05a26795
   149   should not claim any global theory names.
   149   should not claim any global theory names.
   150 
   150 
   151   \<^descr> \isakeyword{document_theories}~\<open>names\<close> specifies theories from other
   151   \<^descr> \isakeyword{document_theories}~\<open>names\<close> specifies theories from other
   152   sessions that should be included in the generated document source directory.
   152   sessions that should be included in the generated document source directory.
   153   These theories need to be explicit imports in the current session, or
   153   These theories need to be explicit imports in the current session, or
   154   impliciti imports from the underlying hierarchy of parent sessions. The
   154   implicit imports from the underlying hierarchy of parent sessions. The
   155   generated \<^verbatim>\<open>session.tex\<close> file is not affected: the session's {\LaTeX} setup
   155   generated \<^verbatim>\<open>session.tex\<close> file is not affected: the session's {\LaTeX} setup
   156   needs to \<^verbatim>\<open>\input{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> generated \<^verbatim>\<open>.tex\<close> files separately.
   156   needs to \<^verbatim>\<open>\input{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> generated \<^verbatim>\<open>.tex\<close> files separately.
   157 
   157 
   158   \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists
   158   \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists
   159   source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for
   159   source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for