diff --git a/tests/lean/interactive/complete.lean.expected.out b/tests/lean/interactive/complete.lean.expected.out index b4875d3ad4..3ea3a9be90 100644 --- a/tests/lean/interactive/complete.lean.expected.out +++ b/tests/lean/interactive/complete.lean.expected.out @@ -1,4 +1,4 @@ {"message":"file invalidated","response":"ok","seq_num":0} -{"completions":[{"text":"foo","type":"Type"},{"text":"foo.rec","type":"Π (C : foo → Type l) (n : foo), C n"},{"text":"foo.rec_on","type":"Π (C : foo → Type l) (n : foo), C n"},{"text":"foo.induction_on","type":"∀ (C : foo → Prop) (n : foo), C n"}],"prefix":"fo","response":"ok","seq_num":6} +{"completions":[{"source":{"column":10,"line":3},"text":"foo","type":"Type"},{"source":{"column":10,"line":3},"text":"foo.induction_on","type":"∀ (C : foo → Prop) (n : foo), C n"},{"source":{"column":10,"line":3},"text":"foo.rec","type":"Π (C : foo → Type l) (n : foo), C n"},{"source":{"column":10,"line":3},"text":"foo.rec_on","type":"Π (C : foo → Type l) (n : foo), C n"}],"prefix":"fo","response":"ok","seq_num":6} {"prefix":"","response":"ok","seq_num":9} {"prefix":"","response":"ok","seq_num":13} diff --git a/tests/lean/interactive/complete_tactic.lean.expected.out b/tests/lean/interactive/complete_tactic.lean.expected.out index 2ab3dc62b6..2481ee399c 100644 --- a/tests/lean/interactive/complete_tactic.lean.expected.out +++ b/tests/lean/interactive/complete_tactic.lean.expected.out @@ -1,5 +1,5 @@ {"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"},"response":"additional_message"} -{"msg":{"caption":"","file_name":"f","pos_col":52,"pos_line":5,"severity":"error","text":"invalid expression, unexpected token"},"response":"additional_message"} +{"msg":{"caption":"","file_name":"f","pos_col":66,"pos_line":5,"severity":"error","text":"invalid expression, unexpected token"},"response":"additional_message"} {"message":"file invalidated","response":"ok","seq_num":0} {"prefix":"","response":"ok","seq_num":2} {"prefix":"","response":"ok","seq_num":5} diff --git a/tests/lean/interactive/complete_trailing_period.lean.expected.out b/tests/lean/interactive/complete_trailing_period.lean.expected.out index 38344ce6e7..43df7ccedc 100644 --- a/tests/lean/interactive/complete_trailing_period.lean.expected.out +++ b/tests/lean/interactive/complete_trailing_period.lean.expected.out @@ -1,2 +1,2 @@ {"message":"file invalidated","response":"ok","seq_num":0} -{"completions":[{"text":"foo.rec","type":"Π (C : foo → Type l) (n : foo), C n"},{"text":"foo.rec_on","type":"Π (C : foo → Type l) (n : foo), C n"},{"text":"foo.induction_on","type":"∀ (C : foo → Prop) (n : foo), C n"},{"text":"foo","type":"Type"}],"prefix":"foo.","response":"ok","seq_num":6} +{"completions":[{"source":{"column":10,"line":3},"text":"foo.induction_on","type":"∀ (C : foo → Prop) (n : foo), C n"},{"source":{"column":10,"line":3},"text":"foo.rec","type":"Π (C : foo → Type l) (n : foo), C n"},{"source":{"column":10,"line":3},"text":"foo.rec_on","type":"Π (C : foo → Type l) (n : foo), C n"},{"source":{"column":10,"line":3},"text":"foo","type":"Type"}],"prefix":"foo.","response":"ok","seq_num":6}