src/Pure/Isar/thy_header.ML
author wenzelm
Tue Dec 05 22:14:42 2006 +0100 (2006-12-05)
changeset 21658 5e31241e1e3c
parent 17978 b48885914c1d
permissions -rw-r--r--
Attrib.internal: morphism;
wenzelm@9139
     1
(*  Title:      Pure/Isar/thy_header.ML
wenzelm@9139
     2
    ID:         $Id$
wenzelm@9139
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@9139
     4
wenzelm@17978
     5
Theory headers -- processed separately with minimal outer syntax.
wenzelm@9139
     6
*)
wenzelm@9139
     7
wenzelm@9139
     8
signature THY_HEADER =
wenzelm@9139
     9
sig
wenzelm@9139
    10
  val args: OuterLex.token list ->
wenzelm@9139
    11
    (string * string list * (string * bool) list) * OuterLex.token list
wenzelm@17933
    12
  val read: (string, 'a) Source.source * Position.T ->
wenzelm@16265
    13
    string * string list * (string * bool) list
wenzelm@9139
    14
end;
wenzelm@9139
    15
wenzelm@9139
    16
structure ThyHeader: THY_HEADER =
wenzelm@9139
    17
struct
wenzelm@9139
    18
wenzelm@9139
    19
structure T = OuterLex;
wenzelm@9139
    20
structure P = OuterParse;
wenzelm@9139
    21
wenzelm@9139
    22
wenzelm@17933
    23
(* keywords *)
wenzelm@17933
    24
wenzelm@17933
    25
val headerN = "header";
wenzelm@17933
    26
val theoryN = "theory";
wenzelm@17933
    27
val importsN = "imports";
wenzelm@17933
    28
val usesN = "uses";
wenzelm@17933
    29
val beginN = "begin";
wenzelm@17933
    30
wenzelm@17933
    31
val header_lexicon = T.make_lexicon
wenzelm@17933
    32
  ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN];
wenzelm@17933
    33
wenzelm@17933
    34
wenzelm@17933
    35
(* header args *)
wenzelm@9139
    36
wenzelm@17933
    37
val file = (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
wenzelm@17933
    38
val uses = Scan.optional (P.$$$ usesN |-- P.!!! (Scan.repeat1 file)) [];
wenzelm@17933
    39
wenzelm@17933
    40
val args =
wenzelm@17933
    41
  P.name -- (P.$$$ importsN |-- P.!!! (Scan.repeat1 P.name -- uses --| P.$$$ beginN))
wenzelm@17933
    42
  >> P.triple2;
wenzelm@17933
    43
wenzelm@17933
    44
wenzelm@17933
    45
(* read header *)
wenzelm@17933
    46
wenzelm@17933
    47
val header =
wenzelm@17933
    48
  (P.$$$ headerN -- P.tags) |-- (P.!!! (P.text -- Scan.repeat P.semicolon --
wenzelm@17933
    49
    (P.$$$ theoryN -- P.tags) |-- args)) ||
wenzelm@17933
    50
  (P.$$$ theoryN -- P.tags) |-- P.!!! args;
wenzelm@17933
    51
wenzelm@17933
    52
fun read (src, pos) =
wenzelm@12840
    53
  let val res =
wenzelm@12840
    54
    src
wenzelm@12840
    55
    |> Symbol.source false
wenzelm@17933
    56
    |> T.source false (fn () => (header_lexicon, Scan.empty_lexicon)) pos
wenzelm@12840
    57
    |> T.source_proper
wenzelm@17933
    58
    |> Source.source T.stopper (Scan.single (Scan.error header)) NONE
wenzelm@12840
    59
    |> Source.get_single;
wenzelm@12840
    60
  in
skalberg@15531
    61
    (case res of SOME (x, _) => x
skalberg@15531
    62
    | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
wenzelm@12840
    63
  end;
wenzelm@9139
    64
wenzelm@9139
    65
end;