rzk-0.11.3: An experimental proof assistant for synthetic ∞-categories
Safe HaskellNone
LanguageHaskell2010

Rzk.Format

Description

The formatter is designed in a way that can be consumed both by the CLI and the LSP server.

Synopsis

Documentation

data FormattingEdit Source #

All indices are 1-based (as received from the lexer) Note: LSP uses 0-based indices

format :: Text -> Text Source #

Format Rzk code, returning the formatted version. Tabs are normalized to single spaces before formatting.

formatDocument :: Text -> Text Source #

Format a whole document, for a consumer that replaces it wholesale (the language server does, so that tab normalization and all formatting rules are applied instead of incremental edits to tabbed source).

The document ends in as many newlines as it began with. Formatting is a rewriting of the code, and whether a file ends in a newline is not something it has an opinion on: that is the editor's insert_final_newline and whatever else formats the surrounding Markdown. The language server used to send the document with every trailing newline stripped, which silently deleted the final one on each save and left the file failing a .editorconfig or Prettier check that no further formatting could satisfy.

formatFile :: FilePath -> IO Text Source #

Format Rzk code from a file

formatFileWrite :: FilePath -> IO () Source #

Format the file and write the result back to the file.

isWellFormatted :: Text -> Bool Source #

Check if the given Rzk source code is well formatted. This is useful for automation tasks. Tabs are normalized to single spaces before checking.

isWellFormattedFile :: FilePath -> IO Bool Source #

Same as isWellFormatted, but reads the source code from a file.

normalizeTabs :: Text -> Text Source #

Replace every tab character with a single space. Call this before formatTextEdits so that the lexer and edit positions are consistent (BNFC column counts are undefined when the source contains tabs).