36 additional project directories given by the user. |
36 additional project directories given by the user. |
37 |
37 |
38 The ROOT file format follows the lexical conventions of the \<^emph>\<open>outer syntax\<close> |
38 The ROOT file format follows the lexical conventions of the \<^emph>\<open>outer syntax\<close> |
39 of Isabelle/Isar, see also @{cite "isabelle-isar-ref"}. This defines common |
39 of Isabelle/Isar, see also @{cite "isabelle-isar-ref"}. This defines common |
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 session_chapter} and @{syntax |
41 comments etc. The grammar for @{syntax chapter_def}, @{syntax chapter_entry} |
42 session_entry} is given as syntax diagram below; each ROOT file may contain |
42 and @{syntax session_entry} is given as syntax diagram below. Each ROOT file |
43 multiple specifications like this. Chapters help to organize browser info |
43 may contain multiple specifications like this. Chapters help to organize |
44 (\secref{sec:info}), but have no formal meaning. The default chapter is |
44 browser info (\secref{sec:info}), but have no formal meaning. The default |
45 ``\<open>Unsorted\<close>''. |
45 chapter is ``\<open>Unsorted\<close>''. Chapter definitions are optional: the main |
|
46 purpose is to associate a description for presentation. |
46 |
47 |
47 Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode |
48 Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode |
48 \<^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 |
49 file of that name. |
50 file of that name. |
50 |
51 |
51 \<^rail>\<open> |
52 \<^rail>\<open> |
52 @{syntax_def session_chapter}: @'chapter' @{syntax name} |
53 @{syntax_def chapter_def}: @'chapter_definition' @{syntax name} description |
|
54 ; |
|
55 |
|
56 @{syntax_def chapter_entry}: @'chapter' @{syntax name} |
53 ; |
57 ; |
54 |
58 |
55 @{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline> |
59 @{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline> |
56 (@{syntax system_name} '+')? description? options? \<newline> |
60 (@{syntax system_name} '+')? description? options? \<newline> |
57 sessions? directories? (theories*) \<newline> |
61 sessions? directories? (theories*) \<newline> |