| author | wenzelm | 
| Mon, 07 Dec 2020 16:09:06 +0100 | |
| changeset 72841 | fd8d82c4433b | 
| 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: 
70681diff
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 |