src/Pure/Sessions.thy
author paulson <lp15@cam.ac.uk>
Wed, 24 Apr 2024 09:21:44 +0100
changeset 80148 b156869b826a
parent 75986 27d98da31985
permissions -rw-r--r--
Another Nominal example
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
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 72600
diff changeset
     9
  keywords "chapter_definition" "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>
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 72600
diff changeset
    16
  Outer_Syntax.command \<^command_keyword>\<open>chapter_definition\<close> "PIDE markup for session ROOT"
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 72600
diff changeset
    17
    Sessions.chapter_definition_parser;
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 72600
diff changeset
    18
67215
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents:
diff changeset
    19
  Outer_Syntax.command \<^command_keyword>\<open>session\<close> "PIDE markup for session ROOT"
75986
27d98da31985 support 'chapter_definition' with description for presentation purposes;
wenzelm
parents: 72600
diff changeset
    20
    Sessions.session_parser;
67215
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents:
diff changeset
    21
\<close>
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents:
diff changeset
    22
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents:
diff changeset
    23
end