src/Pure/General/symbol_pos.ML
changeset 55104 8284c0d5bf52
parent 55103 57d87ec3da4c
child 55105 75815b3b38a1
     1.1 --- a/src/Pure/General/symbol_pos.ML	Mon Jan 20 16:56:18 2014 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Mon Jan 20 19:47:31 2014 +0100
     1.3 @@ -29,8 +29,6 @@
     1.4    val quote_string_bq: string -> string
     1.5    val scan_cartouche: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
     1.6      T list -> T list * T list
     1.7 -  val scan_cartouche_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
     1.8 -    T list -> T list * T list
     1.9    val recover_cartouche: T list -> T list * T list
    1.10    val cartouche_content: T list -> T list
    1.11    val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    1.12 @@ -162,29 +160,20 @@
    1.13  
    1.14  (* nested text cartouches *)
    1.15  
    1.16 -local
    1.17 -
    1.18 -val scan_cart =
    1.19 -  Scan.depend (fn (d: int) => $$ "\\<open>" >> pair (d + 1)) ||
    1.20 -  Scan.depend (fn 0 => Scan.fail | d => $$ "\\<close>" >> pair (d - 1)) ||
    1.21 -  Scan.lift (Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.is_regular s));
    1.22 -
    1.23 -val scan_carts = Scan.pass 0 (Scan.repeat scan_cart);
    1.24 -
    1.25 -val scan_body = change_prompt scan_carts;
    1.26 -
    1.27 -in
    1.28 +val scan_cartouche_depth =
    1.29 +  Scan.repeat1 (Scan.depend (fn (d: int) =>
    1.30 +    $$ "\\<open>" >> pair (d + 1) ||
    1.31 +      (if d > 0 then
    1.32 +        Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.is_regular s) >> pair d ||
    1.33 +        $$ "\\<close>" >> pair (d - 1)
    1.34 +      else Scan.fail)));
    1.35  
    1.36  fun scan_cartouche cut =
    1.37 -  $$ "\\<open>" ::: cut "unclosed text cartouche" (scan_body @@@ $$$ "\\<close>");
    1.38 -
    1.39 -fun scan_cartouche_body cut =
    1.40 -  $$ "\\<open>" |-- cut "unclosed text cartouche" (scan_body --| $$ "\\<close>");
    1.41 +  Scan.ahead ($$ "\\<open>") |--
    1.42 +    cut "unclosed text cartouche"
    1.43 +      (change_prompt (Scan.provide (fn d => d = 0) 0 scan_cartouche_depth));
    1.44  
    1.45 -val recover_cartouche =
    1.46 -  $$$ "\\<open>" @@@ scan_carts;
    1.47 -
    1.48 -end;
    1.49 +val recover_cartouche = Scan.pass 0 scan_cartouche_depth;
    1.50  
    1.51  fun cartouche_content syms =
    1.52    let