# HG changeset patch
# User schirmer
# Date 1142613518 -3600
# Node ID 4c86109423d5ace3ea70eec9f5a56bc2d89dc995
# Parent  88172041c08475da03f3f0d276cb57cd35f64ac1
added parser locale_expr_unless

diff -r 88172041c084 -r 4c86109423d5 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Fri Mar 17 16:17:38 2006 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Fri Mar 17 17:38:38 2006 +0100
@@ -85,6 +85,8 @@
   val locale_target: token list -> xstring * token list
   val opt_locale_target: token list -> xstring option * token list
   val locale_expr: token list -> Locale.expr * token list
+  val locale_expr_unless: (token list -> 'a * token list) -> 
+         token list -> Locale.expr * token list 
   val locale_keyword: token list -> string * token list
   val locale_element: token list -> Element.context Locale.element * token list
   val context_element: token list -> Element.context * token list
@@ -366,20 +368,23 @@
   $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1))
     >> Element.Notes;
 
-fun plus1 scan =
-  scan -- Scan.repeat ($$$ "+" |-- Scan.unless loc_keyword (!!! scan)) >> op ::;
+fun plus1 test scan =
+  scan -- Scan.repeat ($$$ "+" |-- Scan.unless test (!!! scan)) >> op ::;
 
 val rename = name -- Scan.option mixfix;
 
-fun expr2 x = (xname >> Locale.Locale || $$$ "(" |-- !!! (expr0 --| $$$ ")")) x
-and expr1 x = (expr2 -- Scan.repeat1 (maybe rename) >> Locale.Rename || expr2) x
-and expr0 x = (plus1 expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
-
+fun expr test =
+  let 
+    fun expr2 x = (xname >> Locale.Locale || $$$ "(" |-- !!! (expr0 --| $$$ ")")) x
+    and expr1 x = (expr2 -- Scan.repeat1 (maybe rename) >> Locale.Rename || expr2) x
+    and expr0 x = (plus1 test expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
+  in expr0 end;
 in
 
 val locale_target = ($$$ "(" -- $$$ "in") |-- !!! (xname --| $$$ ")");
 val opt_locale_target = Scan.option locale_target;
-val locale_expr = expr0;
+val locale_expr_unless = expr
+val locale_expr = expr loc_keyword;
 val locale_keyword = loc_keyword;
 
 val locale_element = group "locale element"