1.1 --- a/src/Pure/General/scan.ML	Mon Jan 20 16:56:18 2014 +0100
     1.2 +++ b/src/Pure/General/scan.ML	Mon Jan 20 19:47:31 2014 +0100
     1.3 @@ -64,6 +64,7 @@
     1.4    val state: 'a * 'b -> 'a * ('a * 'b)
     1.5    val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
     1.6    val peek: ('a -> 'b -> 'c * 'd) -> 'a * 'b -> 'c * ('a * 'd)
     1.7 +  val provide: ('a -> bool) -> 'b -> ('b * 'c -> 'd * ('a * 'e)) -> 'c -> 'd * 'e
     1.8    val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
     1.9    val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
    1.10    val unlift: (unit * 'a -> 'b * ('c * 'd)) -> 'a -> 'b * 'd
    1.11 @@ -210,9 +211,11 @@
    1.12  
    1.13  fun peek scan = depend (fn st => scan st >> pair st);
    1.14  
    1.15 -fun pass st scan xs =
    1.16 -  let val (y, (_, xs')) = scan (st, xs)
    1.17 -  in (y, xs') end;
    1.18 +fun provide pred st scan xs =
    1.19 +  let val (y, (st', xs')) = scan (st, xs)
    1.20 +  in if pred st' then (y, xs') else fail () end;
    1.21 +
    1.22 +fun pass st = provide (K true) st;
    1.23  
    1.24  fun lift scan (st, xs) =
    1.25    let val (y, xs') = scan xs

     2.1 --- a/src/Pure/General/symbol_pos.ML	Mon Jan 20 16:56:18 2014 +0100
     2.2 +++ b/src/Pure/General/symbol_pos.ML	Mon Jan 20 19:47:31 2014 +0100
     2.3 @@ -29,8 +29,6 @@
     2.4    val quote_string_bq: string -> string
     2.5    val scan_cartouche: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
     2.6      T list -> T list * T list
     2.7 -  val scan_cartouche_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
     2.8 -    T list -> T list * T list
     2.9    val recover_cartouche: T list -> T list * T list
    2.10    val cartouche_content: T list -> T list
    2.11    val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    2.12 @@ -162,29 +160,20 @@
    2.13  
    2.14  (* nested text cartouches *)
    2.15  
    2.16 -local
    2.17 -
    2.18 -val scan_cart =
    2.19 -  Scan.depend (fn (d: int) => $$ "\\<open>" >> pair (d + 1)) ||
    2.20 -  Scan.depend (fn 0 => Scan.fail | d => $$ "\\<close>" >> pair (d - 1)) ||
    2.21 -  Scan.lift (Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.is_regular s));
    2.22 -
    2.23 -val scan_carts = Scan.pass 0 (Scan.repeat scan_cart);
    2.24 -
    2.25 -val scan_body = change_prompt scan_carts;
    2.26 -
    2.27 -in
    2.28 +val scan_cartouche_depth =
    2.29 +  Scan.repeat1 (Scan.depend (fn (d: int) =>
    2.30 +    $$ "\\<open>" >> pair (d + 1) ||
    2.31 +      (if d > 0 then
    2.32 +        Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.is_regular s) >> pair d ||
    2.33 +        $$ "\\<close>" >> pair (d - 1)
    2.34 +      else Scan.fail)));
    2.35  
    2.36  fun scan_cartouche cut =
    2.37 -  $$ "\\<open>" ::: cut "unclosed text cartouche" (scan_body @@@ $$$ "\\<close>");
    2.38 +  Scan.ahead ($$ "\\<open>") |--
    2.39 +    cut "unclosed text cartouche"
    2.40 +      (change_prompt (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth));
    2.41  
    2.42 -fun scan_cartouche_body cut =
    2.43 -  $$ "\\<open>" |-- cut "unclosed text cartouche" (scan_body --| $$ "\\<close>");
    2.44 -
    2.45 -val recover_cartouche =
    2.46 -  $$$ "\\<open>" @@@ scan_carts;
    2.47 -
    2.48 -end;
    2.49 +val recover_cartouche = Scan.pass 0 scan_cartouche_depth;
    2.50  
    2.51  fun cartouche_content syms =
    2.52    let

     3.1 --- a/src/Pure/Isar/token.ML	Mon Jan 20 16:56:18 2014 +0100
     3.2 +++ b/src/Pure/Isar/token.ML	Mon Jan 20 19:47:31 2014 +0100
     3.3 @@ -336,7 +336,8 @@
     3.4  (* scan cartouche *)
     3.5  
     3.6  val scan_cartouche =
     3.7 -  Symbol_Pos.scan_pos -- (Symbol_Pos.scan_cartouche_body !!! -- Symbol_Pos.scan_pos);
     3.8 +  Symbol_Pos.scan_pos --
     3.9 +    ((Symbol_Pos.scan_cartouche !!! >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos);
    3.10  
    3.11  
    3.12  (* scan space *)