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