equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 theory Sessions |
7 theory Sessions |
8 imports Pure |
8 imports Pure |
9 keywords "session" :: thy_decl |
9 keywords "session" :: thy_decl |
10 and "description" "options" "sessions" "theories" "document_files" :: quasi_command |
10 and "description" "options" "sessions" "theories" |
|
11 "document_files" "export_files" :: quasi_command |
11 and "global" |
12 and "global" |
12 begin |
13 begin |
13 |
14 |
14 ML \<open> |
15 ML \<open> |
15 Outer_Syntax.command \<^command_keyword>\<open>session\<close> "PIDE markup for session ROOT" |
16 Outer_Syntax.command \<^command_keyword>\<open>session\<close> "PIDE markup for session ROOT" |