| author | paulson <lp15@cam.ac.uk> | 
| Mon, 30 Nov 2020 11:06:01 +0000 | |
| changeset 72794 | 3757e64e75bb | 
| parent 72600 | 2fa4f25d9d07 | 
| child 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  | 
|
9  | 
keywords "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>  | 
|
16  | 
Outer_Syntax.command \<^command_keyword>\<open>session\<close> "PIDE markup for session ROOT"  | 
|
17  | 
Sessions.command_parser;  | 
|
18  | 
\<close>  | 
|
19  | 
||
20  | 
end  |