src/Pure/Isar/thy_header.ML
author wenzelm
Sat, 21 Jan 2006 23:02:14 +0100
changeset 18728 6790126ab5f6
parent 17978 b48885914c1d
permissions -rw-r--r--
simplified type attribute;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9139
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/thy_header.ML
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
     4
17978
b48885914c1d tuned header;
wenzelm
parents: 17933
diff changeset
     5
Theory headers -- processed separately with minimal outer syntax.
9139
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
     6
*)
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
     7
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
     8
signature THY_HEADER =
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
     9
sig
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
    10
  val args: OuterLex.token list ->
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
    11
    (string * string list * (string * bool) list) * OuterLex.token list
17933
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    12
  val read: (string, 'a) Source.source * Position.T ->
16265
ee2497cde564 new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents: 15531
diff changeset
    13
    string * string list * (string * bool) list
9139
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
    14
end;
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
    15
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
    16
structure ThyHeader: THY_HEADER =
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
    17
struct
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
    18
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
    19
structure T = OuterLex;
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
    20
structure P = OuterParse;
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
    21
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
    22
17933
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    23
(* keywords *)
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    24
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    25
val headerN = "header";
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    26
val theoryN = "theory";
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    27
val importsN = "imports";
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    28
val usesN = "uses";
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    29
val beginN = "begin";
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    30
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    31
val header_lexicon = T.make_lexicon
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    32
  ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN];
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    33
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    34
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    35
(* header args *)
9139
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
    36
17933
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    37
val file = (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    38
val uses = Scan.optional (P.$$$ usesN |-- P.!!! (Scan.repeat1 file)) [];
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    39
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    40
val args =
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    41
  P.name -- (P.$$$ importsN |-- P.!!! (Scan.repeat1 P.name -- uses --| P.$$$ beginN))
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    42
  >> P.triple2;
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    43
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    44
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    45
(* read header *)
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    46
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    47
val header =
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    48
  (P.$$$ headerN -- P.tags) |-- (P.!!! (P.text -- Scan.repeat P.semicolon --
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    49
    (P.$$$ theoryN -- P.tags) |-- args)) ||
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    50
  (P.$$$ theoryN -- P.tags) |-- P.!!! args;
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    51
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    52
fun read (src, pos) =
12840
c7066d8b684f error "Unexpected end of input";
wenzelm
parents: 9139
diff changeset
    53
  let val res =
c7066d8b684f error "Unexpected end of input";
wenzelm
parents: 9139
diff changeset
    54
    src
c7066d8b684f error "Unexpected end of input";
wenzelm
parents: 9139
diff changeset
    55
    |> Symbol.source false
17933
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    56
    |> T.source false (fn () => (header_lexicon, Scan.empty_lexicon)) pos
12840
c7066d8b684f error "Unexpected end of input";
wenzelm
parents: 9139
diff changeset
    57
    |> T.source_proper
17933
b8f2dd8858f6 removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm
parents: 17075
diff changeset
    58
    |> Source.source T.stopper (Scan.single (Scan.error header)) NONE
12840
c7066d8b684f error "Unexpected end of input";
wenzelm
parents: 9139
diff changeset
    59
    |> Source.get_single;
c7066d8b684f error "Unexpected end of input";
wenzelm
parents: 9139
diff changeset
    60
  in
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15141
diff changeset
    61
    (case res of SOME (x, _) => x
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15141
diff changeset
    62
    | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
12840
c7066d8b684f error "Unexpected end of input";
wenzelm
parents: 9139
diff changeset
    63
  end;
9139
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
    64
bf272b4985ec Theory headers (old and new-style).
wenzelm
parents:
diff changeset
    65
end;