40 forms like identifiers, names, quoted strings, verbatim text, nested |
40 forms like identifiers, names, quoted strings, verbatim text, nested |
41 comments etc. The grammar for @{syntax chapter_def}, @{syntax chapter_entry} |
41 comments etc. The grammar for @{syntax chapter_def}, @{syntax chapter_entry} |
42 and @{syntax session_entry} is given as syntax diagram below. Each ROOT file |
42 and @{syntax session_entry} is given as syntax diagram below. Each ROOT file |
43 may contain multiple specifications like this. Chapters help to organize |
43 may contain multiple specifications like this. Chapters help to organize |
44 browser info (\secref{sec:info}), but have no formal meaning. The default |
44 browser info (\secref{sec:info}), but have no formal meaning. The default |
45 chapter is ``\<open>Unsorted\<close>''. Chapter definitions are optional: the main |
45 chapter is ``\<open>Unsorted\<close>''. Chapter definitions, which are optional, allow to |
46 purpose is to associate a description for presentation. |
46 associate additional information. |
47 |
47 |
48 Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode |
48 Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode |
49 \<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is enabled by default for any |
49 \<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is enabled by default for any |
50 file of that name. |
50 file of that name. |
51 |
51 |
52 \<^rail>\<open> |
52 \<^rail>\<open> |
53 @{syntax_def chapter_def}: @'chapter_definition' @{syntax name} description? |
53 @{syntax_def chapter_def}: @'chapter_definition' @{syntax name} \<newline> |
|
54 groups? description? |
54 ; |
55 ; |
55 |
56 |
56 @{syntax_def chapter_entry}: @'chapter' @{syntax name} |
57 @{syntax_def chapter_entry}: @'chapter' @{syntax name} |
57 ; |
58 ; |
58 |
59 |
87 document_files: @'document_files' ('(' dir ')')? (@{syntax embedded}+) |
88 document_files: @'document_files' ('(' dir ')')? (@{syntax embedded}+) |
88 ; |
89 ; |
89 export_files: @'export_files' ('(' dir ')')? ('[' nat ']')? \<newline> |
90 export_files: @'export_files' ('(' dir ')')? ('[' nat ']')? \<newline> |
90 (@{syntax embedded}+) |
91 (@{syntax embedded}+) |
91 \<close> |
92 \<close> |
|
93 |
|
94 \<^descr> \isakeyword{chapter{\isacharunderscorekeyword}definition}~\<open>A (groups)\<close> |
|
95 associates a collection of groups with chapter \<open>A\<close>. All sessions that belong |
|
96 to this chapter will automatically become members of these groups. |
92 |
97 |
93 \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on |
98 \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on |
94 parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions and |
99 parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions and |
95 theories). Note that a parent (like \<open>HOL\<close>) is mandatory in practical |
100 theories). Note that a parent (like \<open>HOL\<close>) is mandatory in practical |
96 applications: only Isabelle/Pure can bootstrap itself from nothing. |
101 applications: only Isabelle/Pure can bootstrap itself from nothing. |
112 \<^verbatim>\<open>ROOT\<close> file. |
117 \<^verbatim>\<open>ROOT\<close> file. |
113 |
118 |
114 All theory files are located relatively to the session directory. The prover |
119 All theory files are located relatively to the session directory. The prover |
115 process is run within the same as its current working directory. |
120 process is run within the same as its current working directory. |
116 |
121 |
117 \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this |
122 \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form description for this |
118 session. |
123 session (or chapter), e.g. for presentation purposes. |
119 |
124 |
120 \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options |
125 \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options |
121 (\secref{sec:system-options}) that are used when processing this session, |
126 (\secref{sec:system-options}) that are used when processing this session, |
122 but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z = |
127 but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z = |
123 true\<close> for Boolean options. |
128 true\<close> for Boolean options. |