src/Pure/Isar/outer_parse.ML

   val and_list: (token list -> 'a * token list) -> token list -> 'a list * token list
   val and_list1: (token list -> 'a * token list) -> token list -> 'a list * token list
   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
   val type_args: token list -> string list * token list
   val typ: token list -> string * token list

 (* names and text *)
 
 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;
 
 
 (* sorts and arities *)