# HG changeset patch
# User wenzelm
# Date 1214329398 -7200
# Node ID 3945da15d410fed6f0210a93944ee0f194ea4b92
# Parent  97e2ccba3b642038df5f119e2e67d4addf002cab
added Open/Close -- checked blocks;

diff -r 97e2ccba3b64 -r 3945da15d410 src/Pure/Isar/antiquote.ML
--- a/src/Pure/Isar/antiquote.ML	Tue Jun 24 19:43:17 2008 +0200
+++ b/src/Pure/Isar/antiquote.ML	Tue Jun 24 19:43:18 2008 +0200
@@ -7,7 +7,9 @@
 
 signature ANTIQUOTE =
 sig
-  datatype antiquote = Text of string | Antiq of string * Position.T
+  datatype antiquote =
+    Text of string | Antiq of string * Position.T |
+    Open of Position.T | Close of Position.T
   val is_antiq: antiquote -> bool
   val scan_antiquotes: string * Position.T -> antiquote list
   val scan_arguments: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
@@ -21,10 +23,28 @@
 
 datatype antiquote =
   Text of string |
-  Antiq of string * Position.T;
+  Antiq of string * Position.T |
+  Open of Position.T |
+  Close of Position.T;
 
 fun is_antiq (Text _) = false
-  | is_antiq (Antiq _) = true;
+  | is_antiq _ = true;
+
+
+(* check_nesting *)
+
+fun err_unbalanced pos =
+  error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
+
+fun check_nesting antiqs =
+  let
+    fun check [] [] = ()
+      | check [] (pos :: _) = err_unbalanced pos
+      | check (Open pos :: ants) ps = check ants (pos :: ps)
+      | check (Close pos :: _) [] = err_unbalanced pos
+      | check (Close _ :: ants) (_ :: ps) = check ants ps
+      | check (_ :: ants) ps = check ants ps;
+  in check antiqs [] end;
 
 
 (* scan_antiquote *)
@@ -35,7 +55,8 @@
 
 val scan_txt =
   T.count ($$ "@" --| Scan.ahead (~$$ "{")) ||
-  T.count (Scan.one (fn s => s <> "@" andalso Symbol.is_regular s));
+  T.count (Scan.one (fn s =>
+    s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>" andalso Symbol.is_regular s));
 
 fun escape "\\" = "\\\\"
   | escape "\"" = "\\\""
@@ -56,7 +77,9 @@
 
 fun scan_antiquote (pos, ss) = (pos, ss) |>
   (Scan.repeat1 scan_txt >> (Text o implode) ||
-    scan_antiq >> (fn s => Antiq (s, pos)));
+    scan_antiq >> (fn s => Antiq (s, pos)) ||
+    T.count ($$ "\\<lbrace>") >> K (Open pos) ||
+    T.count ($$ "\\<rbrace>") >> K (Close pos));
 
 end;
 
@@ -66,7 +89,7 @@
 fun scan_antiquotes (s, pos) =
   (case Scan.error (Scan.finite' Symbol.stopper (Scan.repeat scan_antiquote))
       (pos, Symbol.explode s) of
-    (xs, (_, [])) => xs
+    (xs, (_, [])) => (check_nesting xs; xs)
   | (_, (pos', ss)) => error ("Malformed quotation/antiquotation source at: " ^
       quote (Symbol.beginning 10 ss) ^ Position.str_of pos'));