XCVPXP4UBFU25NF6VQC3MEYHHH45RL2UXM5TA6O23NA64FPCCCJQC NBG3GUEJJMWS2FRJDU26KRQLA6O2YK77PDAPBMD3SKWLDTK23BVAC 6W6OJAUT3KLOXXKYR4GA3MG4ACLO2T4KX3SGD2KZDX6MYEZYTPHAC WRBKZMYVNHRWT7TTUGTDJ3TMWZB32QYW5PCLKTTVAJ2YF6OI3LTAC OHL2PRHBX74FZKWZU7IR6RSXA36PDZDROVI4AHTX4SO7VQFQ5RQQC GUD2J453E3UTRJZIEEUUJ3ZIGL72ETUXTO57XQIZ2Y3ZU3C2R55QC U45XPF3YKPXXRJ4MN24T2RV7GOL4FZKQSWX5P5I7WT4HC5XF4FHAC 5SFTBD4FW6GQPKRUJBAII5R2EZPDYG6CH57BIJD4IVZBE6JZB2ZQC let wg := state.getCurrentWorkgrouplet bounds := ViE.Window.getAllWindowBounds wg.layout (if state.windowHeight > 0 then state.windowHeight - 1 else 0) state.windowWidthlet current := bounds.find? (fun (id, _, _, _, _) => id == wg.activeWindowId)
let ws := state.getCurrentWorkspacelet bounds := ViE.Window.getAllWindowBounds ws.layout (if state.windowHeight > 0 then state.windowHeight - 1 else 0) state.windowWidthlet current := bounds.find? (fun (id, _, _, _, _) => id == ws.activeWindowId)
let wg := state.getCurrentWorkgroupmatch wg.layout.remove wg.activeWindowId with| none => { state with shouldQuit := true }| some newLayout =>state.updateCurrentWorkgroup fun wg =>let newIds := ViE.Window.getWindowIds newLayoutlet newActiveId := match newIds with| [] => 0 -- Should not happen if layout valid| h :: _ => h{ wg with layout := newLayout, activeWindowId := newActiveId }
let doClose (st : EditorState) : EditorState :=let ws := st.getCurrentWorkspacematch ws.layout.remove ws.activeWindowId with| none => { st with shouldQuit := true }| some newLayout =>st.updateCurrentWorkspace fun ws =>let newIds := ViE.Window.getWindowIds newLayoutlet newActiveId := match newIds with| [] => 0 -- Should not happen if layout valid| h :: _ => h{ ws with layout := newLayout, activeWindowId := newActiveId }let activeBuf := state.getActiveBufferlet explorerOpt := state.explorers.find? (fun (id, _) => id == activeBuf.id)match explorerOpt with| none => doClose state| some (bufId, explorer) =>let s1 := { state with explorers := state.explorers.filter (fun (id, _) => id != bufId) }let s2 :=match explorer.previewWindowId with| none => s1| some previewId =>s1.updateCurrentWorkspace fun ws =>match ws.layout.remove previewId with| some newLayout => { ws with layout := newLayout }| none => wslet s3 :=match explorer.previewBufferId with| some previewBufId => ViE.Buffer.removeBuffer s2 previewBufId| none => s2doClose s3
let s' := state.updateCurrentWorkgroup fun wg =>let activeId := wg.activeWindowIdlet nextId := wg.nextWindowIdlet currentView := wg.layout.findView activeId |>.getD initialView
let s' := state.updateCurrentWorkspace fun ws =>let activeId := ws.activeWindowIdlet nextId := ws.nextWindowIdlet currentView := ws.layout.findView activeId |>.getD initialView
| some nextId => { wg with activeWindowId := nextId }| none => { wg with activeWindowId := match ids with | [] => wg.activeWindowId | h :: _ => h }
| some nextId => { ws with activeWindowId := nextId }| none => { ws with activeWindowId := match ids with | [] => ws.activeWindowId | h :: _ => h }
let s' := currentSt.updateCurrentWorkgroup fun wg =>{ wg with buffers := wg.buffers.map (fun (b : FileBuffer) => if b.id == buf.id then updatedBuf else b) }
let s' := currentSt.updateCurrentWorkspace fun ws =>{ ws with buffers := ws.buffers.map (fun (b : FileBuffer) => if b.id == buf.id then updatedBuf else b) }
let s' := currentSt.updateCurrentWorkgroup fun wg =>{ wg with buffers := wg.buffers.map (fun (b : FileBuffer) => if b.id == buf.id then updatedBuf else b) }
let s' := currentSt.updateCurrentWorkspace fun ws =>{ ws with buffers := ws.buffers.map (fun (b : FileBuffer) => if b.id == buf.id then updatedBuf else b) }
/-- Update current workspace within the active workgroup -/def EditorState.updateCurrentWorkspace (s : EditorState) (f : WorkspaceState → WorkspaceState) : EditorState :=s.updateCurrentWorkgroup fun wg =>if h : wg.currentWorkspace < wg.workspaces.size thenlet ws := wg.workspaces[wg.currentWorkspace]!let updated := f ws{ wg with workspaces := wg.workspaces.set! wg.currentWorkspace updated }elsewg
let wg := s.getCurrentWorkgroupmatch wg.layout.findView wg.activeWindowId with| some v => wg.buffers.find? (fun b => b.id == v.bufferId) |>.getD initialBuffer
let ws := s.getCurrentWorkspacematch ws.layout.findView ws.activeWindowId with| some v => ws.buffers.find? (fun b => b.id == v.bufferId) |>.getD initialBuffer
let newBuffers := wg.buffers.map fun b => if b.id == v.bufferId then FileBuffer.clearCache (f b) else b{ wg with buffers := newBuffers }| none => wg
let newBuffers := ws.buffers.map fun b => if b.id == v.bufferId then FileBuffer.clearCache (f b) else b{ ws with buffers := newBuffers }| none => ws
def initialWorkgroupState : WorkgroupState := {name := "1"buffers := [initialBuffer]nextBufferId := 1layout := .window 0 initialView
def makeWorkspaceState (name : String) (rootPath : Option String) (nextBufId : Nat) : WorkspaceState := {name := namerootPath := rootPathbuffers := [{ initialBuffer with id := nextBufId }]nextBufferId := nextBufId + 1layout := .window 0 { initialView with bufferId := nextBufId }
buffers := [{ initialBuffer with id := nextBufId }]nextBufferId := nextBufId + 1layout := .window 0 initialViewactiveWindowId := 0nextWindowId := 1
workspaces := #[makeWorkspaceState defaultWorkspaceName none nextBufId]currentWorkspace := 0
def makeInitialWorkgroups : Array WorkgroupState :=#[initialWorkgroupState]
def makeInitialWorkgroups : Array WorkgroupState := Id.run dolet mut groups : Array WorkgroupState := #[]let mut nextBufId := 0for i in [0:10] dolet name := s!"{i}"let wg := createEmptyWorkgroup name nextBufIdgroups := groups.push wgnextBufId := nextBufId + 1groups
| Key.char 'j' => handleMotion s EditorState.moveCursorDown| Key.char 'k' => handleMotion s EditorState.moveCursorUp
| Key.char 'j' => dolet s' ← handleMotion s EditorState.moveCursorDownViE.Feature.refreshExplorerPreview s'| Key.char 'k' => dolet s' ← handleMotion s EditorState.moveCursorUpViE.Feature.refreshExplorerPreview s'
| Key.char 'p' => pure $ clearInput (EditorState.pasteBelow s)
| Key.char 'p' =>let buf := s.getActiveBufferlet isExplorer := s.explorers.any (fun (id, _) => id == buf.id)if isExplorer thenViE.Feature.toggleExplorerPreview selsepure $ clearInput (EditorState.pasteBelow s)
let next := (s.currentGroup + 1) % 10let s'' := s.switchToWorkgroup nextpure { s'' with message := s!"Switched to workgroup {next}" }
let size := s.workgroups.sizeif size == 0 thenpure s'elselet next := (s.currentGroup + 1) % sizelet s'' := s.switchToWorkgroup nextpure { s'' with message := s!"Switched to workgroup {next}" }
let prev := if s.currentGroup == 0 then 9 else s.currentGroup - 1let s'' := s.switchToWorkgroup prevpure { s'' with message := s!"Switched to workgroup {prev}" }
let size := s.workgroups.sizeif size == 0 thenpure s'elselet prev := if s.currentGroup == 0 then size - 1 else s.currentGroup - 1let s'' := s.switchToWorkgroup prevpure { s'' with message := s!"Switched to workgroup {prev}" }
| _ => pure s'
| _ =>if c.isDigit thenmatch c.toString.toNat? with| some idx =>if idx < s.workgroups.size thenlet s'' := s.switchToWorkgroup idxpure { s'' with message := s!"Switched to workgroup {idx}" }elsepure s'| none => pure s'elsepure s'
return { state withworkspace := { state.workspace with rootPath := some absPath },message := s!"Workspace path: {absPath}"}
let s' := state.updateCurrentWorkspace fun ws =>{ ws with rootPath := some absPath, name := ws.name }return { s' with message := s!"Workspace path: {absPath}" }
return { state withworkspace := { state.workspace with name := name },message := s!"Workspace renamed to: {name}"}
let trimmed := name.trimAscii.toStringif trimmed.isEmpty thenreturn { state with message := "Workspace name cannot be empty" }elselet wg := state.getCurrentWorkgrouplet currentName := state.getCurrentWorkspace.namelet duplicate := wg.workspaces.any (fun ws => ws.name == trimmed && ws.name != currentName)if duplicate thenreturn { state with message := s!"Workspace name already exists: {trimmed}" }elselet s' := state.updateCurrentWorkspace fun ws =>{ ws with name := trimmed }return { s' with message := s!"Workspace renamed to: {trimmed}" }
let current := state.workgroups[state.currentGroup]!let updated := { current with name := name }return { state withworkgroups := state.workgroups.set! state.currentGroup updated,message := s!"Workgroup renamed to: {name}"}
let trimmed := name.trimAscii.toStringif trimmed.isEmpty thenreturn { state with message := "Workgroup name cannot be empty" }elselet currentName := state.getCurrentWorkgroup.namelet duplicate := state.workgroups.any (fun wg => wg.name == trimmed && wg.name != currentName)if duplicate thenreturn { state with message := s!"Workgroup name already exists: {trimmed}" }elselet current := state.workgroups[state.currentGroup]!let updated := { current with name := trimmed }return { state withworkgroups := state.workgroups.set! state.currentGroup updated,message := s!"Workgroup renamed to: {trimmed}"}
| _ => return { state with message := "Usage: :wg <new|close|rename|next|prev|index> [args]" }
| _ => return { state with message := "Usage: :wg <new|list|close|rename|next|prev|index> [args]" }def cmdWs (args : List String) (state : EditorState) : IO EditorState :=let wg := state.getCurrentWorkgrouplet maxBufId := wg.workspaces.foldl (fun m ws => max m ws.nextBufferId) 0let resolvePath (p : String) : String :=if p.startsWith "/" then pelsematch state.getCurrentWorkspace.rootPath with| some root => root ++ "/" ++ p| none => plet parseOpenArgs (rest : List String) : Option (Option String × String) :=match rest with| ["--name", name, path] => some (some name, path)| [path, "--name", name] => some (some name, path)| [path] => some (none, path)| [name, path] => some (some name, path)| _ => nonematch args with| ["list"] =>ViE.Feature.openWorkspaceExplorer state| "open" :: rest =>match parseOpenArgs rest with| some (maybeName, path) =>let absPath := resolvePath pathlet name := maybeName.getD ((System.FilePath.fileName absPath).getD "Workspace")let newWs := makeWorkspaceState name (some absPath) maxBufIdlet newState := state.updateCurrentWorkgroup fun wg =>{ wg withworkspaces := wg.workspaces.push newWs,currentWorkspace := wg.workspaces.size}return { newState with message := s!"Opened workspace: {name} ({absPath})" }| none =>return { state with message := "Usage: :ws open [--name <name>] <path>" }| ["new"] =>let name := s!"Workspace {wg.workspaces.size}"let newWs := makeWorkspaceState name none maxBufIdlet newState := state.updateCurrentWorkgroup fun wg =>{ wg withworkspaces := wg.workspaces.push newWs,currentWorkspace := wg.workspaces.size}return { newState with message := s!"Created workspace: {name}" }| ["new", name] =>let newWs := makeWorkspaceState name none maxBufIdlet newState := state.updateCurrentWorkgroup fun wg =>{ wg withworkspaces := wg.workspaces.push newWs,currentWorkspace := wg.workspaces.size}return { newState with message := s!"Created workspace: {name}" }| ["new", name, path] =>let absPath := resolvePath pathlet newWs := makeWorkspaceState name (some absPath) maxBufIdlet newState := state.updateCurrentWorkgroup fun wg =>{ wg withworkspaces := wg.workspaces.push newWs,currentWorkspace := wg.workspaces.size}return { newState with message := s!"Created workspace: {name} ({absPath})" }| ["close"] =>if wg.workspaces.size <= 1 thenreturn { state with message := "Cannot close the last workspace" }elseif h_idx : wg.currentWorkspace < wg.workspaces.size thenlet prevIdx := if wg.currentWorkspace == 0 then wg.workspaces.size - 1 else wg.currentWorkspace - 1let newSpaces := wg.workspaces.eraseIdx wg.currentWorkspace h_idxlet newIdx := if prevIdx < newSpaces.size then prevIdx else newSpaces.size - 1let newState := state.updateCurrentWorkgroup fun wg =>{ wg with workspaces := newSpaces, currentWorkspace := newIdx }let newWs := newSpaces[newIdx]!return { newState with message := s!"Workspace closed. Switched to: {newWs.name}" }elsereturn { state with message := "Error: invalid workspace index" }| ["rename", name] =>let trimmed := name.trimAscii.toStringif trimmed.isEmpty thenreturn { state with message := "Workspace name cannot be empty" }elselet wg := state.getCurrentWorkgrouplet duplicate := wg.workspaces.any (fun ws => ws.name == trimmed)if duplicate thenreturn { state with message := s!"Workspace name already exists: {trimmed}" }elselet s' := state.updateCurrentWorkspace fun ws =>{ ws with name := trimmed }return { s' with message := s!"Workspace renamed to: {trimmed}" }| ["next"] =>let nextIdx := (wg.currentWorkspace + 1) % wg.workspaces.sizelet ws := wg.workspaces[nextIdx]!let newState := state.updateCurrentWorkgroup fun wg =>{ wg with currentWorkspace := nextIdx }return { newState with message := s!"Switched to: {ws.name}" }| ["prev"] =>let prevIdx := if wg.currentWorkspace == 0 then wg.workspaces.size - 1 else wg.currentWorkspace - 1let ws := wg.workspaces[prevIdx]!let newState := state.updateCurrentWorkgroup fun wg =>{ wg with currentWorkspace := prevIdx }return { newState with message := s!"Switched to: {ws.name}" }| [n] =>match n.toNat? with| some num =>if num < wg.workspaces.size thenlet ws := wg.workspaces[num]!let newState := state.updateCurrentWorkgroup fun wg =>{ wg with currentWorkspace := num }return { newState with message := s!"Switched to: {ws.name}" }elsereturn { state with message := s!"Workspace index out of range (0-{wg.workspaces.size - 1})" }| none => return { state with message := "Invalid workspace number" }| [] =>let ws := wg.workspaces[wg.currentWorkspace]!return { state with message := s!"Current workspace: {ws.name} (index {wg.currentWorkspace})" }| _ => return { state with message := "Usage: :ws <new|open|list|close|rename|next|prev|index> [args]" }
def previewMaxBytes : Nat := 65536def updateExplorerState (state : EditorState) (bufId : Nat) (f : ExplorerState → ExplorerState) : EditorState :={ state with explorers := state.explorers.map (fun (id, ex) => if id == bufId then (id, f ex) else (id, ex)) }def getSelectedEntry (state : EditorState) (explorer : ExplorerState) : Option FileEntry :=let cursor := state.getCursorif cursor.row < 2 thennoneelselet idx := cursor.row - 2if idx.val < explorer.entries.length thensome (explorer.entries[idx.val]!)elsenonedef ensurePreviewBuffer (state : EditorState) (explorer : ExplorerState) (entry : FileEntry) : IO (EditorState × Nat) := dolet resolved := entry.pathlet loaded ← ViE.loadPreviewBufferByteArray resolved previewMaxByteslet previewName := some s!"preview://{resolved}"let previewBuf := { loaded with filename := previewName, dirty := false }match explorer.previewBufferId with| some pid =>let ws := state.getCurrentWorkspaceif ws.buffers.any (fun b => b.id == pid) thenlet updated := { previewBuf with id := pid }let s' := state.updateCurrentWorkspace fun ws =>{ ws with buffers := ws.buffers.map (fun b => if b.id == pid then updated else b) }return (s', pid)elselet (pid, s') := ViE.Buffer.addBuffer state previewBufreturn (s', pid)| none =>let (pid, s') := ViE.Buffer.addBuffer state previewBufreturn (s', pid)def refreshExplorerPreview (state : EditorState) : IO EditorState := dolet buf := state.getActiveBufferlet explorerOpt := state.explorers.find? (fun (id, _) => id == buf.id)match explorerOpt with| none => return state| some (bufId, explorer) =>if explorer.mode != .files thenreturn statematch explorer.previewWindowId with| none => return state| some previewWinId =>match getSelectedEntry state explorer with| none => return state| some entry =>if entry.isDirectory thenreturn stateelselet (s1, previewBufId) ← ensurePreviewBuffer state explorer entrylet s2 := s1.updateCurrentWorkspace fun ws =>{ ws with layout := ws.layout.updateView previewWinId (fun v =>{ v with bufferId := previewBufId, cursor := Point.zero, scrollRow := 0, scrollCol := 0 }) }let s3 := updateExplorerState s2 bufId (fun ex => { ex with previewBufferId := some previewBufId })return s3def openExplorerDefaultPreview (state : EditorState) (bufId : Nat) (explorer : ExplorerState) : IO EditorState := doif explorer.mode != .files thenreturn statematch explorer.previewWindowId with| some _ => return state| none =>let ws := state.getCurrentWorkspacelet previewWinId := ws.nextWindowIdlet s1 := ViE.Window.splitWindow state falselet entryOpt := getSelectedEntry s1 explorerlet (s2, previewBufId) ←match entryOpt with| some entry =>if entry.isDirectory thenlet content : TextBuffer := #[#[]]let buf := { ViE.Buffer.fileBufferFromTextBuffer 0 (some "preview://") content with dirty := false }let (pid, s2) := ViE.Buffer.addBuffer s1 bufpure (s2, pid)elseensurePreviewBuffer s1 explorer entry| none =>let content : TextBuffer := #[#[]]let buf := { ViE.Buffer.fileBufferFromTextBuffer 0 (some "preview://") content with dirty := false }let (pid, s2) := ViE.Buffer.addBuffer s1 bufpure (s2, pid)let s3 := s2.updateCurrentWorkspace fun ws =>{ ws with layout := ws.layout.updateView previewWinId (fun v =>{ v with bufferId := previewBufId, cursor := Point.zero, scrollRow := 0, scrollCol := 0 }) }let s4 := updateExplorerState s3 bufId (fun ex =>{ ex with previewWindowId := some previewWinId, previewBufferId := some previewBufId })return s4def toggleExplorerPreview (state : EditorState) : IO EditorState := dolet buf := state.getActiveBufferlet explorerOpt := state.explorers.find? (fun (id, _) => id == buf.id)match explorerOpt with| none => return state| some (bufId, explorer) =>if explorer.mode != .files thenreturn { state with message := "Preview is only available in file explorer" }match explorer.previewWindowId with| some previewWinId =>let s1 := state.updateCurrentWorkspace fun ws =>match ws.layout.remove previewWinId with| some newLayout => { ws with layout := newLayout }| none => wslet s2 := updateExplorerState s1 bufId (fun ex => { ex with previewWindowId := none, previewBufferId := none })return { s2 with message := "Preview closed" }| none =>match getSelectedEntry state explorer with| none => return { state with message := "Preview: no selection" }| some entry =>if entry.isDirectory thenreturn { state with message := "Preview: directory" }elselet ws := state.getCurrentWorkspacelet previewWinId := ws.nextWindowIdlet s1 := ViE.Window.splitWindow state falselet (s2, previewBufId) ← ensurePreviewBuffer s1 explorer entrylet s3 := s2.updateCurrentWorkspace fun ws =>{ ws with layout := ws.layout.updateView previewWinId (fun v =>{ v with bufferId := previewBufId, cursor := Point.zero, scrollRow := 0, scrollCol := 0 }) }let s4 := updateExplorerState s3 bufId (fun ex => { ex with previewWindowId := some previewWinId, previewBufferId := some previewBufId })return { s4 with message := s!"Preview: {entry.name}" }
let path := if pathArg == "." || pathArg == "" then state.workspace.rootPath.getD "."else if pathArg.startsWith "/" then pathArgelse match state.workspace.rootPath with| some root => root ++ "/" ++ pathArg| none => pathArg
let ws := state.getCurrentWorkspacelet path := if pathArg == "." || pathArg == "" thenws.rootPath.getD "."else if pathArg.startsWith "/" thenpathArgelsematch ws.rootPath with| some root =>if pathArg == root then root else root ++ "/" ++ pathArg| none => pathArg
return { s''' with message := s!"Explorer: {path}" }
let s'''' := { s''' with message := s!"Explorer: {path}" }-- Auto-open preview by default for file explorerreturn (← openExplorerDefaultPreview s'''' bufferId explorerState)catch e =>return { state with message := s!"Error reading directory: {e}" }def openExplorerWithPreview (state : EditorState) (pathArg : String) (previewWindowId : Option Nat) (previewBufferId : Option Nat) : IO EditorState := dolet ws := state.getCurrentWorkspacelet path := if pathArg == "." || pathArg == "" thenws.rootPath.getD "."else if pathArg.startsWith "/" thenpathArgelsematch ws.rootPath with| some root =>if pathArg == root then root else root ++ "/" ++ pathArg| none => pathArgtrylet dirPath := System.FilePath.mk pathlet entries := (← System.FilePath.readDir dirPath).toListlet mut fileEntries : List FileEntry := []if path != "/" thenlet parentPath := match dirPath.parent with| some p => p.toString| none => "/"fileEntries := fileEntries ++ [{name := ".."path := parentPathisDirectory := true}]for entry in entries dolet entryPath := entry.path.toStringlet isDir ← entry.path.isDirfileEntries := fileEntries ++ [{name := entry.fileNamepath := entryPathisDirectory := isDir}]let sortedEntries := fileEntries.toArray.qsort fun a b =>if a.isDirectory != b.isDirectory thena.isDirectoryelsea.name < b.namelet explorerState : ExplorerState := {currentPath := pathentries := sortedEntries.toListselectedIndex := 0mode := .filespreviewWindowId := previewWindowIdpreviewBufferId := previewBufferId}
let header := [s!"Explorer: {path}", ""]let mut content := headerlet mut idx := 0for entry in explorerState.entries dolet pref := if idx == 0 then "> " else " "let icon := if entry.isDirectory then state.config.dirIcon else state.config.fileIconlet suffix := if entry.isDirectory then "/" else ""content := content ++ [s!"{pref}{icon}{entry.name}{suffix}"]idx := idx + 1let contentBuffer := content.toArray.map stringToLinelet (bufferId, s') := ViE.Buffer.createNewBuffer state contentBuffer (some s!"explorer://{path}")let s'' := { s' with explorers := (bufferId, explorerState) :: s'.explorers }let s''' := s''.updateActiveView fun v => { v with bufferId := bufferId, cursor := {row := 2, col := 0}, scrollRow := 0, scrollCol := 0 }let s'''' := { s''' with message := s!"Explorer: {path}" }match previewWindowId with| some _ => refreshExplorerPreview s''''| none => openExplorerDefaultPreview s'''' bufferId explorerState
/-- Open the workspace explorer to list workspaces. -/def openWorkspaceExplorer (state : EditorState) : IO EditorState := dolet wg := state.getCurrentWorkgrouplet mut entries : List FileEntry := []entries := entries ++ [{name := "[New Workspace]"path := ""isDirectory := false}]entries := entries ++ [{name := "[Rename Workspace]"path := ""isDirectory := false}]for ws in wg.workspaces.toList dolet label :=match ws.rootPath with| some root => s!"{ws.name} — {root}"| none => ws.nameentries := entries ++ [{name := labelpath := ws.rootPath.getD ""isDirectory := true}]let explorerState : ExplorerState := {currentPath := s!"workgroup:{wg.name}"entries := entriesselectedIndex := 0mode := .workspacespreviewWindowId := nonepreviewBufferId := none}let header := [s!"Workspace Explorer: {wg.name}", ""]let mut content := headerlet mut idx := 0for entry in explorerState.entries dolet pref := if idx == 0 then "> " else " "let mark := if idx == (wg.currentWorkspace + 1) then "* " else " "let icon := if entry.isDirectory then state.config.dirIcon else state.config.fileIconcontent := content ++ [s!"{pref}{mark}{icon}{entry.name}"]idx := idx + 1let contentBuffer := content.toArray.map stringToLinelet (bufferId, s') := ViE.Buffer.createNewBuffer state contentBuffer (some "explorer://workgroup")let s'' := { s' with explorers := (bufferId, explorerState) :: s'.explorers }let s''' := s''.updateActiveView fun v => { v with bufferId := bufferId, cursor := {row := 2, col := 0}, scrollRow := 0, scrollCol := 0 }return { s''' with message := s!"Workspace Explorer: {wg.name}" }/-- Open the workgroup explorer to list workgroups. -/def openWorkgroupExplorer (state : EditorState) : IO EditorState := dolet mut entries : List FileEntry := []entries := entries ++ [{name := "[New Workgroup]"path := ""isDirectory := false}]entries := entries ++ [{name := "[Rename Workgroup]"path := ""isDirectory := false}]for wg in state.workgroups.toList doentries := entries ++ [{name := wg.namepath := ""isDirectory := true}]let explorerState : ExplorerState := {currentPath := "workgroups"entries := entriesselectedIndex := 0mode := .workgroupspreviewWindowId := nonepreviewBufferId := none}
let header := ["Workgroup Explorer", ""]let mut content := headerlet mut idx := 0for entry in explorerState.entries dolet pref := if idx == explorerState.selectedIndex then "> " else " "let mark := if idx == (state.currentGroup + 1) then "* " else " "let icon := if entry.isDirectory then state.config.dirIcon else state.config.fileIconcontent := content ++ [s!"{pref}{mark}{icon}{entry.name}"]idx := idx + 1let contentBuffer := content.toArray.map stringToLinelet (bufferId, s') := ViE.Buffer.createNewBuffer state contentBuffer (some "explorer://workgroups")let s'' := { s' with explorers := (bufferId, explorerState) :: s'.explorers }let s''' := s''.updateActiveView fun v =>{ v with bufferId := bufferId, cursor := {row := ⟨2 + explorerState.selectedIndex⟩, col := 0}, scrollRow := 0, scrollCol := 0 }return { s''' with message := "Workgroup Explorer" }
if entry.isDirectory then-- Navigate to directoryopenExplorer state entry.pathelse-- Open fileViE.Buffer.openBuffer state entry.path
if entry.isDirectory then-- Navigate to directoryopenExplorerWithPreview state entry.path explorer.previewWindowId explorer.previewBufferIdelse-- Close preview window if it existslet s1 :=match explorer.previewWindowId with| none => state| some previewId =>let s1 := state.updateCurrentWorkspace fun ws =>match ws.layout.remove previewId with| some newLayout => { ws with layout := newLayout }| none => wslet s2 := updateExplorerState s1 buf.id (fun ex => { ex with previewWindowId := none, previewBufferId := none })match explorer.previewBufferId with| some previewBufId => ViE.Buffer.removeBuffer s2 previewBufId| none => s2-- Open fileViE.Buffer.openBuffer s1 entry.path| .workgroups =>let idx := selectedIdx.valif idx == 0 thenlet s' := { state withmode := .commandinputState := { state.inputState with commandBuffer := "wg new ", countBuffer := "", previousKey := none, pendingKeys := "" }}return { s' with message := "Workgroup name:" }else if idx == 1 thenlet current := state.getCurrentWorkgroup.namelet s' := { state withmode := .commandinputState := { state.inputState with commandBuffer := s!"wg rename {current}", countBuffer := "", previousKey := none, pendingKeys := "" }}return { s' with message := "Workgroup rename:" }elselet realIdx := idx - 2if realIdx < state.workgroups.size thenlet s' := { state with currentGroup := realIdx }let wg := s'.getCurrentWorkgroupreturn { s' with message := s!"Switched workgroup: {wg.name}" }elsereturn state| .workspaces =>let idx := selectedIdx.valif idx == 0 thenlet s' := { state withmode := .commandinputState := { state.inputState with commandBuffer := "ws new ", countBuffer := "", previousKey := none, pendingKeys := "" }}return { s' with message := "Workspace name:" }else if idx == 1 thenlet current := state.getCurrentWorkspace.namelet s' := { state withmode := .commandinputState := { state.inputState with commandBuffer := s!"ws rename {current}", countBuffer := "", previousKey := none, pendingKeys := "" }}return { s' with message := "Workspace rename:" }elselet realIdx := idx - 2let s' := state.updateCurrentWorkgroup fun wg =>if realIdx < wg.workspaces.size then{ wg with currentWorkspace := realIdx }elsewglet ws := s'.getCurrentWorkspacereturn { s' with message := s!"Switched workspace: {ws.name}" }
{ wg with buffers := buf :: wg.buffers, nextBufferId := id + 1 }let wg := s'.getCurrentWorkgroup(wg.nextBufferId - 1, s')
{ ws with buffers := buf :: ws.buffers, nextBufferId := id + 1 }let ws := s'.getCurrentWorkspace(ws.nextBufferId - 1, s')def addBuffer (state : EditorState) (buf : FileBuffer) : (Nat × EditorState) :=let s' := state.updateCurrentWorkspace fun ws =>let id := ws.nextBufferIdlet newBuf := { buf with id := id }{ ws with buffers := newBuf :: ws.buffers, nextBufferId := id + 1 }let ws := s'.getCurrentWorkspace(ws.nextBufferId - 1, s')def removeBuffer (state : EditorState) (bufId : Nat) : EditorState :=state.updateCurrentWorkspace fun ws =>{ ws with buffers := ws.buffers.filter (fun b => b.id != bufId) }
def loadPreviewBufferByteArray (filename : String) (maxBytes : Nat) : IO FileBuffer := dotrylet path := System.FilePath.mk filenameif ← path.pathExists thenif ← path.isDir thenreturn {id := 0filename := some filenamedirty := falsetable := PieceTable.fromString ""missingEol := falsecache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }}elselet data ← IO.FS.withFile filename IO.FS.Mode.read fun handle =>handle.read (USize.ofNat maxBytes)let missingEol := data.size > 0 && data[data.size - 1]! != 10let table := PieceTable.fromByteArray datareturn {id := 0filename := some filenamedirty := falsetable := tablemissingEol := missingEolcache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }}elsereturn {id := 0filename := some filenamedirty := falsetable := PieceTable.fromString ""missingEol := falsecache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }}catch _ =>return {id := 0filename := some filenamedirty := falsetable := PieceTable.fromString ""missingEol := falsecache := { lineMap := Lean.RBMap.empty, rawLineMap := Lean.RBMap.empty, lineIndexMap := Lean.RBMap.empty }}
/-- Resolve startup arguments into workspace path and filename. -/def resolveStartupTarget (filename : Option String) : IO (Option String × Option String) := domatch filename with| some path =>let filePath := System.FilePath.mk pathif ← filePath.pathExists thenif ← filePath.isDir then-- It's a directory, use as workspacepure (some path, none)else-- It's a file, use its parent directory as workspacelet parentDir := match filePath.parent with| some p => p.toString| none => "."pure (some parentDir, some path)else-- Path doesn't exist, treat as new filepure (none, some path)| none => pure (none, none)
let (workspacePath, actualFilename) ← match filename with| some path =>let filePath := System.FilePath.mk pathif ← filePath.pathExists thenif ← filePath.isDir then-- It's a directory, use as workspacepure (some path, none)else-- It's a filepure (none, some path)else-- Path doesn't exist, treat as new filepure (none, some path)| none => pure (none, none)
let (workspacePath, actualFilename) ← resolveStartupTarget filename
-- Update the first workgroup with the initial bufferlet state := state.updateCurrentWorkgroup fun wg =>{ wg with buffers := [initialBuffer] }
-- Update the first workspace with the initial buffer and root pathlet state := state.updateCurrentWorkspace fun ws =>let wsName := match workspacePath with| some path => (System.FilePath.fileName path).getD ws.name| none => ws.name{ ws withname := wsName,rootPath := workspacePath,buffers := [initialBuffer],nextBufferId := 1}
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
let rec fib n =if n <= 1 then nelse fib (n - 1) + fib (n - 2)let () =let values = List.init 16 fib inPrintf.printf "fib(0..15) = %s\n" (String.concat ", " (List.map string_of_int values))let rec fib n =if n <= 1 then nelse fib (n - 1) + fib (n - 2)let () =let values = List.init 16 fib inPrintf.printf "fib(0..15) = %s\n" (String.concat ", " (List.map string_of_int values))let rec fib n =if n <= 1 then nelse fib (n - 1) + fib (n - 2)let () =let values = List.init 16 fib inPrintf.printf "fib(0..15) = %s\n" (String.concat ", " (List.map string_of_int values))let rec fib n =if n <= 1 then nelse fib (n - 1) + fib (n - 2)let () =let values = List.init 16 fib inPrintf.printf "fib(0..15) = %s\n" (String.concat ", " (List.map string_of_int values))let rec fib n =if n <= 1 then nelse fib (n - 1) + fib (n - 2)let () =let values = List.init 16 fib inPrintf.printf "fib(0..15) = %s\n" (String.concat ", " (List.map string_of_int values))let rec fib n =if n <= 1 then nelse fib (n - 1) + fib (n - 2)let () =let values = List.init 16 fib inPrintf.printf "fib(0..15) = %s\n" (String.concat ", " (List.map string_of_int values))
module Main wherefib :: Int -> Intfib 0 = 0fib 1 = 1fib n = fib (n - 1) + fib (n - 2)main :: IO ()main = dolet values = map fib [0..15]putStrLn $ "fib(0..15) = " ++ show valuesmodule Main wherefib :: Int -> Intfib 0 = 0fib 1 = 1fib n = fib (n - 1) + fib (n - 2)main :: IO ()main = dolet values = map fib [0..15]putStrLn $ "fib(0..15) = " ++ show valuesmodule Main wherefib :: Int -> Intfib 0 = 0fib 1 = 1fib n = fib (n - 1) + fib (n - 2)main :: IO ()main = dolet values = map fib [0..15]putStrLn $ "fib(0..15) = " ++ show valuesmodule Main wherefib :: Int -> Intfib 0 = 0fib 1 = 1fib n = fib (n - 1) + fib (n - 2)main :: IO ()main = dolet values = map fib [0..15]putStrLn $ "fib(0..15) = " ++ show valuesmodule Main wherefib :: Int -> Intfib 0 = 0fib 1 = 1fib n = fib (n - 1) + fib (n - 2)main :: IO ()main = dolet values = map fib [0..15]putStrLn $ "fib(0..15) = " ++ show valuesmodule Main wherefib :: Int -> Intfib 0 = 0fib 1 = 1fib n = fib (n - 1) + fib (n - 2)main :: IO ()main = dolet values = map fib [0..15]putStrLn $ "fib(0..15) = " ++ show values
#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}
import Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sample
let rec fib n =if n <= 1 then nelse fib (n - 1) + fib (n - 2)let () =let values = List.init 16 fib inPrintf.printf "fib(0..15) = %s\n" (String.concat ", " (List.map string_of_int values))let rec fib n =if n <= 1 then nelse fib (n - 1) + fib (n - 2)let () =let values = List.init 16 fib inPrintf.printf "fib(0..15) = %s\n" (String.concat ", " (List.map string_of_int values))let rec fib n =if n <= 1 then nelse fib (n - 1) + fib (n - 2)let () =let values = List.init 16 fib inPrintf.printf "fib(0..15) = %s\n" (String.concat ", " (List.map string_of_int values))let rec fib n =if n <= 1 then nelse fib (n - 1) + fib (n - 2)let () =let values = List.init 16 fib inPrintf.printf "fib(0..15) = %s\n" (String.concat ", " (List.map string_of_int values))let rec fib n =if n <= 1 then nelse fib (n - 1) + fib (n - 2)let () =let values = List.init 16 fib inPrintf.printf "fib(0..15) = %s\n" (String.concat ", " (List.map string_of_int values))let rec fib n =if n <= 1 then nelse fib (n - 1) + fib (n - 2)let () =let values = List.init 16 fib inPrintf.printf "fib(0..15) = %s\n" (String.concat ", " (List.map string_of_int values))
module Main wherefib :: Int -> Intfib 0 = 0fib 1 = 1fib n = fib (n - 1) + fib (n - 2)main :: IO ()main = dolet values = map fib [0..15]putStrLn $ "fib(0..15) = " ++ show valuesmodule Main wherefib :: Int -> Intfib 0 = 0fib 1 = 1fib n = fib (n - 1) + fib (n - 2)main :: IO ()main = dolet values = map fib [0..15]putStrLn $ "fib(0..15) = " ++ show valuesmodule Main wherefib :: Int -> Intfib 0 = 0fib 1 = 1fib n = fib (n - 1) + fib (n - 2)main :: IO ()main = dolet values = map fib [0..15]putStrLn $ "fib(0..15) = " ++ show valuesmodule Main wherefib :: Int -> Intfib 0 = 0fib 1 = 1fib n = fib (n - 1) + fib (n - 2)main :: IO ()main = dolet values = map fib [0..15]putStrLn $ "fib(0..15) = " ++ show valuesmodule Main wherefib :: Int -> Intfib 0 = 0fib 1 = 1fib n = fib (n - 1) + fib (n - 2)main :: IO ()main = dolet values = map fib [0..15]putStrLn $ "fib(0..15) = " ++ show valuesmodule Main wherefib :: Int -> Intfib 0 = 0fib 1 = 1fib n = fib (n - 1) + fib (n - 2)main :: IO ()main = dolet values = map fib [0..15]putStrLn $ "fib(0..15) = " ++ show values
#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}
import Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sample
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}#include <stdio.h>#include <stdlib.h>static int is_even(int n) {return n % 2 == 0;}int main(void) {int sum = 0;for (int i = 0; i < 100; i++) {if (is_even(i)) sum += i;}printf("sum of even numbers < 100: %d\n", sum);return 0;}
import Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sampleimport Stdnamespace Sampledef fib : Nat → Nat| 0 => 0| 1 => 1| n + 2 => fib (n + 1) + fib ndef isEven : Nat → Bool| 0 => true| 1 => false| n + 2 => isEven ndef main : IO Unit := dolet values := (List.range 20).map fibIO.println s!"fib(0..19) = {values}"IO.println s!"isEven 42 = {isEven 42}"end Sample
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
(define (fib n)(if (< n 2)n(+ (fib (- n 1)) (fib (- n 2)))))(display "fib(0..10) = ")(display (map fib (iota 11)))(newline)(define (fib n)(if (< n 2)n(+ (fib (- n 1)) (fib (- n 2)))))(display "fib(0..10) = ")(display (map fib (iota 11)))(newline)(define (fib n)(if (< n 2)n(+ (fib (- n 1)) (fib (- n 2)))))(display "fib(0..10) = ")(display (map fib (iota 11)))(newline)(define (fib n)(if (< n 2)n(+ (fib (- n 1)) (fib (- n 2)))))(display "fib(0..10) = ")(display (map fib (iota 11)))(newline)(define (fib n)(if (< n 2)n(+ (fib (- n 1)) (fib (- n 2)))))(display "fib(0..10) = ")(display (map fib (iota 11)))(newline)(define (fib n)(if (< n 2)n(+ (fib (- n 1)) (fib (- n 2)))))(display "fib(0..10) = ")(display (map fib (iota 11)))(newline)
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
(define (fib n)(if (< n 2)n(+ (fib (- n 1)) (fib (- n 2)))))(display "fib(0..10) = ")(display (map fib (iota 11)))(newline)(define (fib n)(if (< n 2)n(+ (fib (- n 1)) (fib (- n 2)))))(display "fib(0..10) = ")(display (map fib (iota 11)))(newline)(define (fib n)(if (< n 2)n(+ (fib (- n 1)) (fib (- n 2)))))(display "fib(0..10) = ")(display (map fib (iota 11)))(newline)(define (fib n)(if (< n 2)n(+ (fib (- n 1)) (fib (- n 2)))))(display "fib(0..10) = ")(display (map fib (iota 11)))(newline)(define (fib n)(if (< n 2)n(+ (fib (- n 1)) (fib (- n 2)))))(display "fib(0..10) = ")(display (map fib (iota 11)))(newline)(define (fib n)(if (< n 2)n(+ (fib (- n 1)) (fib (- n 2)))))(display "fib(0..10) = ")(display (map fib (iota 11)))(newline)
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.Lorem ipsum dolor sit amet, consectetur adipiscing elit. Sed do eiusmod tempor incididuntut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitationullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor inreprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteursint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
import ViE.State.Configimport ViE.State.Layoutimport ViE.Workspaceimport ViE.Command.Implimport ViE.Appimport ViE.Buffer.Contentimport ViE.Basicimport Test.Utilsnamespace Test.Workspaceopen Test.Utilsopen ViEdef addWorkspace (state : EditorState) (ws : WorkspaceState) : EditorState :=state.updateCurrentWorkgroup fun wg =>{ wg with workspaces := wg.workspaces.push ws }def switchWorkspace (state : EditorState) (idx : Nat) : EditorState :=state.updateCurrentWorkgroup fun wg =>if idx < wg.workspaces.size then{ wg with currentWorkspace := idx }elsewgdef test : IO Unit := doIO.println "Starting Workspace Test..."let s0 := ViE.initialStatelet wg0 := s0.getCurrentWorkgroupassertEqual "Initial workgroups size" 10 s0.workgroups.sizeassertEqual "Initial workgroup count" 1 wg0.workspaces.sizeassertEqual "Initial workspace index" 0 wg0.currentWorkspaceassertEqual "Initial workspace name" "ViE" s0.getCurrentWorkspace.namelet ws1 := makeWorkspaceState "Project A" (some "/tmp/project-a") 10let s1 := addWorkspace s0 ws1let wg1 := s1.getCurrentWorkgroupassertEqual "Workgroup has 2 workspaces" 2 wg1.workspaces.sizelet s2 := switchWorkspace s1 1assertEqual "Switched to workspace 1" "Project A" s2.getCurrentWorkspace.nameassertEqual "Active buffer comes from workspace 1" 10 (s2.getActiveBuffer.id)let resolved := s2.getCurrentWorkspace.resolvePath "file.txt"assertEqual "ResolvePath uses workspace root" "/tmp/project-a/file.txt" resolvedlet resolvedAbs := s2.getCurrentWorkspace.resolvePath "/abs/file.txt"assertEqual "ResolvePath keeps absolute path" "/abs/file.txt" resolvedAbsIO.println "Starting Workspace Command Test..."let s3 ← ViE.Command.cmdWs ["new", "Project B", "/tmp/project-b"] s2assertEqual "Workspace created and switched" "Project B" s3.getCurrentWorkspace.nameassertEqual "Workspace rootPath set" (some "/tmp/project-b") s3.getCurrentWorkspace.rootPathassertEqual "Active buffer id is new workspace buffer" 11 s3.getActiveBuffer.idlet s4 ← ViE.Command.cmdWs ["rename", "Project B2"] s3assertEqual "Workspace rename applied" "Project B2" s4.getCurrentWorkspace.namelet s5 ← ViE.Command.cmdWs ["new", "Project C"] s4assertEqual "Workspace C created" "Project C" s5.getCurrentWorkspace.namelet s6 ← ViE.Command.cmdWs ["prev"] s5assertEqual "Workspace prev switches back" "Project B2" s6.getCurrentWorkspace.namelet s7 ← ViE.Command.cmdWs ["0"] s6assertEqual "Workspace switch by index" "ViE" s7.getCurrentWorkspace.namelet s8 ← ViE.Command.cmdWs ["list"] s7assertEqual "Workspace list opens explorer buffer" (some "explorer://workgroup") s8.getActiveBuffer.filenamelet wsListText := s8.getActiveBuffer.table.toStringassertEqual "Workspace list contains New Workspace entry" true (wsListText.contains "[New Workspace]")assertEqual "Workspace list contains Rename Workspace entry" true (wsListText.contains "[Rename Workspace]")assertEqual "Workspace list contains Project B2" true (wsListText.contains "Project B2")assertEqual "Workspace list marks current workspace" true (wsListText.contains "*")let s8a := s8.updateActiveView fun v => { v with cursor := {row := ⟨2⟩, col := 0} }let s8b ← ViE.Feature.handleExplorerEnter s8aassertEqual "New workspace enters command mode" Mode.command s8b.modeassertEqual "New workspace command prompt" "ws new " s8b.inputState.commandBufferlet s8c := s8.updateActiveView fun v => { v with cursor := {row := ⟨3⟩, col := 0} }let s8d ← ViE.Feature.handleExplorerEnter s8cassertEqual "Rename workspace enters command mode" Mode.command s8d.modeassertEqual "Rename workspace command prompt" true (s8d.inputState.commandBuffer.startsWith "ws rename ")let s8e ← ViE.Command.cmdWorkspace ["rename", ""] s8assertEqual "Rename workspace rejects empty" "Workspace name cannot be empty" s8e.messagelet s8f ← ViE.Command.cmdWorkspace ["rename", "Project B2"] s8assertEqual "Rename workspace rejects duplicate" true (s8f.message.contains "already exists")let s9 ← ViE.Command.cmdWs ["open", "/tmp/project-d"] s8assertEqual "Workspace open uses path name" "project-d" s9.getCurrentWorkspace.nameassertEqual "Workspace open rootPath set" (some "/tmp/project-d") s9.getCurrentWorkspace.rootPathlet s10 ← ViE.Command.cmdWs ["open", "--name", "Project E", "/tmp/project-e"] s9assertEqual "Workspace open --name prefix" "Project E" s10.getCurrentWorkspace.nameassertEqual "Workspace open --name prefix rootPath" (some "/tmp/project-e") s10.getCurrentWorkspace.rootPathlet s11 ← ViE.Command.cmdWs ["open", "/tmp/project-f", "--name", "Project F"] s10assertEqual "Workspace open --name suffix" "Project F" s11.getCurrentWorkspace.nameassertEqual "Workspace open --name suffix rootPath" (some "/tmp/project-f") s11.getCurrentWorkspace.rootPathlet s12 ← ViE.Command.cmdWs ["close"] s11assertEqual "Workspace close switches to previous" "Project E" s12.getCurrentWorkspace.nameIO.println "Starting Workspace Restore Test..."let bufA : FileBuffer := ViE.Buffer.fileBufferFromTextBuffer 0 none #[stringToLine "WS-A"]let bufB : FileBuffer := ViE.Buffer.fileBufferFromTextBuffer 10 none #[stringToLine "WS-B"]let wsA : WorkspaceState := {name := "WS-A"rootPath := nonebuffers := [bufA]nextBufferId := 1layout := .window 0 { initialView with bufferId := 0 }activeWindowId := 0nextWindowId := 1}let wsB : WorkspaceState := {name := "WS-B"rootPath := nonebuffers := [bufB]nextBufferId := 11layout := .window 0 { initialView with bufferId := 10 }activeWindowId := 0nextWindowId := 1}let s12a := s12.updateCurrentWorkgroup fun wg =>{ wg with workspaces := #[wsA, wsB], currentWorkspace := 0 }let s12b ← ViE.Feature.openWorkspaceExplorer s12alet s12c := s12b.updateActiveView fun v => { v with cursor := {row := ⟨5⟩, col := 0} }let s12d ← ViE.Feature.handleExplorerEnter s12cassertEqual "Workspace selection switches current workspace" "WS-B" s12d.getCurrentWorkspace.nameassertEqual "Workspace selection restores active buffer" "WS-B" s12d.getActiveBuffer.table.toStringIO.println "Starting Workspace Restore Layout Test..."let bufC : FileBuffer := ViE.Buffer.fileBufferFromTextBuffer 20 none #[stringToLine "WS-C1"]let bufD : FileBuffer := ViE.Buffer.fileBufferFromTextBuffer 21 none #[stringToLine "WS-C2"]let layoutC : Layout :=.hsplit(.window 0 { initialView with bufferId := 20 })(.window 1 { initialView with bufferId := 21, cursor := ⟨⟨0⟩, ⟨2⟩⟩ })0.3let wsC : WorkspaceState := {name := "WS-C"rootPath := nonebuffers := [bufC, bufD]nextBufferId := 22layout := layoutCactiveWindowId := 1nextWindowId := 2}let s12e := s12.updateCurrentWorkgroup fun wg =>{ wg with workspaces := #[wsA, wsC], currentWorkspace := 0 }let s12f ← ViE.Feature.openWorkspaceExplorer s12elet s12g := s12f.updateActiveView fun v => { v with cursor := {row := ⟨5⟩, col := 0} }let s12h ← ViE.Feature.handleExplorerEnter s12gassertEqual "Workspace layout restore (active buffer)" "WS-C2" s12h.getActiveBuffer.table.toStringlet ratio := match s12h.getCurrentWorkspace.layout with| .hsplit _ _ r => r| _ => 0.0assertEqual "Workspace layout restore (ratio)" 0.3 ratiolet cursor := s12h.getCursorassertEqual "Workspace layout restore (cursor row)" 0 cursor.row.valassertEqual "Workspace layout restore (cursor col)" 2 cursor.col.valIO.println "Starting Workspace Restore VSplit Test..."let bufE : FileBuffer := ViE.Buffer.fileBufferFromTextBuffer 30 none #[stringToLine "WS-D1"]let bufF : FileBuffer := ViE.Buffer.fileBufferFromTextBuffer 31 none #[stringToLine "WS-D2"]let layoutD : Layout :=.vsplit(.window 0 { initialView with bufferId := 30, cursor := ⟨⟨1⟩, ⟨0⟩⟩, scrollRow := ⟨1⟩, scrollCol := ⟨2⟩ })(.window 1 { initialView with bufferId := 31, cursor := ⟨⟨2⟩, ⟨3⟩⟩, scrollRow := ⟨0⟩, scrollCol := ⟨1⟩ })0.7let wsD : WorkspaceState := {name := "WS-D"rootPath := nonebuffers := [bufE, bufF]nextBufferId := 32layout := layoutDactiveWindowId := 1nextWindowId := 2}let s12i := s12.updateCurrentWorkgroup fun wg =>{ wg with workspaces := #[wsA, wsC, wsD], currentWorkspace := 0 }let s12j ← ViE.Feature.openWorkspaceExplorer s12ilet s12k := s12j.updateActiveView fun v => { v with cursor := {row := ⟨6⟩, col := 0} }let s12l ← ViE.Feature.handleExplorerEnter s12kassertEqual "Workspace vsplit restore (active buffer)" "WS-D2" s12l.getActiveBuffer.table.toStringlet ratio2 := match s12l.getCurrentWorkspace.layout with| .vsplit _ _ r => r| _ => 0.0assertEqual "Workspace vsplit restore (ratio)" 0.7 ratio2let cursor2 := s12l.getCursorassertEqual "Workspace vsplit restore (cursor row)" 2 cursor2.row.valassertEqual "Workspace vsplit restore (cursor col)" 3 cursor2.col.vallet (sRow, sCol) := s12l.getScrollassertEqual "Workspace vsplit restore (scroll row)" 0 sRow.valassertEqual "Workspace vsplit restore (scroll col)" 1 sCol.valIO.println "Starting Workspace Multi-View Restore Test..."let bufG : FileBuffer := ViE.Buffer.fileBufferFromTextBuffer 40 none #[stringToLine "WS-E1"]let bufH : FileBuffer := ViE.Buffer.fileBufferFromTextBuffer 41 none #[stringToLine "WS-E2"]let bufI : FileBuffer := ViE.Buffer.fileBufferFromTextBuffer 42 none #[stringToLine "WS-E3"]let layoutE : Layout :=.hsplit(.vsplit(.window 0 { initialView with bufferId := 40, cursor := ⟨⟨0⟩, ⟨1⟩⟩, scrollRow := ⟨0⟩, scrollCol := ⟨0⟩ })(.window 1 { initialView with bufferId := 41, cursor := ⟨⟨2⟩, ⟨2⟩⟩, scrollRow := ⟨1⟩, scrollCol := ⟨1⟩ })0.4)(.window 2 { initialView with bufferId := 42, cursor := ⟨⟨3⟩, ⟨0⟩⟩, scrollRow := ⟨2⟩, scrollCol := ⟨2⟩ })0.6let wsE : WorkspaceState := {name := "WS-E"rootPath := nonebuffers := [bufG, bufH, bufI]nextBufferId := 43layout := layoutEactiveWindowId := 1nextWindowId := 3}let s12m := s12.updateCurrentWorkgroup fun wg =>{ wg with workspaces := #[wsA, wsC, wsD, wsE], currentWorkspace := 0 }let s12n ← ViE.Feature.openWorkspaceExplorer s12mlet s12o := s12n.updateActiveView fun v => { v with cursor := {row := ⟨7⟩, col := 0} }let s12p ← ViE.Feature.handleExplorerEnter s12oassertEqual "Multi-view restore (active buffer)" "WS-E2" s12p.getActiveBuffer.table.toStringlet (sr2, sc2) := s12p.getScrollassertEqual "Multi-view restore (scroll row)" 1 sr2.valassertEqual "Multi-view restore (scroll col)" 1 sc2.vallet cursor3 := s12p.getCursorassertEqual "Multi-view restore (cursor row)" 2 cursor3.row.valassertEqual "Multi-view restore (cursor col)" 2 cursor3.col.valassertEqual "Multi-view restore (layout hsplit ratio)" 0.6 (match s12p.getCurrentWorkspace.layout with | .hsplit _ _ r => r | _ => 0.0)let subRatio := match s12p.getCurrentWorkspace.layout with| .hsplit left _ _ =>match left with| .vsplit _ _ r => r| _ => 0.0| _ => 0.0assertEqual "Multi-view restore (layout vsplit ratio)" 0.4 subRatioIO.println "Starting Workspace Startup Target Test..."let base := "Test/test_paths"let dirOnly := s!"{base}/dir0"let (wsDirOnly, fileDirOnly) ← ViE.resolveStartupTarget (some dirOnly)assertEqual "Directory arg sets workspace" (some dirOnly) wsDirOnlyassertEqual "Directory arg has no file" none fileDirOnlylet fileNested := s!"{base}/dir0/dir1/dir2/file0.txt"let (wsFileNested, fileFileNested) ← ViE.resolveStartupTarget (some fileNested)assertEqual "File arg sets workspace to parent dir" (some s!"{base}/dir0/dir1/dir2") wsFileNestedassertEqual "File arg keeps filename" (some fileNested) fileFileNestedlet fileTop := s!"{base}/file0.txt"let (wsFileTop, fileFileTop) ← ViE.resolveStartupTarget (some fileTop)assertEqual "Top-level file sets workspace to base" (some base) wsFileTopassertEqual "Top-level file keeps filename" (some fileTop) fileFileTopIO.println "Starting Explorer Path Resolution Test..."let s13 := s12.updateCurrentWorkspace fun ws =>{ ws with rootPath := some "Test", name := "Test" }let s14 ← ViE.Feature.openExplorer s13 "Test"assertEqual "Explorer opens workspace root without duplication" (some "explorer://Test") s14.getActiveBuffer.filenameIO.println "WorkspaceTest passed!"end Test.Workspace
import ViE.State.Configimport ViE.State.Layoutimport ViE.Command.Explorerimport ViE.State.Configimport ViE.Command.Implimport Test.Utilsnamespace Test.WorkgroupExploreropen Test.Utilsopen ViEdef addWorkspace (state : EditorState) (ws : WorkspaceState) : EditorState :=state.updateCurrentWorkgroup fun wg =>{ wg with workspaces := wg.workspaces.push ws }def addWorkgroup (state : EditorState) (name : String) : EditorState :=let nextBufId := state.workgroups.foldl (fun m g =>g.workspaces.foldl (fun m2 ws => max m2 ws.nextBufferId) m) 0let newWg := createEmptyWorkgroup name nextBufId{ state with workgroups := state.workgroups.push newWg }def setCursorRow (state : EditorState) (row : Nat) : EditorState :=state.updateActiveView fun v => { v with cursor := { v.cursor with row := ⟨row⟩ } }def test : IO Unit := doIO.println "Starting Workgroup Explorer Test..."let s0 := ViE.initialStatelet ws1 := makeWorkspaceState "Project A" (some "/tmp/project-a") 10let ws2 := makeWorkspaceState "Project B" (some "/tmp/project-b") 20let s1 := addWorkspace (addWorkspace s0 ws1) ws2let s1 := addWorkgroup s1 "Group B"let s1 := addWorkgroup s1 "Group C"let s2 ← ViE.Command.cmdWg ["list"] s1assertEqual "Explorer buffer is active" (some "explorer://workgroups") s2.getActiveBuffer.filenamelet bufText := s2.getActiveBuffer.table.toStringassertEqual "Explorer contains Workgroup header" true (bufText.contains "Workgroup Explorer")assertEqual "Explorer contains New Workgroup entry" true (bufText.contains "[New Workgroup]")assertEqual "Explorer contains Rename Workgroup entry" true (bufText.contains "[Rename Workgroup]")assertEqual "Explorer contains Group 0" true (bufText.contains "0")assertEqual "Explorer contains Group B" true (bufText.contains "Group B")assertEqual "Explorer marks current workgroup" true (bufText.contains "*")let s3 := setCursorRow s2 2let s4 ← ViE.Feature.handleExplorerEnter s3assertEqual "New workgroup enters command mode" Mode.command s4.modeassertEqual "New workgroup command prompt" "wg new " s4.inputState.commandBufferlet s3b := setCursorRow s2 3let s4b ← ViE.Feature.handleExplorerEnter s3bassertEqual "Rename workgroup enters command mode" Mode.command s4b.modeassertEqual "Rename workgroup command prompt" true (s4b.inputState.commandBuffer.startsWith "wg rename ")let s4c ← ViE.Command.cmdWg ["rename", ""] s2assertEqual "Rename workgroup rejects empty" "Workgroup name cannot be empty" s4c.messagelet s4d ← ViE.Command.cmdWg ["rename", "Group B"] s2assertEqual "Rename workgroup rejects duplicate" true (s4d.message.contains "already exists")let s5 ← ViE.Command.cmdWg ["list"] s1let s6 := setCursorRow s5 5let s7 ← ViE.Feature.handleExplorerEnter s6assertEqual "Switched to workgroup index 1" 1 s7.currentGroupassertEqual "Switch restores workgroup layout" true (s7.getActiveBuffer.filename != some "explorer://workgroup")IO.println "WorkgroupExplorerTest passed!"end Test.WorkgroupExplorer
import ViE.Buffer.LowIOimport ViE.State.Configimport ViE.State.Layoutimport Test.Utilsnamespace Test.PreviewDataopen Test.Utilsdef basePath : String := "Test/test_paths"def testFiles : List String := [s!"{basePath}/file0.txt",s!"{basePath}/dir0/file0.txt",s!"{basePath}/dir0/file1.txt",s!"{basePath}/dir0/file2.txt",s!"{basePath}/dir0/file3.txt",s!"{basePath}/dir0/dir0/file0.txt",s!"{basePath}/dir0/dir1/file1.txt",s!"{basePath}/dir0/dir1/file2.txt",s!"{basePath}/dir0/dir1/file3.txt",s!"{basePath}/dir0/dir1/file4.txt",s!"{basePath}/dir0/dir1/file5.txt"]def test : IO Unit := doIO.println "Starting Preview Data Test..."for path in testFiles dolet buf ← ViE.loadBufferByteArray pathlet content := buf.table.toStringlet byteLen := content.toUTF8.sizeassertEqual s!"{path} has content" true (content.length > 0)assertEqual s!"{path} has bytes" true (byteLen > 0)assertEqual s!"{path} has lines" true (buf.lineCount > 0)let firstLine := ViE.getLineFromBuffer buf 0 |>.getD ""assertEqual s!"{path} has first line" true (firstLine.length > 0)IO.println "PreviewDataTest passed!"end Test.PreviewData
def testWorkgroupSwitch : IO Unit := doIO.println " Testing Workgroup Switching..."let s0 := ViE.initialStatelet s1 ← runKeys s0 [Key.alt '3']assertEqual "Alt-3 switches workgroup" 3 s1.currentGrouplet s2 ← runKeys s1 [Key.alt '0']assertEqual "Alt-0 switches workgroup" 0 s2.currentGroup
import ViE.State.Configimport ViE.Command.Explorerimport ViE.Window.Analysisimport ViE.Window.Actionsimport Test.Utilsnamespace Test.ExplorerPreviewopen Test.Utilsopen ViEdef findEntryIndex (entries : List FileEntry) (name : String) : Option Nat :=let rec loop (list : List FileEntry) (idx : Nat) : Option Nat :=match list with| [] => none| e :: rest =>if e.name == name thensome idxelseloop rest (idx + 1)loop entries 0def test : IO Unit := doIO.println "Starting Explorer Preview Test..."let s0 := ViE.initialStatelet path := "Test/test_paths/dir0/dir1"let s1 ← ViE.Feature.openExplorer s0 pathlet buf := s1.getActiveBufferlet explorerOpt := s1.explorers.find? (fun (id, _) => id == buf.id)match explorerOpt with| none =>throw (IO.userError "Explorer buffer not registered")| some (_, explorer) =>let idx1 := findEntryIndex explorer.entries "file1.txt"let idx2 := findEntryIndex explorer.entries "file2.txt"assert "file1.txt exists in explorer entries" idx1.isSomeassert "file2.txt exists in explorer entries" idx2.isSomelet row1 : Row := ⟨2 + idx1.get!⟩let row2 : Row := ⟨2 + idx2.get!⟩let exAfterOpen := s1.explorers.find? (fun (id, _) => id == buf.id) |>.map (fun (_, ex) => ex)match exAfterOpen with| none => throw (IO.userError "Explorer buffer not registered after open")| some exOpen =>assert "Preview window created on open" exOpen.previewWindowId.isSomelet s2 := s1.updateActiveView fun v => { v with cursor := { row := row1, col := 0 } }let s3 ← ViE.Feature.refreshExplorerPreview s2let exAfterOpt := s3.explorers.find? (fun (id, _) => id == buf.id)match exAfterOpt with| none =>throw (IO.userError "Explorer buffer not registered after preview")| some (_, exAfter) =>assert "Preview window created" exAfter.previewWindowId.isSomeassert "Preview buffer created" exAfter.previewBufferId.isSomelet ws := s3.getCurrentWorkspacelet previewWinId := exAfter.previewWindowId.get!let previewView := ws.layout.findView previewWinId |>.getD initialViewlet previewBuf := ws.buffers.find? (fun b => b.id == previewView.bufferId) |>.getD initialBufferassert "Preview filename has prefix" ((previewBuf.filename.getD "").startsWith "preview://")assert "Preview filename contains file1.txt" ((previewBuf.filename.getD "").contains "file1.txt")let dirIdx := findEntryIndex exAfter.entries "dir0"assert "dir0 exists in explorer entries" dirIdx.isSomelet dirRow : Row := ⟨2 + dirIdx.get!⟩let s3a := s3.updateActiveView fun v => { v with cursor := { row := dirRow, col := 0 } }let s3b ← ViE.Feature.handleExplorerEnter s3alet idsAfterDir := ViE.Window.getWindowIds s3b.getCurrentWorkspace.layoutassert "Preview window kept on directory navigation" (idsAfterDir.contains previewWinId)let newExplorerOpt := s3b.explorers.find? (fun (id, _) => id == s3b.getActiveBuffer.id)match newExplorerOpt with| none => throw (IO.userError "Explorer buffer not registered after directory nav")| some (_, exAfterDir) =>assert "Preview window id preserved on directory nav" (exAfterDir.previewWindowId == exAfter.previewWindowId)let s4 := s3.updateActiveView fun v => { v with cursor := { row := row2, col := 0 } }let s5 ← ViE.Feature.refreshExplorerPreview s4let ws5 := s5.getCurrentWorkspacelet previewView2 := ws5.layout.findView previewWinId |>.getD initialViewlet previewBuf2 := ws5.buffers.find? (fun b => b.id == previewView2.bufferId) |>.getD initialBufferassert "Preview filename updates to file2.txt" ((previewBuf2.filename.getD "").contains "file2.txt")let s5a := s5.updateActiveView fun v => { v with cursor := { row := row2, col := 0 } }let s5b ← ViE.Feature.handleExplorerEnter s5alet idsAfterOpen := ViE.Window.getWindowIds s5b.getCurrentWorkspace.layoutassert "Preview window removed on file open" (!idsAfterOpen.contains previewWinId)let bufIdsAfterOpen := s5b.getCurrentWorkspace.buffers.map (fun b => b.id)let previewBufId := exAfter.previewBufferId.getD 0assert "Preview buffer removed on file open" (!bufIdsAfterOpen.contains previewBufId)let sClose := ViE.Window.closeActiveWindow s5let idsAfter := ViE.Window.getWindowIds sClose.getCurrentWorkspace.layoutassert "Preview window removed on explorer close" (!idsAfter.contains previewWinId)let bufIdsAfterClose := sClose.getCurrentWorkspace.buffers.map (fun b => b.id)assert "Preview buffer removed on explorer close" (!bufIdsAfterClose.contains previewBufId)let s6 ← ViE.Feature.toggleExplorerPreview s5let exAfterClose := s6.explorers.find? (fun (id, _) => id == buf.id) |>.map (fun (_, ex) => ex)match exAfterClose with| none => throw (IO.userError "Explorer buffer missing after close")| some exClose =>assert "Preview window cleared" exClose.previewWindowId.isNoneIO.println "Explorer Preview Test passed!"end Test.ExplorerPreview