src/Pure/General/symbol_pos.ML
changeset 48743 a72f8ffecf31
parent 43947 9b00f09f7721
child 48764 4fe0920d5049
     1.1 --- a/src/Pure/General/symbol_pos.ML	Thu Aug 09 14:09:36 2012 +0200
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Aug 09 14:37:43 2012 +0200
     1.3 @@ -19,6 +19,9 @@
     1.4    val scan_string_q: T list -> (Position.T * (T list * Position.T)) * T list
     1.5    val scan_string_qq: T list -> (Position.T * (T list * Position.T)) * T list
     1.6    val scan_string_bq: T list -> (Position.T * (T list * Position.T)) * T list
     1.7 +  val recover_string_q: T list -> T list * T list
     1.8 +  val recover_string_qq: T list -> T list * T list
     1.9 +  val recover_string_bq: T list -> T list * T list
    1.10    val quote_string_q: string -> string
    1.11    val quote_string_qq: string -> string
    1.12    val quote_string_bq: string -> string
    1.13 @@ -26,6 +29,7 @@
    1.14      T list -> T list * T list
    1.15    val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
    1.16      T list -> T list * T list
    1.17 +  val recover_comment: T list -> T list * T list
    1.18    val source: Position.T -> (Symbol.symbol, 'a) Source.source ->
    1.19      (T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source
    1.20    type text = string
    1.21 @@ -98,12 +102,19 @@
    1.22    (scan_pos --| $$$ q) -- !!! (fn () => "missing quote at end of string")
    1.23      (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- scan_pos)));
    1.24  
    1.25 +fun recover_strs q =
    1.26 +  $$$ q @@@ (Scan.repeat (Scan.permissive (scan_str q)) >> flat);
    1.27 +
    1.28  in
    1.29  
    1.30  val scan_string_q = scan_strs "'";
    1.31  val scan_string_qq = scan_strs "\"";
    1.32  val scan_string_bq = scan_strs "`";
    1.33  
    1.34 +val recover_string_q = recover_strs "'";
    1.35 +val recover_string_qq = recover_strs "\"";
    1.36 +val recover_string_bq = recover_strs "`";
    1.37 +
    1.38  end;
    1.39  
    1.40  
    1.41 @@ -140,7 +151,9 @@
    1.42    Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) ||
    1.43    Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s)) >> single;
    1.44  
    1.45 -val scan_body = change_prompt (Scan.pass 0 (Scan.repeat scan_cmt >> flat));
    1.46 +val scan_cmts = Scan.pass 0 (Scan.repeat scan_cmt >> flat);
    1.47 +
    1.48 +val scan_body = change_prompt scan_cmts;
    1.49  
    1.50  in
    1.51  
    1.52 @@ -150,6 +163,9 @@
    1.53  fun scan_comment_body cut =
    1.54    $$$ "(" |-- $$$ "*" |-- cut "missing end of comment" (scan_body --| $$$ "*" --| $$$ ")");
    1.55  
    1.56 +val recover_comment =
    1.57 +  $$$ "(" @@@ $$$ "*" @@@ scan_cmts;
    1.58 +
    1.59  end;
    1.60  
    1.61