wenzelm@22106: (*  Title:      Pure/Thy/thy_header.ML
wenzelm@22106:     ID:         $Id$
wenzelm@22106:     Author:     Markus Wenzel, TU Muenchen
wenzelm@22106: 
wenzelm@22106: Theory headers -- independent of outer syntax.
wenzelm@22106: *)
wenzelm@22106: 
wenzelm@22106: signature THY_HEADER =
wenzelm@22106: sig
wenzelm@22106:   val args: OuterLex.token list ->
wenzelm@22106:     (string * string list * (string * bool) list) * OuterLex.token list
wenzelm@23863:   val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
wenzelm@22106: end;
wenzelm@22106: 
wenzelm@22106: structure ThyHeader: THY_HEADER =
wenzelm@22106: struct
wenzelm@22106: 
wenzelm@22106: structure T = OuterLex;
wenzelm@22106: structure P = OuterParse;
wenzelm@22106: 
wenzelm@22106: 
wenzelm@22106: (* keywords *)
wenzelm@22106: 
wenzelm@22106: val headerN = "header";
wenzelm@22106: val theoryN = "theory";
wenzelm@22106: val importsN = "imports";
wenzelm@22106: val usesN = "uses";
wenzelm@22106: val beginN = "begin";
wenzelm@22106: 
wenzelm@22106: val header_lexicon = T.make_lexicon
wenzelm@22106:   ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN];
wenzelm@22106: 
wenzelm@22106: 
wenzelm@22106: (* header args *)
wenzelm@22106: 
wenzelm@22106: val file = (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
wenzelm@22106: val uses = Scan.optional (P.$$$ usesN |-- P.!!! (Scan.repeat1 file)) [];
wenzelm@22106: 
wenzelm@22106: val args =
wenzelm@22106:   P.name -- (P.$$$ importsN |-- P.!!! (Scan.repeat1 P.name -- uses --| P.$$$ beginN))
wenzelm@22106:   >> P.triple2;
wenzelm@22106: 
wenzelm@22106: 
wenzelm@22106: (* read header *)
wenzelm@22106: 
wenzelm@22106: val header =
wenzelm@22106:   (P.$$$ headerN -- P.tags) |-- (P.!!! (P.text -- Scan.repeat P.semicolon --
wenzelm@22106:     (P.$$$ theoryN -- P.tags) |-- args)) ||
wenzelm@22106:   (P.$$$ theoryN -- P.tags) |-- P.!!! args;
wenzelm@22106: 
wenzelm@23863: fun read pos src =
wenzelm@22106:   let val res =
wenzelm@22106:     src
wenzelm@22106:     |> Symbol.source false
wenzelm@23677:     |> T.source NONE (fn () => (header_lexicon, Scan.empty_lexicon)) pos
wenzelm@22106:     |> T.source_proper
wenzelm@22106:     |> Source.source T.stopper (Scan.single (Scan.error header)) NONE
wenzelm@22106:     |> Source.get_single;
wenzelm@22106:   in
wenzelm@22106:     (case res of SOME (x, _) => x
wenzelm@22106:     | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
wenzelm@22106:   end;
wenzelm@22106: 
wenzelm@22106: end;