src/Pure/General/symbol_pos.ML
changeset 61502 760e21900b01
parent 61476 1884c40f1539
child 61705 546e6494049f
     1.1 --- a/src/Pure/General/symbol_pos.ML	Wed Oct 21 19:23:14 2015 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Oct 22 21:16:27 2015 +0200
     1.3 @@ -162,19 +162,22 @@
     1.4  (* nested text cartouches *)
     1.5  
     1.6  val scan_cartouche_depth =
     1.7 -  Scan.repeat1 (Scan.depend (fn (d: int) =>
     1.8 -    $$ "\\<open>" >> pair (d + 1) ||
     1.9 -      (if d > 0 then
    1.10 -        Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.not_eof s) >> pair d ||
    1.11 -        $$ "\\<close>" >> pair (d - 1)
    1.12 -      else Scan.fail)));
    1.13 +  Scan.repeat1 (Scan.depend (fn (depth: int option) =>
    1.14 +    (case depth of
    1.15 +      SOME d =>
    1.16 +        $$ "\\<open>" >> pair (SOME (d + 1)) ||
    1.17 +          (if d > 0 then
    1.18 +            Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.not_eof s) >> pair depth ||
    1.19 +            $$ "\\<close>" >> pair (if d = 1 then NONE else SOME (d - 1))
    1.20 +          else Scan.fail)
    1.21 +    | NONE => Scan.fail)));
    1.22  
    1.23  fun scan_cartouche err_prefix =
    1.24    Scan.ahead ($$ "\\<open>") |--
    1.25      !!! (fn () => err_prefix ^ "unclosed text cartouche")
    1.26 -      (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth);
    1.27 +      (Scan.provide is_none (SOME 0) scan_cartouche_depth);
    1.28  
    1.29 -val recover_cartouche = Scan.pass 0 scan_cartouche_depth;
    1.30 +val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth;
    1.31  
    1.32  fun cartouche_content syms =
    1.33    let