# HG changeset patch
# User wenzelm
# Date 1445541387 -7200
# Node ID 760e21900b014cefbdf4ad84fdab0e2b629eb836
# Parent  42afc789add83f8cfab7dd8cb1adfb6101e6a1a9
clarified scan_cartouche_depth (amending 8284c0d5bf52): finish after outermost cartouche;

diff -r 42afc789add8 -r 760e21900b01 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Wed Oct 21 19:23:14 2015 +0200
+++ b/src/Pure/General/symbol_pos.ML	Thu Oct 22 21:16:27 2015 +0200
@@ -162,19 +162,22 @@
 (* nested text cartouches *)
 
 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.not_eof s) >> pair d ||
-        $$ "\\<close>" >> pair (d - 1)
-      else Scan.fail)));
+  Scan.repeat1 (Scan.depend (fn (depth: int option) =>
+    (case depth of
+      SOME d =>
+        $$ "\\<open>" >> pair (SOME (d + 1)) ||
+          (if d > 0 then
+            Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.not_eof s) >> pair depth ||
+            $$ "\\<close>" >> pair (if d = 1 then NONE else SOME (d - 1))
+          else Scan.fail)
+    | NONE => Scan.fail)));
 
 fun scan_cartouche err_prefix =
   Scan.ahead ($$ "\\<open>") |--
     !!! (fn () => err_prefix ^ "unclosed text cartouche")
-      (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth);
+      (Scan.provide is_none (SOME 0) scan_cartouche_depth);
 
-val recover_cartouche = Scan.pass 0 scan_cartouche_depth;
+val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth;
 
 fun cartouche_content syms =
   let