added uname;
authorwenzelm
Thu Nov 22 17:14:17 2001 +0100 (2001-11-22)
changeset 1226828e60c998eee
parent 12267 50e2bca71c9d
child 12269 fda9192d0344
added uname;
syntax for locale expressions (presently unused);
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Thu Nov 22 17:13:36 2001 +0100
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Thu Nov 22 17:14:17 2001 +0100
     1.3 @@ -44,6 +44,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 uname: token list -> string option * token list
     1.8    val comment: token list -> Comment.text * token list
     1.9    val marg_comment: token list -> Comment.text * token list
    1.10    val interest: token list -> Comment.interest * token list
    1.11 @@ -172,6 +173,8 @@
    1.12  val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
    1.13  val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
    1.14  
    1.15 +val uname = underscore >> K None || name >> Some;
    1.16 +
    1.17  
    1.18  (* formal comments *)
    1.19  
    1.20 @@ -303,6 +306,13 @@
    1.21  
    1.22  (* locale elements *)
    1.23  
    1.24 +(* FIXME
    1.25 +fun expr2 x = (xname >> Locale.Locale || $$$ "(" |-- !!! (expr0 --| $$$ ")")) x
    1.26 +and expr1 x = (expr2 -- Scan.repeat1 uname >> Locale.Rename || expr2) x
    1.27 +and expr0 x = (enum1 "+" expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
    1.28 +*)
    1.29 +val expr0 = xname;
    1.30 +
    1.31  val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K None || opt_mixfix >> Some;
    1.32  
    1.33  val locale_element = group "locale element"
    1.34 @@ -313,7 +323,7 @@
    1.35    $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
    1.36      >> Locale.Defines ||
    1.37    $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1)) >> Locale.Notes ||
    1.38 -  $$$ "uses" |-- !!! xname >> (Locale.Uses o Locale.Locale));
    1.39 +  $$$ "uses" |-- !!! expr0 >> (Locale.Uses o Locale.Locale));
    1.40  
    1.41  
    1.42  (* proof methods *)