src/Pure/Sessions.thy
author wenzelm
Fri, 03 Jul 2020 17:00:41 +0200
changeset 71993 088e3aa85250
parent 70681 a6c0f2d106c8
child 72600 2fa4f25d9d07
permissions -rw-r--r--
clarified signature;
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
70668
9cac4dec0da9 support for explicit session directories;
wenzelm
parents: 68292
diff changeset
    10
    and "description" "directories" "options" "sessions" "theories"
68292
7ca0c23179e6 support 'export_files' in session ROOT;
wenzelm
parents: 68189
diff changeset
    11
      "document_files" "export_files" :: quasi_command
70681
a6c0f2d106c8 disallow overlapping session directories;
wenzelm
parents: 70668
diff changeset
    12
    and "global"
67215
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents:
diff changeset
    13
begin
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents:
diff changeset
    14
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents:
diff changeset
    15
ML \<open>
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents:
diff changeset
    16
  Outer_Syntax.command \<^command_keyword>\<open>session\<close> "PIDE markup for session ROOT"
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents:
diff changeset
    17
    Sessions.command_parser;
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents:
diff changeset
    18
\<close>
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents:
diff changeset
    19
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents:
diff changeset
    20
end