# HG changeset patch
# User wenzelm
# Date 1390243651 -3600
# Node ID 8284c0d5bf52aee806a4e48d4cff213f4efe994b
# Parent  57d87ec3da4cbbbe6bd9f011c287fa07d129828d
clarified scan_cartouche_depth, according to Scala version;
more accurate error position;

diff -r 57d87ec3da4c -r 8284c0d5bf52 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Mon Jan 20 16:56:18 2014 +0100
+++ b/src/Pure/General/scan.ML	Mon Jan 20 19:47:31 2014 +0100
@@ -64,6 +64,7 @@
   val state: 'a * 'b -> 'a * ('a * 'b)
   val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
   val peek: ('a -> 'b -> 'c * 'd) -> 'a * 'b -> 'c * ('a * 'd)
+  val provide: ('a -> bool) -> 'b -> ('b * 'c -> 'd * ('a * 'e)) -> 'c -> 'd * 'e
   val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
   val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
   val unlift: (unit * 'a -> 'b * ('c * 'd)) -> 'a -> 'b * 'd
@@ -210,9 +211,11 @@
 
 fun peek scan = depend (fn st => scan st >> pair st);
 
-fun pass st scan xs =
-  let val (y, (_, xs')) = scan (st, xs)
-  in (y, xs') end;
+fun provide pred st scan xs =
+  let val (y, (st', xs')) = scan (st, xs)
+  in if pred st' then (y, xs') else fail () end;
+
+fun pass st = provide (K true) st;
 
 fun lift scan (st, xs) =
   let val (y, xs') = scan xs
diff -r 57d87ec3da4c -r 8284c0d5bf52 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Mon Jan 20 16:56:18 2014 +0100
+++ b/src/Pure/General/symbol_pos.ML	Mon Jan 20 19:47:31 2014 +0100
@@ -29,8 +29,6 @@
   val quote_string_bq: string -> string
   val scan_cartouche: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
     T list -> T list * T list
-  val scan_cartouche_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
-    T list -> T list * T list
   val recover_cartouche: T list -> T list * T list
   val cartouche_content: T list -> T list
   val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
@@ -162,29 +160,20 @@
 
 (* nested text cartouches *)
 
-local
-
-val scan_cart =
-  Scan.depend (fn (d: int) => $$ "\\<open>" >> pair (d + 1)) ||
-  Scan.depend (fn 0 => Scan.fail | d => $$ "\\<close>" >> pair (d - 1)) ||
-  Scan.lift (Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.is_regular s));
-
-val scan_carts = Scan.pass 0 (Scan.repeat scan_cart);
-
-val scan_body = change_prompt scan_carts;
-
-in
+val scan_cartouche_depth =
+  Scan.repeat1 (Scan.depend (fn (d: int) =>
+    $$ "\\<open>" >> pair (d + 1) ||
+      (if d > 0 then
+        Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.is_regular s) >> pair d ||
+        $$ "\\<close>" >> pair (d - 1)
+      else Scan.fail)));
 
 fun scan_cartouche cut =
-  $$ "\\<open>" ::: cut "unclosed text cartouche" (scan_body @@@ $$$ "\\<close>");
-
-fun scan_cartouche_body cut =
-  $$ "\\<open>" |-- cut "unclosed text cartouche" (scan_body --| $$ "\\<close>");
+  Scan.ahead ($$ "\\<open>") |--
+    cut "unclosed text cartouche"
+      (change_prompt (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth));
 
-val recover_cartouche =
-  $$$ "\\<open>" @@@ scan_carts;
-
-end;
+val recover_cartouche = Scan.pass 0 scan_cartouche_depth;
 
 fun cartouche_content syms =
   let
diff -r 57d87ec3da4c -r 8284c0d5bf52 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Jan 20 16:56:18 2014 +0100
+++ b/src/Pure/Isar/token.ML	Mon Jan 20 19:47:31 2014 +0100
@@ -336,7 +336,8 @@
 (* scan cartouche *)
 
 val scan_cartouche =
-  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_cartouche_body !!! -- Symbol_Pos.scan_pos);
+  Symbol_Pos.scan_pos --
+    ((Symbol_Pos.scan_cartouche !!! >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos);
 
 
 (* scan space *)