added path;
authorwenzelm
Tue Jun 15 13:23:39 2004 +0200 (2004-06-15)
changeset 149495f5605361aad
parent 14948 aa6d54648b32
child 14950 e22fad2b6f6f
added path;
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Tue Jun 15 13:23:23 2004 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Tue Jun 15 13:23:39 2004 +0200
     1.3 @@ -45,6 +45,7 @@
     1.4    val name: token list -> bstring * token list
     1.5    val xname: token list -> xstring * token list
     1.6    val text: token list -> string * token list
     1.7 +  val path: token list -> Path.T * token list
     1.8    val uname: token list -> string option * token list
     1.9    val sort: token list -> string * token list
    1.10    val arity: token list -> (string list * string) * token list
    1.11 @@ -175,6 +176,7 @@
    1.12  val name = group "name declaration" (short_ident || sym_ident || string || number);
    1.13  val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
    1.14  val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
    1.15 +val path = group "file name/path specification" name >> Path.unpack;
    1.16  
    1.17  val uname = underscore >> K None || name >> Some;
    1.18