author | paulson <lp15@cam.ac.uk> |
Sat, 26 May 2018 08:36:09 +0100 | |
changeset 68284 | 5e4e006f9552 |
parent 68189 | 6163c90694ef |
child 68292 | 7ca0c23179e6 |
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 |
|
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 |