src/Pure/General/symbol_pos.ML
changeset 55033 8e8243975860
parent 54732 b01bb3d09928
child 55035 68afbb5ce4ff
     1.1 --- a/src/Pure/General/symbol_pos.ML	Fri Jan 17 20:51:36 2014 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Sat Jan 18 19:15:12 2014 +0100
     1.3 @@ -13,6 +13,7 @@
     1.4    val $$$ : Symbol.symbol -> T list -> T list * T list
     1.5    val ~$$$ : Symbol.symbol -> T list -> T list * T list
     1.6    val content: T list -> string
     1.7 +  val range: T list -> Position.range
     1.8    val is_eof: T -> bool
     1.9    val stopper: T Scan.stopper
    1.10    val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
    1.11 @@ -27,6 +28,12 @@
    1.12    val quote_string_q: string -> string
    1.13    val quote_string_qq: string -> string
    1.14    val quote_string_bq: string -> string
    1.15 +  val scan_cartouche: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    1.16 +    T list -> T list * T list
    1.17 +  val scan_cartouche_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    1.18 +    T list -> T list * T list
    1.19 +  val recover_cartouche: T list -> T list * T list
    1.20 +  val cartouche_content: T list -> T list
    1.21    val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    1.22      T list -> T list * T list
    1.23    val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    1.24 @@ -36,7 +43,6 @@
    1.25      (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
    1.26    type text = string
    1.27    val implode: T list -> text
    1.28 -  val range: T list -> Position.range
    1.29    val implode_range: Position.T -> Position.T -> T list -> text * Position.range
    1.30    val explode: text * Position.T -> T list
    1.31    val scan_ident: T list -> T list * T list
    1.32 @@ -54,6 +60,11 @@
    1.33  
    1.34  val content = implode o map symbol;
    1.35  
    1.36 +fun range (syms as (_, pos) :: _) =
    1.37 +      let val pos' = List.last syms |-> Position.advance
    1.38 +      in Position.range pos pos' end
    1.39 +  | range [] = Position.no_range;
    1.40 +
    1.41  
    1.42  (* stopper *)
    1.43  
    1.44 @@ -81,6 +92,7 @@
    1.45  
    1.46  fun change_prompt scan = Scan.prompt "# " scan;
    1.47  
    1.48 +fun $$ s = Scan.one (fn x => symbol x = s);
    1.49  fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
    1.50  fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
    1.51  
    1.52 @@ -147,6 +159,47 @@
    1.53  end;
    1.54  
    1.55  
    1.56 +(* nested text cartouches *)
    1.57 +
    1.58 +local
    1.59 +
    1.60 +val scan_cart =
    1.61 +  Scan.depend (fn (d: int) => $$ "\\<open>" >> pair (d + 1)) ||
    1.62 +  Scan.depend (fn 0 => Scan.fail | d => $$ "\\<close>" >> pair (d - 1)) ||
    1.63 +  Scan.lift (Scan.one (fn (s, _) => s <> "\\<close>" andalso Symbol.is_regular s));
    1.64 +
    1.65 +val scan_carts = Scan.pass 0 (Scan.repeat scan_cart);
    1.66 +
    1.67 +val scan_body = change_prompt scan_carts;
    1.68 +
    1.69 +in
    1.70 +
    1.71 +fun scan_cartouche cut =
    1.72 +  $$ "\\<open>" ::: cut "unclosed text cartouche" (scan_body @@@ $$$ "\\<close>");
    1.73 +
    1.74 +fun scan_cartouche_body cut =
    1.75 +  $$ "\\<open>" |-- cut "unclosed text cartouche" (scan_body --| $$ "\\<close>");
    1.76 +
    1.77 +val recover_cartouche =
    1.78 +  $$$ "\\<open>" @@@ scan_carts;
    1.79 +
    1.80 +end;
    1.81 +
    1.82 +fun cartouche_content syms =
    1.83 +  let
    1.84 +    fun err () =
    1.85 +      error ("Malformed text cartouche: " ^ quote (content syms) ^
    1.86 +        Position.here (Position.set_range (range syms)));
    1.87 +  in
    1.88 +    (case syms of
    1.89 +      ("\\<open>", _) :: rest =>
    1.90 +        (case rev rest of
    1.91 +          ("\\<close>", _) :: rrest => rev rrest
    1.92 +        | _ => err ())
    1.93 +    | _ => err ())
    1.94 +  end;
    1.95 +
    1.96 +
    1.97  (* ML-style comments *)
    1.98  
    1.99  local
   1.100 @@ -196,11 +249,6 @@
   1.101  
   1.102  val implode = implode o pad;
   1.103  
   1.104 -fun range (syms as (_, pos) :: _) =
   1.105 -      let val pos' = List.last syms |-> Position.advance
   1.106 -      in Position.range pos pos' end
   1.107 -  | range [] = Position.no_range;
   1.108 -
   1.109  fun implode_range pos1 pos2 syms =
   1.110    let val syms' = (("", pos1) :: syms @ [("", pos2)])
   1.111    in (implode syms', range syms') end;