diff --git a/tests/lean/interactive/info1.input b/tests/lean/interactive/info1.input index a67ac958d9..4fa628e206 100644 --- a/tests/lean/interactive/info1.input +++ b/tests/lean/interactive/info1.input @@ -1,2 +1,2 @@ -{"seq_num": 0, "command":"sync","file_name":"\/home\/leo\/projects\/lean\/tests\/lean\/interactive\/info1.lean","content":"def foo.f : nat \u2192 nat := \u03bb x, x\ndef bla.f : string \u2192 string := \u03bb x, x\nopen foo bla\nexample : nat :=\nf 0\n"} -{"seq_num": 1, "command":"info","file_name":"\/home\/leo\/projects\/lean\/tests\/lean\/interactive\/info1.lean","line":5,"column":0} +{"seq_num": 0, "command":"sync","file_name":"info1.lean","content":"def foo.f : nat \u2192 nat := \u03bb x, x\ndef bla.f : string \u2192 string := \u03bb x, x\nopen foo bla\nexample : nat :=\nf 0\n"} +{"seq_num": 1, "command":"info","file_name":"info1.lean","line":5,"column":0} diff --git a/tests/lean/interactive/info1.input.expected.out b/tests/lean/interactive/info1.input.expected.out index 0219ad6bcf..4c828f524e 100644 --- a/tests/lean/interactive/info1.input.expected.out +++ b/tests/lean/interactive/info1.input.expected.out @@ -1,2 +1,2 @@ {"message":"file invalidated","response":"ok","seq_num":0} -{"record":{"full-id":"foo.f","source":{"column":4,"file":"/tests/lean/interactive/info1.lean","line":1},"type":"ℕ → ℕ"},"response":"ok","seq_num":1} +{"record":{"full-id":"foo.f","source":{"column":4,"file":"info1.lean","line":1},"type":"ℕ → ℕ"},"response":"ok","seq_num":1} diff --git a/tests/lean/interactive/info2.input b/tests/lean/interactive/info2.input index 42ce2729de..cdf1210730 100644 --- a/tests/lean/interactive/info2.input +++ b/tests/lean/interactive/info2.input @@ -1,2 +1,2 @@ -{"seq_num":0,"command":"sync","file_name":"\/home\/leo\/projects\/lean\/build\/release\/param.lean","content":"section s1\nparameters {\u03b1 \u03b2 : Type}\n\nparameter [decidable_eq \u03b1]\n\nparameter [decidable_eq \u03b2]\nparameter [decidable_eq nat]\nparameter [decidable_eq nat]\n\nend s1\n"} -{"seq_num":2,"command":"sync","file_name":"\/home\/leo\/projects\/lean\/build\/release\/param.lean","content":"section s1\nparameters {\u03b1 \u03b2 : Type}\n\nparameter [decidable_eq \u03b1]\n\nparameter [decidable_eq \u03b2]\nparameter [decidable_eq nat]\n\nparameter [decidable_eq nat]\n\nend s1\n"} +{"seq_num":0,"command":"sync","file_name":"param.lean","content":"section s1\nparameters {\u03b1 \u03b2 : Type}\n\nparameter [decidable_eq \u03b1]\n\nparameter [decidable_eq \u03b2]\nparameter [decidable_eq nat]\nparameter [decidable_eq nat]\n\nend s1\n"} +{"seq_num":2,"command":"sync","file_name":"param.lean","content":"section s1\nparameters {\u03b1 \u03b2 : Type}\n\nparameter [decidable_eq \u03b1]\n\nparameter [decidable_eq \u03b2]\nparameter [decidable_eq nat]\n\nparameter [decidable_eq nat]\n\nend s1\n"}