# HG changeset patch
# User wenzelm
# Date 1006445657 -3600
# Node ID 28e60c998eee63e2b00a568eab26a3a4ac5d7cf6
# Parent  50e2bca71c9d8c741e528924983c057160164851
added uname;
syntax for locale expressions (presently unused);

diff -r 50e2bca71c9d -r 28e60c998eee src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Thu Nov 22 17:13:36 2001 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Thu Nov 22 17:14:17 2001 +0100
@@ -44,6 +44,7 @@
   val name: token list -> bstring * token list
   val xname: token list -> xstring * token list
   val text: token list -> string * token list
+  val uname: token list -> string option * token list
   val comment: token list -> Comment.text * token list
   val marg_comment: token list -> Comment.text * token list
   val interest: token list -> Comment.interest * token list
@@ -172,6 +173,8 @@
 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 uname = underscore >> K None || name >> Some;
+
 
 (* formal comments *)
 
@@ -303,6 +306,13 @@
 
 (* locale elements *)
 
+(* FIXME
+fun expr2 x = (xname >> Locale.Locale || $$$ "(" |-- !!! (expr0 --| $$$ ")")) x
+and expr1 x = (expr2 -- Scan.repeat1 uname >> Locale.Rename || expr2) x
+and expr0 x = (enum1 "+" expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
+*)
+val expr0 = xname;
+
 val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K None || opt_mixfix >> Some;
 
 val locale_element = group "locale element"
@@ -313,7 +323,7 @@
   $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
     >> Locale.Defines ||
   $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1)) >> Locale.Notes ||
-  $$$ "uses" |-- !!! xname >> (Locale.Uses o Locale.Locale));
+  $$$ "uses" |-- !!! expr0 >> (Locale.Uses o Locale.Locale));
 
 
 (* proof methods *)