explicit type Name.binding for higher-specification elements;
authorwenzelm
Tue Sep 02 14:10:31 2008 +0200 (2008-09-02)
changeset 28081d664b2c1dfe6
parent 28080 4723eb2456ce
child 28082 37350f301128
explicit type Name.binding for higher-specification elements;
added binding, parbinding;
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Tue Sep 02 14:10:30 2008 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Tue Sep 02 14:10:31 2008 +0200
     1.3 @@ -62,10 +62,12 @@
     1.4    val list1: (token list -> 'a * token list) -> token list -> 'a list * token list
     1.5    val properties: token list -> Properties.T * token list
     1.6    val name: token list -> bstring * token list
     1.7 +  val binding: token list -> Name.binding * token list
     1.8    val xname: token list -> xstring * token list
     1.9    val text: token list -> string * token list
    1.10    val path: token list -> Path.T * token list
    1.11    val parname: token list -> string * token list
    1.12 +  val parbinding: token list -> Name.binding * token list
    1.13    val sort: token list -> string * token list
    1.14    val arity: token list -> (string * string list * string) * token list
    1.15    val multi_arity: token list -> (string list * string list * string) * token list
    1.16 @@ -80,11 +82,11 @@
    1.17    val opt_mixfix': token list -> mixfix * token list
    1.18    val where_: token list -> string * token list
    1.19    val const: token list -> (string * string * mixfix) * token list
    1.20 -  val params: token list -> (string * string option) list * token list
    1.21 -  val simple_fixes: token list -> (string * string option) list * token list
    1.22 -  val fixes: token list -> (string * string option * mixfix) list * token list
    1.23 -  val for_fixes: token list -> (string * string option * mixfix) list * token list
    1.24 -  val for_simple_fixes: token list -> (string * string option) list * token list
    1.25 +  val params: token list -> (Name.binding * string option) list * token list
    1.26 +  val simple_fixes: token list -> (Name.binding * string option) list * token list
    1.27 +  val fixes: token list -> (Name.binding * string option * mixfix) list * token list
    1.28 +  val for_fixes: token list -> (Name.binding * string option * mixfix) list * token list
    1.29 +  val for_simple_fixes: token list -> (Name.binding * string option) list * token list
    1.30    val ML_source: token list -> (SymbolPos.text * Position.T) * token list
    1.31    val doc_source: token list -> (SymbolPos.text * Position.T) * token list
    1.32    val term_group: token list -> string * token list
    1.33 @@ -227,11 +229,13 @@
    1.34  (* names and text *)
    1.35  
    1.36  val name = group "name declaration" (short_ident || sym_ident || string || number);
    1.37 +val binding = position name >> Name.binding_pos;
    1.38  val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
    1.39  val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
    1.40  val path = group "file name/path specification" name >> Path.explode;
    1.41  
    1.42  val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
    1.43 +val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Name.no_binding;
    1.44  
    1.45  
    1.46  (* sorts and arities *)
    1.47 @@ -289,13 +293,13 @@
    1.48  
    1.49  val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
    1.50  
    1.51 -val params = Scan.repeat1 name -- Scan.option ($$$ "::" |-- !!! typ)
    1.52 +val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
    1.53    >> (fn (xs, T) => map (rpair T) xs);
    1.54  
    1.55  val simple_fixes = and_list1 params >> flat;
    1.56  
    1.57  val fixes =
    1.58 -  and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
    1.59 +  and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
    1.60      params >> map Syntax.no_syn) >> flat;
    1.61  
    1.62  val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];