src/Pure/Sessions.thy
author wenzelm
Tue, 15 May 2018 13:57:39 +0200
changeset 68189 6163c90694ef
parent 67215 03d0c958d65a
child 68292 7ca0c23179e6
permissions -rw-r--r--
tuned headers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
68189
6163c90694ef tuned headers;
wenzelm
parents: 67215
diff changeset
     1
(*  Title:      Pure/Sessions.thy
67215
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