# HG changeset patch
# User wenzelm
# Date 1087298619 -7200
# Node ID 5f5605361aad12030ea9884b6e9c104e2e0807cf
# Parent  aa6d54648b32042de611083d08be611d81b238f0
added path;

diff -r aa6d54648b32 -r 5f5605361aad src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Tue Jun 15 13:23:23 2004 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Tue Jun 15 13:23:39 2004 +0200
@@ -45,6 +45,7 @@
   val name: token list -> bstring * token list
   val xname: token list -> xstring * token list
   val text: token list -> string * token list
+  val path: token list -> Path.T * token list
   val uname: token list -> string option * token list
   val sort: token list -> string * token list
   val arity: token list -> (string list * string) * token list
@@ -175,6 +176,7 @@
 val name = group "name declaration" (short_ident || sym_ident || string || number);
 val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
+val path = group "file name/path specification" name >> Path.unpack;
 
 val uname = underscore >> K None || name >> Some;