src/Pure/Isar/parse.ML
changeset 40800 330eb65c9469
parent 40793 d21aedaa91e7
child 42287 d98eb048a2e4
     1.1 --- a/src/Pure/Isar/parse.ML	Sun Nov 28 20:36:45 2010 +0100
     1.2 +++ b/src/Pure/Isar/parse.ML	Sun Nov 28 21:07:28 2010 +0100
     1.3 @@ -63,6 +63,7 @@
     1.4    val xname: xstring parser
     1.5    val text: string parser
     1.6    val path: Path.T parser
     1.7 +  val liberal_name: xstring parser
     1.8    val parname: string parser
     1.9    val parbinding: binding parser
    1.10    val sort: string parser
    1.11 @@ -234,6 +235,8 @@
    1.12  val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
    1.13  val path = group "file name/path specification" name >> Path.explode;
    1.14  
    1.15 +val liberal_name = keyword_ident_or_symbolic || xname;
    1.16 +
    1.17  val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
    1.18  val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
    1.19