Skip to content

goal_markers stops working #488

@zayn7lie

Description

@zayn7lie

In a few weeks ago, my customize goal marker worked. But now it accidentally stop working:

Image

Here is the config:

vim.pack.add({
  { src = "https://github.com/Julian/lean.nvim" },
  { src = "https://github.com/nvim-lua/plenary.nvim" },
})

vim.api.nvim_create_autocmd('BufReadPre', {
  group = vim.api.nvim_create_augroup("SetupLean", { clear = true }),
  once = true,
  callback = function()
    require('lean').setup {
      goal_markers = { accomplished = '', unsolved = '' },
      -- Enable suggested mappings?
      --
      -- false by default, true to enable
      mappings = false,

      -- Enable the Lean language server(s)?
      --
      -- false to disable, otherwise should be a table of options to pass to `leanls`
      --
      -- See :help vim.lsp.Config for details.

      ft = {
        -- A list of patterns which will be used to protect any matching
        -- Lean file paths from being accidentally modified (by marking the
        -- buffer as `nomodifiable`).
        nomodifiable = {
            -- by default, this list includes the Lean standard libraries,
            -- as well as files within dependency directories (e.g. `_target`)
            -- Set this to an empty table to disable.
        }
      },

      -- Abbreviation support
      abbreviations = {
        -- Enable expanding of unicode abbreviations?
        enable = true,
        -- additional abbreviations:
        extra = {
          -- Add a \wknight abbreviation to insert ♘
          --
          -- Note that the backslash is implied, and that you of
          -- course may also use a snippet engine directly to do
          -- this if so desired.
          wknight = '',
        },
        -- Change if you don't like the backslash
        -- (comma is a popular choice on French keyboards)
        leader = '\\',
      },

      -- Infoview support
      infoview = {
        -- Automatically open an infoview on entering a Lean buffer?
        -- Should be a function that will be called anytime a new Lean file
        -- is opened. Return true to open an infoview, otherwise false.
        -- Setting this to `true` is the same as `function() return true end`,
        -- i.e. autoopen for any Lean file, or setting it to `false` is the
        -- same as `function() return false end`, i.e. never autoopen.
        autoopen = true,

        -- Set the initial size (in columns/lines) of the infoview's window.
        -- Windows open horizontally or vertically based on available space.
        -- Values less than 1 are treated as a percentage of the current
        -- buffer's max columns or lines.
        width = 1/3,
        height = 1/3,

        -- Set the infoviews' orientation to be dynamic based on screen layout
        -- or fixed to a vertical or horizontal orientation
        -- auto | vertical | horizontal
        orientation = "auto",

        -- Put the infoview on the top or bottom when horizontal?
        -- top | bottom
        horizontal_position = "bottom",

        -- Always open the infoview window in a separate tabpage.
        -- Might be useful if you are using a screen reader and don't want too
        -- many dynamic updates in the terminal at the same time.
        -- Note that `height` and `width` will be ignored in this case.
        separate_tab = false,

        -- Show indicators for pin locations when entering an infoview window?
        -- always | never | auto (= only when there are multiple pins)
        indicators = "auto",
      },

      -- Progress bar support
      progress_bars = {
        -- Enable the progress bars?
        -- By default, this is `true` if satellite.nvim is not installed, otherwise
        -- it is turned off, as when satellite.nvim is present this information would
        -- be duplicated.
        enable = true,  -- see above for default
        -- What character should be used for the bars?
        character = '',
        -- Use a different priority for the signs
        priority = 10,
      },

      -- Redirect Lean's stderr messages somewhere (to a buffer by default)
      stderr = {
        enable = true,
        -- height of the window
        height = 5,
        -- a callback which will be called with (multi-line) stderr output
        -- e.g., use:
        --   on_lines = function(lines) vim.notify(lines) end
        -- if you want to redirect stderr to `vim.notify`.
        -- The default implementation will redirect to a dedicated stderr
        -- window.
        on_lines = nil,
      },
    }
  end,
})

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions