Language services, formatter and editors

One implementation serves every front end: TTT's editor (through t0-host), t0 lsp, the CLI and future agents. Nothing re-derives types or names; everything reads what the compiler itself recorded.

t0_syntax::lexer::lex_full  ─► highlight  (classes for colouring)
                            └► format     (indentation only, proved)
t0_compiler::analyze        ─► Analysis { compilation, facts, types }
                                 └► t0_compiler::service: hover, definition,
                                    references, symbols, complete

Analysis (t0_compiler::analyze)#

analyze is compile that also keeps the checker's facts: the type of every expression (by span), every declaration (name, kind, span, a one-line signature, and its type for values), and every use of a declared name (use span → declaration span). Facts are recorded while checking, by the same code that decides whether the program is correct; text that does not parse has no facts.

Services (t0_compiler::service)#

service	answers
hover(analysis, offset)	the declaration's signature for a declared or used name; else the type of the smallest expression at offset
definition(analysis, offset)	the declaration span of the name used at offset
references(analysis, offset)	the declaration and every use
symbols(analysis)	functions, structs, enums, constants, strategies
complete(text, offset, manifest, analysis)	candidates at offset (below)

Decorators. After @ it offers param; inside @param( it offers only the keys (min max step log label group hint above below switch off) that are not written yet, above: / below: offer the strategy's parameters (also those written after the cursor) and log: and switch: offer true / false; past the closing ) the ordinary completion returns. Hovering @param or one of its keys says what it is (t0-compiler/src/decorator.rs; the words are declared as facts of kind decorator, which are not items of the program and are never offered as names).

Completion is capability-aware. After contract. it lists that contract's operations with their signature and the permission they need, and gives a status when one cannot be used as written: the program has not declared the contract (requires), the operation is a signal (only inside a strategy), or this host cannot serve it now (the manifest's live status, e.g. "no window is open"). Such entries are still listed — hiding them would hide why a program fails — but marked. At the top level it offers keywords, prelude functions, currencies, modules (marked when not imported), contracts (marked when not declared), the program's items and the locals declared before the cursor. After module. it offers the module's functions; after an enum, its variants; after a value, its fields and methods.

Programs of several files. When a program imports modules (import "lib/levels.tz" as levels;) the analysis keeps their declarations: hover and go to definition on levels.double lead to the line of lib/levels.tz that declares it (service::locate says which file a span is in and gives it in that file's own coordinates), references include the declaration there, levels. offers the functions, types, enums and constants the module lends and levels.Dir. the variants of its enum, and the alias itself is offered at the top level. The outline of a document lists its own items only. The type of an expression is only recorded for the text that is open. t0 lsp reads the modules from beside a file:// document as they were last saved; a document with any other URI has no folder and its imports are refused in words.

Completion usually runs on text that does not parse (someone typing p.), so it works from the last analysis that checked. A position recorded there is trusted only where the current text still reads the same name at that place; otherwise it is ignored rather than guessed.

Formatter (t0_syntax::format::format, t0 fmt)#

t0 fmt <folder> --check|--write formats every .tz file under a folder (a program and its modules together); hidden folders and target are skipped.

It changes only whitespace between lines: each line's indentation (four spaces per earlier line that left a {, ( or [ open, plus one level for a statement continued on the next line), trailing whitespace, and runs of blank lines (at most one; none at the start or end; one final line break). It never joins or splits lines and never touches the inside of a string or a comment; lines inside a block comment are copied byte for byte.

It proves its result before returning it: the output is lexed again and must give the same tokens and the same comments (line comments may lose trailing spaces). Otherwise it refuses and the text is left as it was. It also refuses text with lexical errors and text with carriage returns. Tests: unit tests of the rules; the proof rejecting changed tokens, strings and comments; idempotence; and a round trip over every .tz file in the repository, as written and with all indentation stripped, checking that the compiler reports the same diagnostics before and after (crates/t0-testkit/tests/services.rs).

Highlighting (t0_syntax::highlight)#

Classes come from the real lexer: keywords; contextual keywords only where the grammar takes them as keywords (requires at the head of a file is a keyword, requires as a parameter name is a name); types (capitalised names); calls; numbers; durations; strings; comments; punctuation. Text the lexer cannot read stays uncoloured; nothing is dropped.

t0 lsp#

A Language Server Protocol server over stdin/stdout, written by hand on serde_json (no new dependency). Supported: initialize, initialized, shutdown, exit (exit code 0 only after shutdown), full-text didOpen/didChange/didClose, publishDiagnostics (code, range, severity; notes and help in the message), completion (trigger .; the status shown as documentation), hover, definition, references, documentSymbol, formatting (whole document; a refusal is an error reply with the reason). Other requests get "method not found"; requests before initialize get "server not initialized". Positions are UTF-16 code units unless the client offers UTF-8. Messages over 16 MiB are refused. The server compiles against --manifest if given and never runs a program or grants anything. Tests: framing, a whole session covering every supported request, diagnostics, refusals, completion on unparseable text, UTF-16/UTF-8 positions (crates/t0-cli/src/lsp.rs), and the real binary started, initialised and shut down (crates/t0-cli/tests/cli.rs). No editor extension is shipped; any LSP client can start t0 lsp.

TTT's editor#

The T0 Editor window (terminal-ui/src/t0_window.rs and its t0_window/ modules; the application side in terminal-app/src/t0.rs and main.rs) is laid out as a code editor is: menus (File, Edit, Run, View), an activity bar with three side bar views (Explorer, Permissions, Host), the editor with a tab, run controls and a breadcrumb, a panel (Problems, Output, Jobs) and a status bar, in the T0 brand kit's colours. It:

• colours text with highlight and numbers each line beside its first row;
• colours text with highlight and numbers each line beside its first row;
• underlines diagnostics in the text only while they are about the text on screen: diagnostics, the build and the last run each record a hash of the text they came from, and once it differs they are marked out of date and their positions are no longer drawn;
• lists problems with code, category and position; clicking one, or the ◀ ▶ buttons, selects it in the text;
• shows unsaved changes and asks before anything discards them: New and Open (Discard / Keep editing), and every close — the window's own close button or the OS's close of it, the terminal's close (title bar, Alt+F4, the window manager) and the terminal's self-restart (activation, update) — with Save / Discard / Cancel. Save closes only if saving worked (a failed or declined save closes nothing and says why); Cancel closes nothing; a restart starts the new process only after the answer. The decision logic is terminal_app::t0::CloseGuard (tested without a window); the source and a running program are separate — saving does not stop the program, and closing the terminal stops it (and its jobs) only after the answer, in on_exit;
• saves atomically (a temporary file renamed over the target, so a failed save leaves the old file whole), adds .tz to a name without it, and opens only .tz files up to 1 MiB;
• has separate Check, Build, Validate, Run and Stop; Format runs the formatter above;
• lists backtest jobs with their progress and how full the capacity is (this session, the terminal): Stop job stops one job and leaves its program running (it sees the job stopped by you); Stop program stops the program and every job it started;
• shows the last run's peak memory, and copies the program's output to the window only when it changed;
• offers suggestions after . or Ctrl+Space, from complete against the terminal's live manifest and the last check;
• keeps permissions off until turned on, for the session only, never saved and never set by a program.

Nothing in the window runs anything: it reports what was pressed and the application acts. The parser bounds nesting (128 levels), which keeps the parse behind suggestions safe on the UI thread; compilation and execution run on their own threads with a large stack.