From 39ce3d14f42bcccb5105883ad3160655f9873d8a Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Fri, 11 Apr 2025 13:16:16 +0200
Subject: [PATCH] test: make test deterministic (#7916)

---
 tests/lean/interactive/definition.lean          |  1 +
 .../interactive/definition.lean.expected.out    | 17 ++++++-----------
 2 files changed, 7 insertions(+), 11 deletions(-)

diff --git a/tests/lean/interactive/definition.lean b/tests/lean/interactive/definition.lean
index 00aeb837d5..75912ccf99 100644
--- a/tests/lean/interactive/definition.lean
+++ b/tests/lean/interactive/definition.lean
@@ -1,5 +1,6 @@
 inductive Foo where
   | foo
+--^ waitForILeans
 example : Foo :=
   let c := Foo.foo
   c
diff --git a/tests/lean/interactive/definition.lean.expected.out b/tests/lean/interactive/definition.lean.expected.out
index 3b10090a62..7a6bf7c2fd 100644
--- a/tests/lean/interactive/definition.lean.expected.out
+++ b/tests/lean/interactive/definition.lean.expected.out
@@ -1,19 +1,14 @@
 {"textDocument": {"uri": "file:///definition.lean"},
- "position": {"line": 4, "character": 2}}
+ "position": {"line": 5, "character": 2}}
 [{"targetUri": "file:///definition.lean",
   "targetSelectionRange":
   {"start": {"line": 0, "character": 10}, "end": {"line": 0, "character": 13}},
   "targetRange":
   {"start": {"line": 0, "character": 0}, "end": {"line": 1, "character": 7}},
   "originSelectionRange":
-  {"start": {"line": 4, "character": 2}, "end": {"line": 4, "character": 3}}}]
+  {"start": {"line": 5, "character": 2}, "end": {"line": 5, "character": 3}}}]
 {"textDocument": {"uri": "file:///definition.lean"},
- "position": {"line": 10, "character": 13}}
-[{"targetUri": "file:///definition.lean",
-  "targetSelectionRange":
-  {"start": {"line": 10, "character": 4}, "end": {"line": 10, "character": 5}},
-  "targetRange":
-  {"start": {"line": 10, "character": 4}, "end": {"line": 10, "character": 5}},
-  "originSelectionRange":
-  {"start": {"line": 10, "character": 13},
-   "end": {"line": 10, "character": 14}}}]
+ "position": {"line": 11, "character": 13}}
+[{"uri": "file:///definition.lean",
+  "range":
+  {"start": {"line": 11, "character": 4}, "end": {"line": 11, "character": 5}}}]