| author | wenzelm |
| Tue, 13 Oct 2020 20:28:43 +0200 | |
| changeset 72470 | e2e9ef9aa2df |
| parent 70681 | a6c0f2d106c8 |
| child 72600 | 2fa4f25d9d07 |
| permissions | -rw-r--r-- |
(* Title: Pure/Sessions.thy Author: Makarius PIDE markup for session ROOT. *) theory Sessions imports Pure keywords "session" :: thy_decl and "description" "directories" "options" "sessions" "theories" "document_files" "export_files" :: quasi_command and "global" begin ML \<open> Outer_Syntax.command \<^command_keyword>\<open>session\<close> "PIDE markup for session ROOT" Sessions.command_parser; \<close> end