| author | desharna | 
| Fri, 29 Sep 2023 15:36:12 +0200 | |
| changeset 78733 | 70e1c0167ae2 | 
| 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: 
72600 
diff
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: 
70681 
diff
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: 
72600 
diff
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: 
72600 
diff
changeset
 | 
17  | 
Sessions.chapter_definition_parser;  | 
| 
 
27d98da31985
support 'chapter_definition' with description for presentation purposes;
 
wenzelm 
parents: 
72600 
diff
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: 
72600 
diff
changeset
 | 
20  | 
Sessions.session_parser;  | 
| 67215 | 21  | 
\<close>  | 
22  | 
||
23  | 
end  |