From dbbacb3bfd9a58a4b2596fa4a63287b69d26ba53 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 17 Jun 2020 18:10:10 -0700 Subject: [PATCH] chore: remove comment from `Linter` Old frontend is just providing `Syntax.missing` --- src/Lean/Linter.lean | 2 +- src/frontends/lean/definition_cmds.cpp | 2 +- tests/plugin/SnakeLinter.lean | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Linter.lean b/src/Lean/Linter.lean index 0b8c74d0ca..323bb26d14 100644 --- a/src/Lean/Linter.lean +++ b/src/Lean/Linter.lean @@ -11,7 +11,7 @@ import Lean.Message namespace Lean -def Linter := Environment → Name → /-Syntax → -/IO MessageLog +def Linter := Environment → Name → Syntax → IO MessageLog def mkLintersRef : IO (IO.Ref (Array Linter)) := IO.mkRef #[] diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 686d196ca6..81d3a5b569 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -480,7 +480,7 @@ static environment elab_single_def(parser & p, decl_cmd_kind const & kind, cmd_m lean_assert(io_result_is_ok(r.raw())); array_ref linters(io_result_get_value(r.raw()), true); for (object * const & linter : linters) { - object * r2 = apply_3(linter, new_env.to_obj_arg(), local_name_p(fn).to_obj_arg(), io_mk_world()); + object * r2 = apply_4(linter, new_env.to_obj_arg(), local_name_p(fn).to_obj_arg(), lean_box(0) /* Syntax.missing */, io_mk_world()); consume_io_result(r2); } diff --git a/tests/plugin/SnakeLinter.lean b/tests/plugin/SnakeLinter.lean index 656f3aef42..6be20fad34 100644 --- a/tests/plugin/SnakeLinter.lean +++ b/tests/plugin/SnakeLinter.lean @@ -5,7 +5,7 @@ open Lean def oh_no : Nat := 0 def snakeLinter : Linter := -fun env n => +fun env n stx => -- TODO(Sebastian): return actual message with position from syntax tree if n.toString.contains '_' then throw $ IO.userError "SNAKES!!" else pure MessageLog.empty