src/Pure/Thy/thy_header.ML
changeset 58918 8d36bc5eaed3
parent 58908 58bedbc18915
child 58920 2f8168dc0eac
equal deleted inserted replaced
58910:edcd9339bda1 58918:8d36bc5eaed3
    10   type header =
    10   type header =
    11    {name: string * Position.T,
    11    {name: string * Position.T,
    12     imports: (string * Position.T) list,
    12     imports: (string * Position.T) list,
    13     keywords: keywords}
    13     keywords: keywords}
    14   val make: string * Position.T -> (string * Position.T) list -> keywords -> header
    14   val make: string * Position.T -> (string * Position.T) list -> keywords -> header
    15   val define_keywords: header -> unit
    15   val define_keywords: keywords -> unit
    16   val declare_keyword: string * Keyword.spec option -> theory -> theory
    16   val declare_keyword: string * Keyword.spec option -> theory -> theory
    17   val the_keyword: theory -> string -> Keyword.spec option
    17   val the_keyword: theory -> string -> Keyword.spec option
    18   val args: header parser
    18   val args: header parser
    19   val read: Position.T -> string -> header
    19   val read: Position.T -> string -> header
    20   val read_tokens: Token.T list -> header
    20   val read_tokens: Token.T list -> header
    35 
    35 
    36 
    36 
    37 
    37 
    38 (** keyword declarations **)
    38 (** keyword declarations **)
    39 
    39 
    40 fun define_keywords ({keywords, ...}: header) =
    40 fun define_keywords (keywords: keywords) =
    41   List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords;
    41   List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords;
    42 
    42 
    43 fun err_dup name = error ("Duplicate declaration of outer syntax keyword " ^ quote name);
    43 fun err_dup name = error ("Duplicate declaration of outer syntax keyword " ^ quote name);
    44 
    44 
    45 structure Data = Theory_Data
    45 structure Data = Theory_Data