| author | wenzelm | 
| Fri, 23 Feb 2018 14:32:59 +0100 | |
| changeset 67703 | 8c4806fe827f | 
| parent 67215 | 03d0c958d65a | 
| child 68189 | 6163c90694ef | 
| permissions | -rw-r--r-- | 
| 67215 | 1 | (* Title: Pure/Thy/Sessions.thy | 
| 2 | Author: Makarius | |
| 3 | ||
| 4 | PIDE markup for session ROOT. | |
| 5 | *) | |
| 6 | ||
| 7 | theory Sessions | |
| 8 | imports Pure | |
| 9 | keywords "session" :: thy_decl | |
| 10 | and "description" "options" "sessions" "theories" "document_files" :: quasi_command | |
| 11 | and "global" | |
| 12 | begin | |
| 13 | ||
| 14 | ML \<open> | |
| 15 | Outer_Syntax.command \<^command_keyword>\<open>session\<close> "PIDE markup for session ROOT" | |
| 16 | Sessions.command_parser; | |
| 17 | \<close> | |
| 18 | ||
| 19 | end |