Update

10 files changed, 821 insertions, 63 deletions

diff --git a/README.md b/README.md
index 9498f373..65494ec0 100644
--- a/README.md
+++ b/README.md
@@ -83,7 +83,7 @@ On top of all language packs from [vim repository](https://github.com/vim/vim/tr
 - [fsharp](https://github.com/ionide/Ionide-vim) (F# syntax highlighting for fs, fsi and fsx files)
 - [gdscript](https://github.com/calviken/vim-gdscript3) (GDScript syntax highlighting for gd files)
 - [git](https://github.com/tpope/vim-git) (Git Config syntax highlighting for gitconfig files)
-- [gitignore](https://github.com/fszymanski/fzf-gitignore)
+- [gitignore](https://github.com/SirJson/fzf-gitignore)
 - [gleam](https://github.com/gleam-lang/gleam.vim) (Syntax highlighting for gleam files)
 - [glsl](https://github.com/tikhomirov/vim-glsl) (GLSL syntax highlighting for glsl, fp, frag, frg, fs and 16 more files)
 - [gmpl](https://github.com/maelvalais/gmpl.vim) (Syntax highlighting for mod files)
diff --git a/autoload/smt2.vim b/autoload/smt2.vim
deleted file mode 100644
index 1aee2635..00000000
--- a/autoload/smt2.vim
+++ /dev/null
@@ -1,34 +0,0 @@
-if polyglot#init#is_disabled(expand('<sfile>:p'), 'smt2', 'autoload/smt2.vim')
-  finish
-endif
-
-" Invokes the solver on current file
-function! smt2#RunSolver()
-    silent !clear
-    execute "!" . g:smt2_solver_command . " " . bufname("%")
-endfunction
-
-" Puts the solver's output in new split (replaces old split)
-function! smt2#RunSolverAndShowResult()
-    let output = system(g:smt2_solver_command . " " . bufname("%") . " 2>&1")
-
-    " Create split (or reuse existent)
-    if exists("s:outputbufnr") && bufwinnr(s:outputbufnr) > 0
-        execute bufwinnr(s:outputbufnr) . 'wincmd w'
-    else
-        silent! vnew
-        let s:outputbufnr=bufnr('%')
-    endif
-
-    " Clear & (re-)fill contents
-    silent! normal! ggdG
-    setlocal filetype=smt2 buftype=nofile nobuflisted noswapfile
-    call append(0, split(output, '\v\n'))
-    normal! gg
-endfunction
-
-" Requests the solver's version
-function! smt2#PrintSolverVersion()
-    silent !clear
-    execute "!" . g:smt2_solver_command . " " . g:smt2_solver_version_switch
-endfunction
diff --git a/autoload/smt2/formatter.vim b/autoload/smt2/formatter.vim
new file mode 100644
index 00000000..6a461b4c
--- /dev/null
+++ b/autoload/smt2/formatter.vim
@@ -0,0 +1,142 @@
+if polyglot#init#is_disabled(expand('<sfile>:p'), 'smt2', 'autoload/smt2/formatter.vim')
+  finish
+endif
+
+" Formatting requires a rather recent Vim version
+if !((v:version > 802) || (v:version == 802 && has("patch2725")))
+    const s:errmsg_oldvim = "Vim >= 8.2.2725 required for auto-formatting"
+
+    "Dummies
+    function! smt2#formatter#FormatCurrentParagraph()
+        echoerr s:errmsg_oldvim
+    endfunction
+    function! smt2#formatter#FormatAllParagraphs()
+        echoerr s:errmsg_oldvim
+    endfunction
+
+    finish
+endif
+vim9script
+
+# ------------------------------------------------------------------------------
+# Config
+# ------------------------------------------------------------------------------
+# Length of "short" S-expressions
+if !exists("g:smt2_formatter_short_length")
+    g:smt2_formatter_short_length = 80
+endif
+
+# String to use for indentation
+if !exists("g:smt2_formatter_indent_str")
+    g:smt2_formatter_indent_str = '  '
+endif
+
+# ------------------------------------------------------------------------------
+# Formatter
+# ------------------------------------------------------------------------------
+def FitsOneLine(ast: dict<any>): bool
+    # A paragraph with several entries should not be formatted in one line
+    if ast.kind ==# 'Paragraph' && len(ast.value) != 1
+        return false
+    endif
+    return ast.pos_to - ast.pos_from < g:smt2_formatter_short_length && !ast.contains_comment
+enddef
+
+def FormatOneLine(ast: dict<any>): string
+    if ast.kind ==# 'Atom'
+        return ast.value.lexeme
+    elseif ast.kind ==# 'SExpr'
+        var formatted = []
+        for expr in ast.value
+            call formatted->add(expr->FormatOneLine())
+        endfor
+        return '(' .. formatted->join(' ') .. ')'
+    elseif ast.kind ==# 'Paragraph'
+        return ast.value[0]->FormatOneLine()
+    endif
+    throw 'Cannot format AST node: ' .. string(ast)
+    return '' # Unreachable
+enddef
+
+def Format(ast: dict<any>, indent = 0): string
+    const indent_str = repeat(g:smt2_formatter_indent_str, indent)
+
+    if ast.kind ==# 'Atom'
+        return indent_str .. ast.value.lexeme
+    elseif ast.kind ==# 'SExpr'
+        # Short expression -- avoid line breaks
+        if ast->FitsOneLine()
+            return indent_str .. ast->FormatOneLine()
+        endif
+
+        # Long expression -- break lines and indent subexpressions.
+        # Don't break before first subexpression if it's an atom
+        # Note: ast.value->empty() == false; otherwise it would fit in one line
+        var formatted = []
+        if (ast.value[0].kind ==# 'Atom')
+            call formatted->add(ast.value[0]->Format(0))
+        else
+            call formatted->add("\n" .. ast.value[0]->Format(indent + 1))
+        endif
+        for child in ast.value[1 :]
+            call formatted->add(child->Format(indent + 1))
+        endfor
+        return indent_str .. "(" .. formatted->join("\n") .. ")"
+    elseif ast.kind ==# 'Paragraph'
+        var formatted = []
+        for child in ast.value
+            call formatted->add(child->Format())
+        endfor
+        return formatted->join("\n")
+    endif
+    throw 'Cannot format AST node: ' .. string(ast)
+    return '' # Unreachable
+enddef
+
+# ------------------------------------------------------------------------------
+# Public functions
+# ------------------------------------------------------------------------------
+def smt2#formatter#FormatCurrentParagraph()
+    const cursor = getpos('.')
+    const ast = smt2#parser#ParseCurrentParagraph()
+
+    # Identify on which end of the buffer we are (to fix newlines later)
+    silent! normal! {
+    const is_first_paragraph = line('.') == 1
+    silent! normal! }
+    const is_last_paragraph = line('.') == line('$')
+
+    # Replace paragraph by formatted lines
+    const lines = split(Format(ast), '\n')
+    silent! normal! {d}
+    if is_last_paragraph && !is_first_paragraph
+        call append('.', [''] + lines)
+    else
+        call append('.', lines + [''])
+    endif
+
+    # Remove potentially introduced first empty line
+    if is_first_paragraph | silent! :1delete | endif
+
+    # Restore cursor position
+    call setpos('.', cursor)
+enddef
+
+def smt2#formatter#FormatAllParagraphs()
+    const cursor = getpos('.')
+    const asts = smt2#parser#ParseAllParagraphs()
+
+    # Clear buffer & insert formatted paragraphs
+    silent! :1,$delete
+    for ast in asts
+        const lines = split(Format(ast), '\n') + ['']
+        call append('$', lines)
+    endfor
+
+    # Remove first & trailing empty lines
+    silent! :1delete
+    silent! :$delete
+
+    # Restore cursor position
+    call setpos('.', cursor)
+enddef
diff --git a/autoload/smt2/parser.vim b/autoload/smt2/parser.vim
new file mode 100644
index 00000000..ef4068e5
--- /dev/null
+++ b/autoload/smt2/parser.vim
@@ -0,0 +1,227 @@
+if polyglot#init#is_disabled(expand('<sfile>:p'), 'smt2', 'autoload/smt2/parser.vim')
+  finish
+endif
+
+vim9script
+const debug = false
+set maxfuncdepth=100000000 # SMT files tend to be highly nested
+
+# TODO: Retry iterative parsing now that we have a scanner and simpler grammar
+# TODO: Refer to token kind by name, e.g. token_comment instead of 8
+# TODO: Change Ast.kind type from string to enum/number?
+
+# ------------------------------------------------------------------------------
+# AST nodes -- essentially named token wrappers
+#
+# Note: pos_from, pos_to and contains_comment were only introduced to allow for
+#       a fast FitsOneLine(ast) function in the formatter.
+#       Here, pos_from and pos_to refer to indices of characters -- not tokens
+# ------------------------------------------------------------------------------
+def Ast(kind: string, value: any, pos_from: number, pos_to: number, contains_comment: bool): dict<any>
+    return {kind: kind, value: value, pos_from: pos_from, pos_to: pos_to, contains_comment: contains_comment}
+enddef
+
+def ParagraphAst(exprs: list<dict<any>>, pos_from: number, pos_to: number): dict<any>
+    var contains_comment = false
+    for expr in exprs
+        if expr.contains_comment
+            contains_comment = true
+            break
+        endif
+    endfor
+    return Ast('Paragraph', exprs, pos_from, pos_to, contains_comment)
+enddef
+
+def SExprAst(exprs: list<dict<any>>, pos_from: number, pos_to: number): dict<any>
+    var contains_comment = false
+    for expr in exprs
+        if expr.contains_comment
+            contains_comment = true
+            break
+        endif
+    endfor
+    return Ast('SExpr', exprs, pos_from, pos_to, contains_comment)
+enddef
+
+def AtomAst(token: dict<any>): dict<any>
+    return Ast('Atom', token, token.pos, token.pos + len(token.lexeme), token.kind == 8)
+enddef
+
+def PrintAst(ast: dict<any>, indent = 0)
+    echo repeat(' ', indent * 2) .. '[' .. ast.kind .. '] '
+
+    if ast.kind ==# 'Atom'
+        echon ast.value.lexeme
+    elseif ast.kind ==# 'SExpr'
+        for v in ast.value
+            call PrintAst(v, indent + 1)
+        endfor
+    elseif ast.kind ==# 'Paragraph'
+        for v in ast.value
+            call PrintAst(v, indent + 1)
+        endfor
+    endif
+enddef
+
+# ------------------------------------------------------------------------------
+# Grammar
+# ------------------------------------------------------------------------------
+# Paragraph ::= Expr+
+# Expr      ::= SExpr | Atom
+# SExpr     ::= '(' Expr* ')'
+
+# ------------------------------------------------------------------------------
+# LParen
+# ------------------------------------------------------------------------------
+def AtStartOfLParen(scanner: dict<any>): bool
+    return scanner.cur_token.kind == 0 # token_lparen
+enddef
+
+def ParseLParen(scanner: dict<any>) # consumes token; no return
+    if debug
+        scanner->smt2#scanner#Enforce(scanner->AtStartOfLParen(),
+            "ParseLParen called but not at start of LParen",
+            scanner.cur_token.pos)
+    endif
+
+    scanner->smt2#scanner#NextToken()
+enddef
+
+# ------------------------------------------------------------------------------
+# RParen
+# ------------------------------------------------------------------------------
+def AtStartOfRParen(scanner: dict<any>): bool
+    return scanner.cur_token.kind == 1 # token_rparen
+enddef
+
+def ParseRParen(scanner: dict<any>) # consumes token; no return
+    if debug
+        scanner->smt2#scanner#Enforce(scanner->AtStartOfRParen(),
+            "ParseRParen called but not at start of RParen",
+            scanner.cur_token.pos)
+    endif
+
+    scanner->smt2#scanner#NextToken()
+enddef
+
+# ------------------------------------------------------------------------------
+# Atom
+# ------------------------------------------------------------------------------
+def AtStartOfAtom(scanner: dict<any>): bool
+    return 2 <= scanner.cur_token.kind && scanner.cur_token.kind <= 8
+enddef
+
+def ParseAtom(scanner: dict<any>): dict<any>
+    if debug
+        scanner->smt2#scanner#Enforce(scanner->AtStartOfAtom(),
+            "ParseAtom called but not at start of Atom",
+            scanner.cur_token.pos)
+    endif
+
+    const ast = AtomAst(scanner.cur_token)
+    scanner->smt2#scanner#NextToken()
+    return ast
+enddef
+
+# ------------------------------------------------------------------------------
+# Expr
+# ------------------------------------------------------------------------------
+def AtStartOfExpr(scanner: dict<any>): bool
+    return scanner->AtStartOfSExpr() || scanner->AtStartOfAtom()
+enddef
+def ParseExpr(scanner: dict<any>): dict<any>
+    if debug
+        scanner->smt2#scanner#Enforce(scanner->AtStartOfExpr(),
+            "ParseExpr called but not at start of Expr",
+            scanner.cur_token.pos)
+    endif
+
+    if scanner->AtStartOfSExpr()
+        return scanner->ParseSExpr()
+    endif
+    return scanner->ParseAtom()
+enddef
+
+# ------------------------------------------------------------------------------
+# SExpr
+# ------------------------------------------------------------------------------
+const AtStartOfSExpr = funcref(AtStartOfLParen)
+def ParseSExpr(scanner: dict<any>): dict<any>
+    const pos_from = scanner.cur_token.pos
+
+    if debug
+        scanner->smt2#scanner#Enforce(scanner->AtStartOfSExpr(),
+            "ParseSExpr called but not at start of SExpr",
+            pos_from)
+    endif
+    scanner->ParseLParen()
+
+    # Expr*
+    var exprs: list<any>
+    while scanner->AtStartOfExpr()
+        exprs->add(scanner->ParseExpr())
+    endwhile
+
+    scanner->smt2#scanner#Enforce(scanner->AtStartOfRParen(),
+        printf("Expected RParen but got %s", scanner.cur_token.kind->smt2#scanner#TokenKind2Str()),
+        scanner.cur_token.pos)
+    scanner->ParseRParen()
+
+    const pos_to = scanner.cur_token.pos
+    return SExprAst(exprs, pos_from, pos_to)
+enddef
+
+# ------------------------------------------------------------------------------
+# Paragraph
+# ------------------------------------------------------------------------------
+def ParseParagraph(scanner: dict<any>): dict<any>
+    const pos_from = scanner.cur_token.pos
+
+    # Expr+
+    scanner->smt2#scanner#Enforce(scanner->AtStartOfExpr(),
+        printf("Expected Expr but got %s", scanner.cur_token.kind->smt2#scanner#TokenKind2Str()),
+        pos_from)
+
+    var exprs = [scanner->ParseExpr()]
+    while scanner->AtStartOfExpr() && !scanner.at_new_paragraph
+        exprs->add(scanner->ParseExpr())
+    endwhile
+
+    const pos_to = scanner.cur_token.pos
+    return ParagraphAst(exprs, pos_from, pos_to)
+enddef
+
+# ------------------------------------------------------------------------------
+# Public functions
+# ------------------------------------------------------------------------------
+def smt2#parser#ParseCurrentParagraph(): dict<any>
+    # source = [start of current paragraph, EOF]
+    # Note: This is needed since `silent! normal! {y}` may not yank full paragraphs
+    #       in the context of multiline expressions
+    const cursor = getpos('.')
+    silent! normal! {
+    const line_offset = line('.')
+    const source = join(getline('.', '$'), "\n")
+    call setpos('.', cursor)
+
+    var scanner = smt2#scanner#Scanner(source, line_offset)
+    const ast = scanner->ParseParagraph()
+
+    if debug | ast->PrintAst() | endif
+    return ast
+enddef
+
+def smt2#parser#ParseAllParagraphs(): list<dict<any>>
+    # source = current buffer
+    const source = join(getline(1, '$'), "\n")
+
+    var scanner = smt2#scanner#Scanner(source)
+    var asts = []
+    while scanner.cur_token.kind != 9 # token_eof
+        const ast = scanner->ParseParagraph()
+        asts->add(ast)
+
+        if debug | ast->PrintAst() | endif
+    endwhile
+    return asts
+enddef
diff --git a/autoload/smt2/scanner.vim b/autoload/smt2/scanner.vim
new file mode 100644
index 00000000..464dbe24
--- /dev/null
+++ b/autoload/smt2/scanner.vim
@@ -0,0 +1,381 @@
+if polyglot#init#is_disabled(expand('<sfile>:p'), 'smt2', 'autoload/smt2/scanner.vim')
+  finish
+endif
+
+vim9script
+const debug = false
+
+# ------------------------------------------------------------------------------
+# Ref: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf
+# ------------------------------------------------------------------------------
+
+# ------------------------------------------------------------------------------
+# Token
+# ------------------------------------------------------------------------------
+const token_lparen = 0
+const token_rparen = 1
+const token_numeral = 2
+const token_decimal = 3
+const token_bv = 4
+const token_string = 5
+const token_symbol = 6
+const token_keyword = 7
+const token_comment = 8
+const token_eof = 9
+
+def Token(kind: number, pos: number, lexeme: string): dict<any>
+    return {kind: kind, pos: pos, lexeme: lexeme}
+enddef
+
+def smt2#scanner#TokenKind2Str(kind: number): string
+    if kind == token_lparen
+        return "LParen"
+    elseif kind == token_rparen
+        return "RParen"
+    elseif kind == token_numeral
+        return "Numeral"
+    elseif kind == token_decimal
+        return "Decimal"
+    elseif kind == token_bv
+        return "Bv"
+    elseif kind == token_string
+        return "String"
+    elseif kind == token_symbol
+        return "Symbol"
+    elseif kind == token_keyword
+        return "Keyword"
+    elseif kind == token_comment
+        return "Comment"
+    elseif kind == token_eof
+        return "EOF"
+    else
+        echoerr "Unexpected token kind: " .. kind
+        return ''
+    endif
+enddef
+
+def PrettyPrint(scanner: dict<any>, token: dict<any>)
+    const coord = scanner->Pos2Coord(token.pos)
+    echo printf("%4d:%-3d (%5d) %8s %s", coord.line, coord.col, token.pos, token.kind->smt2#scanner#TokenKind2Str(), token.lexeme)
+enddef
+
+# ------------------------------------------------------------------------------
+# Scanner
+#
+# Note: The public interface is limited to the
+#       - field cur_token
+#       - method NextToken
+#       - field at_new_paragraph (needed to distinguish paragraphs in parser)
+#
+#       The other fields should only be used internally / in this file
+# ------------------------------------------------------------------------------
+# TODO: Enforce restriction to ASCII? We should if we use the lookup table below
+# TODO: Do not take a string but a character stream (or just buffer and pos)?
+
+def smt2#scanner#Scanner(source: string, line_offset = 1): dict<any>
+    var scanner = {
+        chars: source->trim(" \t\n\r", 2)->split('\zs'),
+        line_offset: line_offset, # start line of source string in buffer
+        pos: 0,                   # pos in source string -- not column in line
+        at_new_paragraph: false}
+
+    if scanner.chars->empty()
+        scanner.at_eof = true
+        scanner.cur_char = ''
+    else
+        scanner.at_eof = false
+        scanner.cur_char = scanner.chars[0]
+    endif
+    scanner.cur_char_nr = scanner.cur_char->char2nr()
+    scanner.chars_len = len(scanner.chars)
+    scanner.cur_token = {}
+    scanner->smt2#scanner#NextToken()
+    return scanner
+enddef
+
+def smt2#scanner#NextToken(scanner: dict<any>)
+    if scanner.at_eof
+        scanner.cur_token = Token(token_eof, scanner.pos, '')
+    else
+        scanner->SkipWhitespace() # Cannot end up at eof since end is trimmed
+
+        const nr = scanner.cur_char_nr
+        if nr == 40 # '('
+            scanner.cur_token = Token(token_lparen, scanner.pos, '(')
+            scanner->NextPos()
+        elseif nr == 41 # ')'
+            scanner.cur_token = Token(token_rparen, scanner.pos, ')')
+            scanner->NextPos()
+        elseif nr->IsStartOfSimpleSymbol()
+            scanner.cur_token = scanner->ReadSimpleSymbol()
+        elseif nr == 124 # '|'
+            scanner.cur_token = scanner->ReadQuotedSymbol()
+        elseif nr == 58 # ':'
+            scanner.cur_token = scanner->ReadKeyword()
+        elseif nr->IsDigit()
+            scanner.cur_token = scanner->ReadNumber()
+        elseif nr == 35 # '#'
+            scanner.cur_token = scanner->ReadBv()
+        elseif nr == 34 # '"'
+            scanner.cur_token = scanner->ReadString()
+        elseif nr == 59 # ';'
+            scanner.cur_token = scanner->ReadComment()
+        else
+            scanner->smt2#scanner#Enforce(false, printf("Unexpected character '%s'", scanner.cur_char), scanner.pos)
+        endif
+    endif
+
+    if debug
+        if scanner.at_new_paragraph | echo "\n" | endif
+        scanner->PrettyPrint(scanner.cur_token)
+    endif
+enddef
+
+def NextPos(scanner: dict<any>)
+    if debug | scanner->smt2#scanner#Enforce(!scanner.at_eof, "Already at EOF", scanner.pos) | endif
+
+    scanner.pos += 1
+    scanner.at_eof = scanner.pos == scanner.chars_len
+    scanner.cur_char = scanner.at_eof ? '' : scanner.chars[scanner.pos]
+    scanner.cur_char_nr = scanner.cur_char->char2nr()
+enddef
+
+def smt2#scanner#Enforce(scanner: dict<any>, expr: bool, msg: string, pos: number)
+    if !expr
+        const coord = scanner->Pos2Coord(pos)
+        throw printf("Syntax error (at %d:%d): %s ", coord.line, coord.col, msg)
+    endif
+enddef
+
+# This is slow and intended for use in error messages & debugging only
+def Pos2Coord(scanner: dict<any>, pos: number): dict<number>
+    const line = scanner.chars[: pos]->count("\n") + scanner.line_offset
+
+    var cur_pos = pos - 1
+    while cur_pos >= 0 && scanner.chars[cur_pos] != "\n"
+        cur_pos -= 1
+    endwhile
+
+    return {line: line, col: pos - cur_pos}
+enddef
+
+# ------------------------------------------------------------------------------
+# <white_space_char> ::= 9 (tab), 10 (lf), 13 (cr), 32 (space)
+#
+# Note: The source string has all lines joined by "\n" so "\r" can be ignored
+# ------------------------------------------------------------------------------
+def SkipWhitespace(scanner: dict<any>)
+    var newlines = 0
+    while !scanner.at_eof
+        const nr = scanner.cur_char_nr
+        if nr == 32 || nr == 9
+            scanner->NextPos()
+        elseif nr == 10
+            newlines += 1
+            scanner->NextPos()
+        else
+            break
+        endif
+    endwhile
+    scanner.at_new_paragraph = newlines > 1
+enddef
+
+# ------------------------------------------------------------------------------
+# A comment is any character sequence not contained within a string literal or a
+# quoted symbol that begins with ; and ends with the first subsequent
+# line-breaking character, i.e. 10 (lf) or 13 (cr)
+#
+# Note: The source string has all lines joined by "\n" so "\r" can be ignored
+# ------------------------------------------------------------------------------
+def ReadComment(scanner: dict<any>): dict<any>
+    if debug | scanner->smt2#scanner#Enforce(scanner.cur_char == ';', "Not the start of a comment", scanner.pos) | endif
+
+    const start_pos = scanner.pos
+    scanner->NextPos()
+    while !scanner.at_eof && scanner.cur_char_nr != 10
+        scanner->NextPos()
+    endwhile
+    return Token(token_comment, start_pos, scanner.chars[start_pos : scanner.pos - 1]->join(''))
+enddef
+
+# ------------------------------------------------------------------------------
+# <numeral> ::= 0
+#             | a non-empty sequence of digits not starting with 0
+#
+# <decimal> ::= <numeral>.0*<numeral>
+# ------------------------------------------------------------------------------
+def IsDigit(char_nr: number): bool
+    # '0'->char2nr() == 48 && '9'->char2nr() == 57
+    return 48 <= char_nr && char_nr <= 57
+enddef
+
+def ReadNumber(scanner: dict<any>): dict<any>
+    if debug | scanner->smt2#scanner#Enforce(scanner.cur_char_nr->IsDigit(), "Not the start of a number", scanner.pos) | endif
+
+    const starts_with_zero = scanner.cur_char == '0'
+    const start_pos = scanner.pos
+    scanner->NextPos()
+    # Note: We aren't strict about numbers not starting with 0 when not debugging
+    if debug | scanner->smt2#scanner#Enforce(!starts_with_zero || scanner.cur_char != '0', "Numeral may not start with 0", scanner.pos) | endif
+
+    var is_decimal = false
+    while !scanner.at_eof
+        const nr = scanner.cur_char_nr
+        if 48 <= nr && nr <= 57 # inlined IsDigit
+            scanner->NextPos()
+        elseif scanner.cur_char == '.'
+            if is_decimal
+                break
+            else
+                is_decimal = true
+                scanner->NextPos()
+            endif
+        else
+            break
+        endif
+    endwhile
+    const kind = is_decimal ? token_decimal : token_numeral
+    return Token(kind, start_pos, scanner.chars[start_pos : scanner.pos - 1]->join(''))
+enddef
+
+# ------------------------------------------------------------------------------
+# <hexadecimal> ::= #x followed by a non-empty sequence of digits and letters
+#                   from A to F, capitalized or not
+#
+# <binary> ::= #b followed by a non-empty sequence of 0 and 1 characters
+# ------------------------------------------------------------------------------
+
+# Build lookup table for char->match('\m\C^[0-9a-fA-F]')
+def InitIsAlphaNumericCharNr(): list<bool>
+    var lookup_table = []
+    var char_nr = 0
+    while char_nr < 255
+        lookup_table->add(char_nr->nr2char()->match('\m\C^[0-9a-fA-F]') != -1)
+        char_nr += 1
+    endwhile
+    return lookup_table
+enddef
+const is_alphanumeric_char_nr = InitIsAlphaNumericCharNr()
+
+def ReadBv(scanner: dict<any>): dict<any>
+    if debug | scanner->smt2#scanner#Enforce(scanner.cur_char == '#', "Not the start of a bit vector literal", scanner.pos) | endif
+
+    const start_pos = scanner.pos
+    scanner->NextPos()
+    if scanner.cur_char == 'x'
+        scanner->NextPos()
+        scanner->smt2#scanner#Enforce(!scanner.at_eof && is_alphanumeric_char_nr[scanner.cur_char_nr],
+            "hexadecimal literal may not be empty",
+            scanner.pos)
+        while !scanner.at_eof && is_alphanumeric_char_nr[scanner.cur_char_nr]
+            scanner->NextPos()
+        endwhile
+    elseif scanner.cur_char == 'b'
+        scanner->NextPos()
+        # '0'->char2nr() == 48 && '1'->char2nr() == 49
+        scanner->smt2#scanner#Enforce(!scanner.at_eof && scanner.cur_char_num == 48 || scanner.cur_char_num == 49,
+            "binary literal may not be empty",
+            scanner.pos)
+        while !scanner.at_eof && scanner.cur_char_num == 48 || scanner.cur_char_num == 49
+            scanner->NextPos()
+        endwhile
+    else
+        scanner->smt2#scanner#Enforce(false, "invalid bit vector literal -- expected 'x' or 'b'", scanner.pos)
+    endif
+    return Token(token_bv, start_pos, scanner.chars[start_pos : scanner.pos - 1]->join(''))
+enddef
+
+# ------------------------------------------------------------------------------
+# <string> ::= sequence of whitespace and printable characters in double
+#              quotes with escape sequence ""
+# ------------------------------------------------------------------------------
+# TODO: Allow only printable characters, i.e. ranges [32, 126], [128-255]?
+def ReadString(scanner: dict<any>): dict<any>
+    if debug | scanner->smt2#scanner#Enforce(scanner.cur_char == '"', "Not the start of a string", scanner.pos) | endif
+
+    const start_pos = scanner.pos
+    scanner->NextPos()
+    while true
+        scanner->smt2#scanner#Enforce(!scanner.at_eof, "unexpected end of string", scanner.pos)
+
+        if scanner.cur_char == '"'
+            scanner->NextPos()
+            if scanner.cur_char != '"'
+                break
+            endif
+        endif
+        scanner->NextPos()
+    endwhile
+    return Token(token_string, start_pos, scanner.chars[start_pos : scanner.pos - 1]->join(''))
+enddef
+
+# ------------------------------------------------------------------------------
+# <simple symbol> ::= a non-empty sequence of letters, digits and the characters
+#                     + - / * = % ? ! . $ _ ~ & ^ < > @ that does not start with
+#                     a digit
+# ------------------------------------------------------------------------------
+
+# Build lookup table for char->match('\m\C^[a-zA-Z0-9+-/*=%?!.$_~&^<>@]')
+def InitIsSimpleSymbolCharNr(): list<bool>
+    var lookup_table = []
+    var char_nr = 0
+    while char_nr < 255
+        lookup_table->add(char_nr->nr2char()->match('\m\C^[a-zA-Z0-9+-/*=%?!.$_~&^<>@]') != -1)
+        char_nr += 1
+    endwhile
+    return lookup_table
+enddef
+const is_simple_symbol_char_nr = InitIsSimpleSymbolCharNr()
+
+def IsStartOfSimpleSymbol(char_nr: number): bool
+    # '0'->char2nr() == 48 && '9'->char2nr() == 57
+    return is_simple_symbol_char_nr[char_nr] && !(48 <= char_nr && char_nr <= 57)
+enddef
+
+def ReadSimpleSymbol(scanner: dict<any>): dict<any>
+    if debug | scanner->smt2#scanner#Enforce(scanner.cur_char_nr->IsStartOfSimpleSymbol(), "Not the start of a simple symbol", scanner.pos) | endif
+
+    const start_pos = scanner.pos
+    scanner->NextPos()
+    while !scanner.at_eof && is_simple_symbol_char_nr[scanner.cur_char_nr]
+        scanner->NextPos()
+    endwhile
+    return Token(token_symbol, start_pos, scanner.chars[start_pos : scanner.pos - 1]->join(''))
+enddef
+
+# ------------------------------------------------------------------------------
+# <symbol> ::= <simple symbol>
+#            | a sequence of whitespace and printable characters that starts
+#              and ends with '|' and does not otherwise include '|' or '\'
+# ------------------------------------------------------------------------------
+# TODO: Allow only printable characters, i.e. ranges [32, 126], [128-255]?
+def ReadQuotedSymbol(scanner: dict<any>): dict<any>
+    if debug | scanner->smt2#scanner#Enforce(scanner.cur_char == '|', "Not the start of a quoted symbol", scanner.pos) | endif
+
+    const start_pos = scanner.pos
+    scanner->NextPos()
+    while true
+        scanner->smt2#scanner#Enforce(!scanner.at_eof, "unexpected end of quoted symbol", scanner.pos)
+        scanner->smt2#scanner#Enforce(scanner.cur_char != '\\', "quoted symbol may not contain '\'", scanner.pos)
+        if scanner.cur_char == '|'
+            break
+        endif
+        scanner->NextPos()
+    endwhile
+    scanner->NextPos()
+    return Token(token_symbol, start_pos, scanner.chars[start_pos : scanner.pos - 1]->join(''))
+enddef
+
+# ------------------------------------------------------------------------------
+# <keyword> ::= :<simple symbol>
+# ------------------------------------------------------------------------------
+def ReadKeyword(scanner: dict<any>): dict<any>
+    if debug | scanner->smt2#scanner#Enforce(scanner.cur_char == ':', "Not the start of a keyword", scanner.pos) | endif
+
+    const start_pos = scanner.pos
+    scanner->NextPos()
+    while !scanner.at_eof && is_simple_symbol_char_nr[scanner.cur_char_nr]
+        scanner->NextPos()
+    endwhile
+    return Token(token_keyword, start_pos, scanner.chars[start_pos : scanner.pos - 1]->join(''))
+enddef
diff --git a/autoload/smt2/solver.vim b/autoload/smt2/solver.vim
new file mode 100644
index 00000000..39e7d477
--- /dev/null
+++ b/autoload/smt2/solver.vim
@@ -0,0 +1,56 @@
+if polyglot#init#is_disabled(expand('<sfile>:p'), 'smt2', 'autoload/smt2/solver.vim')
+  finish
+endif
+
+" ------------------------------------------------------------------------------
+" Config
+" ------------------------------------------------------------------------------
+" If no command for invoking a solver is specified in ~/.vimrc, test if either
+" 'z3' or 'boolector' is accessible through $PATH (in that order)
+if !exists("g:smt2_solver_command")
+    if executable("z3")
+        let g:smt2_solver_command = "z3"
+    elseif executable("boolector")
+        let g:smt2_solver_command = "boolector"
+    endif
+endif
+
+" If no command line switch for printing the solver's version is specified in
+" ~/.vimrc, use '--version'
+if !exists("g:smt2_solver_version_switch")
+    let g:smt2_solver_version_switch = "--version"
+endif
+
+" ------------------------------------------------------------------------------
+" Public functions
+" ------------------------------------------------------------------------------
+" Invokes the solver on current file
+function! smt2#solver#Run()
+    silent !clear
+    execute "!" . g:smt2_solver_command . " " . bufname("%")
+endfunction
+
+" Puts the solver's output in new split (replaces old split)
+function! smt2#solver#RunAndShowResult()
+    let output = system(g:smt2_solver_command . " " . bufname("%") . " 2>&1")
+
+    " Create split (or reuse existent)
+    if exists("s:outputbufnr") && bufwinnr(s:outputbufnr) > 0
+        execute bufwinnr(s:outputbufnr) . 'wincmd w'
+    else
+        silent! vnew
+        let s:outputbufnr=bufnr('%')
+    endif
+
+    " Clear & (re-)fill contents
+    silent! normal! ggdG
+    setlocal filetype=smt2 buftype=nofile nobuflisted noswapfile
+    call append(0, split(output, '\v\n'))
+    normal! gg
+endfunction
+
+" Requests the solver's version
+function! smt2#solver#PrintVersion()
+    silent !clear
+    execute "!" . g:smt2_solver_command . " " . g:smt2_solver_version_switch
+endfunction
diff --git a/extras/filetype.vim b/extras/filetype.vim
index 26c15db3..e6ab472f 100644
--- a/extras/filetype.vim
+++ b/extras/filetype.vim
@@ -1496,7 +1496,7 @@ au BufNewFile,BufRead *.sass			setf sass
 au BufNewFile,BufRead *.sa			setf sather
 
 " Scala
-au BufNewFile,BufRead *.scala			setf scala
+au BufNewFile,BufRead *.scala,*.sc		setf scala
 
 " SBT - Scala Build Tool
 au BufNewFile,BufRead *.sbt			setf sbt
diff --git a/ftplugin/dhall.vim b/ftplugin/dhall.vim
index a484585b..9a662090 100644
--- a/ftplugin/dhall.vim
+++ b/ftplugin/dhall.vim
@@ -33,7 +33,7 @@ endif
 function! DhallFormat()
     let cursor = getpos('.')
     exec 'normal! gg'
-    exec 'silent !dhall format --inplace ' . expand('%')
+    exec 'silent !dhall format ' . expand('%')
     exec 'e'
     call setpos('.', cursor)
 endfunction
diff --git a/ftplugin/julia.vim b/ftplugin/julia.vim
index 785ffa2a..39126598 100644
--- a/ftplugin/julia.vim
+++ b/ftplugin/julia.vim
@@ -39,7 +39,7 @@ if exists("loaded_matchit")
   " for nested-structures-skipping to work properly
   " note: 'mutable struct' and 'struct' are defined separately because
   " using \? puts the cursor on 'struct' instead of 'mutable' for some reason
-  let b:julia_begin_keywords = '\%(\%(\.\s*\)\@<!\|\%(@\s*.\s*\)\@<=\)\<\%(function\|macro\|begin\|mutable\s\+struct\|\%(mutable\s\+\)\@<!struct\|\%(abstract\|primitive\)\s\+type\|let\|do\|\%(bare\)\?module\|quote\|if\|for\|while\|try\)\>'
+  let b:julia_begin_keywords = '\%(\.\s*\|@\)\@<!\<\%(function\|macro\|begin\|mutable\s\+struct\|\%(mutable\s\+\)\@<!struct\|\%(abstract\|primitive\)\s\+type\|let\|do\|\%(bare\)\?module\|quote\|if\|for\|while\|try\)\>'
   " note: the following regex not only recognizes macros, but also local/global keywords.
   " the purpose is recognizing things like `@inline myfunction()`
   " or `global myfunction(...)` etc, for matchit and block movement functionality
@@ -67,7 +67,7 @@ if exists("loaded_matchit")
     call cursor(l, c)
     if attr == 'juliaConditional'
       return b:julia_begin_keywordsm . ':\<\%(elseif\|else\)\>:' . b:julia_end_keywords
-    elseif attr =~ '\<\%(juliaRepeat\|juliaRepKeyword\)\>'
+    elseif attr =~# '\<\%(juliaRepeat\|juliaRepKeyword\)\>'
       return b:julia_begin_keywordsm . ':\<\%(break\|continue\)\>:' . b:julia_end_keywords
     elseif attr == 'juliaBlKeyword'
       return b:julia_begin_keywordsm . ':' . b:julia_end_keywords
@@ -82,8 +82,8 @@ if exists("loaded_matchit")
   " we need to skip everything within comments, strings and
   " the 'begin' and 'end' keywords when they are used as a range rather than as
   " the delimiter of a block
-  let b:match_skip = 'synIDattr(synID(line("."),col("."),1),"name") =~ '
-        \ . '"\\<julia\\%(Comprehension\\%(For\\|If\\)\\|RangeKeyword\\|Comment\\%([LM]\\|Delim\\)\\|\\%([bs]\\|Shell\\|Printf\\|Doc\\)\\?String\\|StringPrefixed\\|DocStringM\\(Raw\\)\\?\\|RegEx\\|SymbolS\\?\\|Macro\\|Dotted\\)\\>"'
+  let b:match_skip = 'synIDattr(synID(line("."),col("."),0),"name") =~# '
+        \ . '"\\<julia\\%(Comprehension\\%(For\\|If\\)\\|RangeKeyword\\|Comment\\%([LM]\\|Delim\\)\\|\\%([bs]\\|Shell\\|Printf\\|Doc\\)\\?String\\|StringPrefixed\\|DocStringM\\(Raw\\)\\?\\|RegEx\\|SymbolS\\?\\|Dotted\\)\\>"'
 
   let b:undo_ftplugin = b:undo_ftplugin
         \ . " | unlet! b:match_words b:match_skip b:match_ignorecase"
diff --git a/ftplugin/smt2.vim b/ftplugin/smt2.vim
index d6cfa5ec..b8e8c46c 100644
--- a/ftplugin/smt2.vim
+++ b/ftplugin/smt2.vim
@@ -3,27 +3,13 @@ if polyglot#init#is_disabled(expand('<sfile>:p'), 'smt2', 'ftplugin/smt2.vim')
 endif
 
 setlocal iskeyword+=-,:,#,',$
+setlocal commentstring=;%s
 
-" If no command for invoking a solver is specified in ~/.vimrc, test if either
-" 'z3' or 'boolector' is accessible through $PATH (in that order)
-if !exists("g:smt2_solver_command")
-    if executable("z3")
-        let g:smt2_solver_command = "z3"
-    elseif executable("boolector")
-        let g:smt2_solver_command = "boolector"
-    endif
-endif
-
-" If no command line switch for printing the solver's version is specified in
-" ~/.vimrc, use '--version'
-if !exists("g:smt2_solver_version_switch")
-    let g:smt2_solver_version_switch = "--version"
-endif
-
-" Mappings
-nnoremap <silent> <buffer> <localleader>r :call smt2#RunSolver()<cr>
-nnoremap <silent> <buffer> <localleader>R :call smt2#RunSolverAndShowResult()<cr>
-nnoremap <silent> <buffer> <localleader>v :call smt2#PrintSolverVersion()<cr>
+" Mappings for solver functionality
+nnoremap <silent> <buffer> <localleader>r :call smt2#solver#Run()<cr>
+nnoremap <silent> <buffer> <localleader>R :call smt2#solver#RunAndShowResult()<cr>
+nnoremap <silent> <buffer> <localleader>v :call smt2#solver#PrintVersion()<cr>
 
-" Comment String
-setlocal commentstring=;%s
+" Mappings for formatting functionality
+nnoremap <silent> <buffer> <localleader>f :call smt2#formatter#FormatCurrentParagraph()<cr>
+nnoremap <silent> <buffer> <localleader>F :call smt2#formatter#FormatAllParagraphs()<cr>