author | wenzelm |
Sun, 19 May 2024 18:43:45 +0200 | |
changeset 80181 | aa92c0f96036 |
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 |