src/Pure/Thy/thy_header.ML
changeset 23863 8f3099589cfa
parent 23677 1114cc909800
child 24577 c6acb6d79757
equal deleted inserted replaced
23862:b1861768d8f4 23863:8f3099589cfa
     7 
     7 
     8 signature THY_HEADER =
     8 signature THY_HEADER =
     9 sig
     9 sig
    10   val args: OuterLex.token list ->
    10   val args: OuterLex.token list ->
    11     (string * string list * (string * bool) list) * OuterLex.token list
    11     (string * string list * (string * bool) list) * OuterLex.token list
    12   val read: (string, 'a) Source.source * Position.T ->
    12   val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
    13     string * string list * (string * bool) list
       
    14 end;
    13 end;
    15 
    14 
    16 structure ThyHeader: THY_HEADER =
    15 structure ThyHeader: THY_HEADER =
    17 struct
    16 struct
    18 
    17 
    47 val header =
    46 val header =
    48   (P.$$$ headerN -- P.tags) |-- (P.!!! (P.text -- Scan.repeat P.semicolon --
    47   (P.$$$ headerN -- P.tags) |-- (P.!!! (P.text -- Scan.repeat P.semicolon --
    49     (P.$$$ theoryN -- P.tags) |-- args)) ||
    48     (P.$$$ theoryN -- P.tags) |-- args)) ||
    50   (P.$$$ theoryN -- P.tags) |-- P.!!! args;
    49   (P.$$$ theoryN -- P.tags) |-- P.!!! args;
    51 
    50 
    52 fun read (src, pos) =
    51 fun read pos src =
    53   let val res =
    52   let val res =
    54     src
    53     src
    55     |> Symbol.source false
    54     |> Symbol.source false
    56     |> T.source NONE (fn () => (header_lexicon, Scan.empty_lexicon)) pos
    55     |> T.source NONE (fn () => (header_lexicon, Scan.empty_lexicon)) pos
    57     |> T.source_proper
    56     |> T.source_proper