| author | wenzelm |
| Sun, 05 Apr 2020 13:19:29 +0200 | |
| changeset 71693 | f249b5c0fea2 |
| parent 70681 | a6c0f2d106c8 |
| child 72600 | 2fa4f25d9d07 |
| 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 |
|
9 |
keywords "session" :: thy_decl |
|
| 70668 | 10 |
and "description" "directories" "options" "sessions" "theories" |
| 68292 | 11 |
"document_files" "export_files" :: quasi_command |
| 70681 | 12 |
and "global" |
| 67215 | 13 |
begin |
14 |
||
15 |
ML \<open> |
|
16 |
Outer_Syntax.command \<^command_keyword>\<open>session\<close> "PIDE markup for session ROOT" |
|
17 |
Sessions.command_parser; |
|
18 |
\<close> |
|
19 |
||
20 |
end |