Skip to content

Idris API Redesign Goals

Michael Messer edited this page Nov 30, 2021 · 5 revisions

Idris API Redesign Goals

  • Decouple from REPL/IDE Mode
  • Check as you type
  • Documentation
  • Multithreaded?
  • Process notifications?
  • Streaming results?

File Management

  • Handle multiple loaded files
  • Handle files not on disk
  • Support incremental changes
  • REPL IDE prints after every file load, but LSP can't access till after after every file is completed
  • Use something similar to LSP's Diagnostic so LSP doesn't have to pattern match on all errors and warnings
  • Accept just a location (no name)
  • Return range
  • Expose unified structure of in-order non-overlapping single-line tokens
  • Partial?
  • Delta?

REPL (Custom extension)

  • What would REPL look like with multiple files loaded and check as you type?
  • Reactive notebooks?