added type 'a parser, simplified signature;
authorwenzelm
Fri Jan 02 15:44:33 2009 +0100 (2009-01-02)
changeset 29312f369fb19146e
parent 29311 4c830711e6f1
child 29313 6852248da4b4
added type 'a parser, simplified signature;
src/Pure/Isar/spec_parse.ML
     1.1 --- a/src/Pure/Isar/spec_parse.ML	Fri Jan 02 15:44:33 2009 +0100
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Fri Jan 02 15:44:33 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Pure/Isar/spec_parse.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Makarius
     1.7  
     1.8  Parsers for complex specifications.
     1.9 @@ -7,35 +6,33 @@
    1.10  
    1.11  signature SPEC_PARSE =
    1.12  sig
    1.13 -  type token
    1.14 -  val attrib: OuterLex.token list -> Attrib.src * token list
    1.15 -  val attribs: token list -> Attrib.src list * token list
    1.16 -  val opt_attribs: token list -> Attrib.src list * token list
    1.17 -  val thm_name: string -> token list -> Attrib.binding * token list
    1.18 -  val opt_thm_name: string -> token list -> Attrib.binding * token list
    1.19 -  val spec: token list -> (Attrib.binding * string list) * token list
    1.20 -  val named_spec: token list -> (Attrib.binding * string list) * token list
    1.21 -  val spec_name: token list -> ((Binding.T * string) * Attrib.src list) * token list
    1.22 -  val spec_opt_name: token list -> ((Binding.T * string) * Attrib.src list) * token list
    1.23 -  val xthm: token list -> (Facts.ref * Attrib.src list) * token list
    1.24 -  val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
    1.25 -  val name_facts: token list ->
    1.26 -    (Attrib.binding * (Facts.ref * Attrib.src list) list) list * token list
    1.27 -  val locale_mixfix: token list -> mixfix * token list
    1.28 -  val locale_fixes: token list -> (Binding.T * string option * mixfix) list * token list
    1.29 -  val locale_insts: token list -> (string option list * (Attrib.binding * string) list) * token list
    1.30 -  val class_expr: token list -> string list * token list
    1.31 -  val locale_expr: token list -> Locale.expr * token list
    1.32 -  val locale_expression: OuterParse.token list -> Expression.expression * OuterParse.token list
    1.33 -  val locale_keyword: token list -> string * token list
    1.34 -  val context_element: token list -> Element.context * token list
    1.35 -  val statement: token list -> (Attrib.binding * (string * string list) list) list * token list
    1.36 -  val general_statement: token list ->
    1.37 -    (Element.context list * Element.statement) * OuterLex.token list
    1.38 -  val statement_keyword: token list -> string * token list
    1.39 -  val specification: token list ->
    1.40 -    (Binding.T *
    1.41 -      ((Attrib.binding * string list) list * (Binding.T * string option) list)) list * token list
    1.42 +  type token = OuterParse.token
    1.43 +  type 'a parser = 'a OuterParse.parser
    1.44 +  val attrib: Attrib.src parser
    1.45 +  val attribs: Attrib.src list parser
    1.46 +  val opt_attribs: Attrib.src list parser
    1.47 +  val thm_name: string -> Attrib.binding parser
    1.48 +  val opt_thm_name: string -> Attrib.binding parser
    1.49 +  val spec: (Attrib.binding * string list) parser
    1.50 +  val named_spec: (Attrib.binding * string list) parser
    1.51 +  val spec_name: ((Binding.T * string) * Attrib.src list) parser
    1.52 +  val spec_opt_name: ((Binding.T * string) * Attrib.src list) parser
    1.53 +  val xthm: (Facts.ref * Attrib.src list) parser
    1.54 +  val xthms1: (Facts.ref * Attrib.src list) list parser
    1.55 +  val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
    1.56 +  val locale_mixfix: mixfix parser
    1.57 +  val locale_fixes: (Binding.T * string option * mixfix) list parser
    1.58 +  val locale_insts: (string option list * (Attrib.binding * string) list) parser
    1.59 +  val class_expr: string list parser
    1.60 +  val locale_expr: Locale.expr parser
    1.61 +  val locale_expression: Expression.expression parser
    1.62 +  val locale_keyword: string parser
    1.63 +  val context_element: Element.context parser
    1.64 +  val statement: (Attrib.binding * (string * string list) list) list parser
    1.65 +  val general_statement: (Element.context list * Element.statement) parser
    1.66 +  val statement_keyword: string parser
    1.67 +  val specification:
    1.68 +    (Binding.T * ((Attrib.binding * string list) list * (Binding.T * string option) list)) list parser
    1.69  end;
    1.70  
    1.71  structure SpecParse: SPEC_PARSE =
    1.72 @@ -43,6 +40,7 @@
    1.73  
    1.74  structure P = OuterParse;
    1.75  type token = P.token;
    1.76 +type 'a parser = 'a P.parser;
    1.77  
    1.78  
    1.79  (* theorem specifications *)