import ViE.State
import ViE.Lsp.Lean
import ViE.Buffer.EditQueue

namespace ViE.Language.Lean.Key

open ViE

def handleInsertKey? (state : EditorState) (k : Key) : IO (Option EditorState) := do
  if !ViE.Lsp.Lean.isLeanBuffer state.getActiveBuffer then
    return none

  match state.completionPopup with
  | some _ =>
      match k with
      | Key.ctrl 'n' | Key.down =>
          return some <| ViE.Lsp.Lean.selectNextCompletion state
      | Key.ctrl 'p' | Key.up =>
          return some <| ViE.Lsp.Lean.selectPrevCompletion state
      | Key.ctrl 'y' | Key.char '\t' =>
          return some (← ViE.Lsp.Lean.acceptSelectedCompletion state)
      | Key.enter =>
          return some <| ViE.Lsp.Lean.clearCompletionPopup state.insertNewline
      | Key.esc =>
          let s' ← ViE.Buffer.EditQueue.awaitActiveInsertOps state
          return some <| ViE.Lsp.Lean.clearCompletionPopup ((s'.commitEdit.moveCursorLeft).setMode Mode.normal)
      | Key.backspace =>
          let s1 ← ViE.Buffer.EditQueue.awaitActiveInsertOps state
          let s' := s1.deleteBeforeCursor
          return some (← ViE.Lsp.Lean.requestCompletionForActiveIfRunning s')
      | Key.char c =>
          let s' := state.insertChar c
          return some (← ViE.Lsp.Lean.requestCompletionForActiveIfRunning s')
      | _ =>
          return none
  | none =>
      match k with
      | Key.ctrl 'n' =>
          return some (← ViE.Lsp.Lean.requestCompletionForActiveIfRunning state)
      | Key.ctrl 'y' =>
          return some state
      | Key.char c =>
          let s' := state.insertChar c
          return some (← ViE.Lsp.Lean.requestCompletionForActiveIfRunning s')
      | Key.backspace =>
          let s1 ← ViE.Buffer.EditQueue.awaitActiveInsertOps state
          let s' := s1.deleteBeforeCursor
          return some (← ViE.Lsp.Lean.requestCompletionForActiveIfRunning s')
      | _ =>
          return none

end ViE.Language.Lean.Key