diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_rsyntax.ml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml index d4e56c86b..03f9fcbc6 100644 --- a/parsing/g_rsyntax.ml +++ b/parsing/g_rsyntax.ml @@ -65,6 +65,17 @@ let r_printer std_pr p = | Some i -> [< 'sTR (string_of_int (i+1)) >] | None -> std_pr (replace_plus p) +let r_printer_outside std_pr p = + let (_,ast1,astp,_) = get_r_sign dummy_loc in + match (int_of_r p) with + | Some i -> [< 'sTR "``"; 'sTR (string_of_int (i+1)); 'sTR "``" >] + | None -> std_pr (replace_plus p) let _ = Esyntax.Ppprim.add ("r_printer", r_printer) +let _ = Esyntax.Ppprim.add ("r_printer_outside", r_printer_outside) + + + + + |