src/Pure/Sessions.thy
author wenzelm
Sun, 24 Oct 2021 21:59:36 +0200
changeset 74572 08b4292abe2b
parent 72600 2fa4f25d9d07
child 75986 27d98da31985
permissions -rw-r--r--
more antiquotations;
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"
72600
2fa4f25d9d07 official support for document theories from other sessions;
wenzelm
parents: 70681
diff changeset
    11
      "document_theories" "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