isabelle: src/Pure/Sessions.thy@fad29d2a17a5 (annotated)

67215 03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	1	(* Title: Pure/Thy/Sessions.thy
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	2	Author: Makarius
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	3
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	4	PIDE markup for session ROOT.
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	5	*)
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	6
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	7	theory Sessions
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	8	imports Pure
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	9	keywords "session" :: thy_decl
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	10	and "description" "options" "sessions" "theories" "document_files" :: quasi_command
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	11	and "global"
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	12	begin
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	13
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	14	ML \<open>
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	15	Outer_Syntax.command \<^command_keyword>\<open>session\<close> "PIDE markup for session ROOT"
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	16	Sessions.command_parser;
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	17	\<close>
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	18
03d0c958d65a PIDE markup for session ROOT files; wenzelm parents: diff changeset	19	end

author	immler
	Thu, 03 May 2018 15:07:14 +0200
changeset 68073	fad29d2a17a5
parent 67215	03d0c958d65a
child 68189	6163c90694ef
permissions	-rw-r--r--