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