| author | nipkow | 
| Mon, 14 Jan 2019 16:10:56 +0100 | |
| changeset 69655 | 2b56cbb02e8a | 
| parent 68292 | 7ca0c23179e6 | 
| child 70668 | 9cac4dec0da9 | 
| 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  | 
|
| 68292 | 10  | 
and "description" "options" "sessions" "theories"  | 
11  | 
"document_files" "export_files" :: quasi_command  | 
|
| 67215 | 12  | 
and "global"  | 
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  |