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