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