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