src/Pure/Sessions.thy
author wenzelm
Tue, 16 Jan 2018 11:27:52 +0100
changeset 67446 1f4d167b6ac9
parent 67215 03d0c958d65a
child 68189 6163c90694ef
permissions -rw-r--r--
discontinued old form of marginal comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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