tuned signature;
authorwenzelm
Thu Mar 31 15:42:01 2016 +0200 (2016-03-31)
changeset 627817ba8b944d093
parent 62777 596baa1a3251
child 62782 057e8dbe4326
tuned signature;
src/Pure/General/symbol_pos.ML
     1.1 --- a/src/Pure/General/symbol_pos.ML	Thu Mar 31 08:38:50 2016 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Mar 31 15:42:01 2016 +0200
     1.3 @@ -30,9 +30,10 @@
     1.4    val quote_string_q: string -> string
     1.5    val quote_string_qq: string -> string
     1.6    val quote_string_bq: string -> string
     1.7 +  val cartouche_content: T list -> T list
     1.8    val scan_cartouche: string -> T list -> T list * T list
     1.9 +  val scan_cartouche_content: string -> T list -> T list * T list
    1.10    val recover_cartouche: T list -> T list * T list
    1.11 -  val cartouche_content: T list -> T list
    1.12    val scan_comment: string -> T list -> T list * T list
    1.13    val scan_comment_body: string -> T list -> T list * T list
    1.14    val recover_comment: T list -> T list * T list
    1.15 @@ -177,6 +178,20 @@
    1.16  
    1.17  (* nested text cartouches *)
    1.18  
    1.19 +fun cartouche_content syms =
    1.20 +  let
    1.21 +    fun err () =
    1.22 +      error ("Malformed text cartouche: "
    1.23 +        ^ quote (content syms) ^ Position.here (#1 (range syms)));
    1.24 +  in
    1.25 +    (case syms of
    1.26 +      ("\<open>", _) :: rest =>
    1.27 +        (case rev rest of
    1.28 +          ("\<close>", _) :: rrest => rev rrest
    1.29 +        | _ => err ())
    1.30 +    | _ => err ())
    1.31 +  end;
    1.32 +
    1.33  val scan_cartouche_depth =
    1.34    Scan.repeat1 (Scan.depend (fn (depth: int option) =>
    1.35      (case depth of
    1.36 @@ -193,21 +208,10 @@
    1.37      !!! (fn () => err_prefix ^ "unclosed text cartouche")
    1.38        (Scan.provide is_none (SOME 0) scan_cartouche_depth);
    1.39  
    1.40 -val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth;
    1.41 +fun scan_cartouche_content err_prefix =
    1.42 +  scan_cartouche err_prefix >> cartouche_content;
    1.43  
    1.44 -fun cartouche_content syms =
    1.45 -  let
    1.46 -    fun err () =
    1.47 -      error ("Malformed text cartouche: "
    1.48 -        ^ quote (content syms) ^ Position.here (#1 (range syms)));
    1.49 -  in
    1.50 -    (case syms of
    1.51 -      ("\<open>", _) :: rest =>
    1.52 -        (case rev rest of
    1.53 -          ("\<close>", _) :: rrest => rev rrest
    1.54 -        | _ => err ())
    1.55 -    | _ => err ())
    1.56 -  end;
    1.57 +val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth;
    1.58  
    1.59  
    1.60  (* ML-style comments *)