diff --git a/examples/wip.rs b/examples/wip.rs index 85c7230..e12dd7c 100644 --- a/examples/wip.rs +++ b/examples/wip.rs @@ -1,8 +1,7 @@ verus! { -fn get<'a>(&'a self) -> (o: Option<&'a V>) { +fn get<'a>(&'a self, k: &K) -> (o: Option<&'a V>) { a } - } // verus! diff --git a/src/lib.rs b/src/lib.rs index 58830cb..bee4694 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -517,7 +517,9 @@ fn to_doc<'a>( //*************************// // Names, Paths and Macros // //*************************// - Rule::name | Rule::name_ref | Rule::lifetime => s, + Rule::name | Rule::name_ref => s, + Rule::lifetime => s.append(arena.space()), + Rule::lifetime_no_space => s, Rule::path => map_to_doc(ctx, arena, pair), Rule::path_segment => map_to_doc(ctx, arena, pair), Rule::generic_arg_list => map_to_doc(ctx, arena, pair), diff --git a/src/verus.pest b/src/verus.pest index 49ba5db..a294907 100644 --- a/src/verus.pest +++ b/src/verus.pest @@ -366,6 +366,7 @@ name = { identifier | self_str } name_ref = { identifier | self_str | super_str | crate_str | Self_str } lifetime = { lifetime_ident } +lifetime_no_space = { lifetime } // A lifetime that shouldn't be followed by a space path = { (path_segment ~ colons_str)* ~ path_segment } @@ -402,7 +403,7 @@ assoc_type_arg = { } lifetime_arg = { - lifetime + lifetime_no_space } const_arg = { @@ -739,7 +740,7 @@ const_param = { } lifetime_param = { - attr* ~ lifetime ~ (colon_str ~ type_bound_list)? + attr* ~ lifetime_no_space ~ (colon_str ~ type_bound_list)? } where_clause = { @@ -747,7 +748,7 @@ where_clause = { } where_pred = { - (for_str ~ generic_param_list)? ~ (lifetime | type) ~ colon_str ~ type_bound_list? + (for_str ~ generic_param_list)? ~ (lifetime_no_space | type) ~ colon_str ~ type_bound_list? } visibility = { @@ -1102,7 +1103,7 @@ while_expr = { } label = { - lifetime ~ colon_str + lifetime_no_space ~ colon_str } break_expr = { @@ -1254,7 +1255,7 @@ type_bound_list = { } type_bound = { - lifetime + lifetime_no_space | ("?" | "~" ~ const_str)? ~ type } diff --git a/tests/snap-tests.rs b/tests/snap-tests.rs index 2554058..1a1b5f3 100644 --- a/tests/snap-tests.rs +++ b/tests/snap-tests.rs @@ -824,7 +824,7 @@ fn get<'a>(&'a self, k: &K) -> (o: Option<&'a V>) { assert_snapshot!(parse_and_format(file).unwrap(), @r###" verus! { - fn get<'a>(&'aself, k: &K) -> (o: Option<&'aV>) { + fn get<'a>(&'a self, k: &K) -> (o: Option<&'a V>) { a }