| author | wenzelm | 
| Sun, 04 Dec 2022 14:15:12 +0100 | |
| changeset 76552 | 13fde66c7cf6 | 
| parent 75986 | 27d98da31985 | 
| permissions | -rw-r--r-- | 
| 68189 | 1 | (* Title: Pure/Sessions.thy | 
| 67215 | 2 | Author: Makarius | 
| 3 | ||
| 4 | PIDE markup for session ROOT. | |
| 5 | *) | |
| 6 | ||
| 7 | theory Sessions | |
| 8 | imports Pure | |
| 75986 
27d98da31985
support 'chapter_definition' with description for presentation purposes;
 wenzelm parents: 
72600diff
changeset | 9 | keywords "chapter_definition" "session" :: thy_decl | 
| 70668 | 10 | and "description" "directories" "options" "sessions" "theories" | 
| 72600 
2fa4f25d9d07
official support for document theories from other sessions;
 wenzelm parents: 
70681diff
changeset | 11 | "document_theories" "document_files" "export_files" :: quasi_command | 
| 70681 | 12 | and "global" | 
| 67215 | 13 | begin | 
| 14 | ||
| 15 | ML \<open> | |
| 75986 
27d98da31985
support 'chapter_definition' with description for presentation purposes;
 wenzelm parents: 
72600diff
changeset | 16 | Outer_Syntax.command \<^command_keyword>\<open>chapter_definition\<close> "PIDE markup for session ROOT" | 
| 
27d98da31985
support 'chapter_definition' with description for presentation purposes;
 wenzelm parents: 
72600diff
changeset | 17 | Sessions.chapter_definition_parser; | 
| 
27d98da31985
support 'chapter_definition' with description for presentation purposes;
 wenzelm parents: 
72600diff
changeset | 18 | |
| 67215 | 19 | Outer_Syntax.command \<^command_keyword>\<open>session\<close> "PIDE markup for session ROOT" | 
| 75986 
27d98da31985
support 'chapter_definition' with description for presentation purposes;
 wenzelm parents: 
72600diff
changeset | 20 | Sessions.session_parser; | 
| 67215 | 21 | \<close> | 
| 22 | ||
| 23 | end |