| author | wenzelm | 
| Tue, 28 Aug 2018 11:40:11 +0200 | |
| changeset 68829 | 1a4fa494a4a8 | 
| 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 |