Todo List is a DrRacket tool that displays a list of the unwritten parts of a program, as determined by the macros that implement those unwritten parts, as well as providing opportunities to write the unfinished parts of the program with compiler support.
In particular, when Check Syntax finds a syntax object during expansion with the 'todo syntax property, then it considers that syntax object to be a task to be completed. After expansion, a panel pops up with a list of these tasks to be completed. When it finds an object with the 'editing-command property mapped to a description of the editing command, then the editing commands are provided in a DrRacket right-click menu.
This tool is intended for use with cooperating languages, especially statically typed languages and proof assistants. It is inspired by the hole list in the Agda mode for Emacs as well as the ability of users to add custom interactive commands to Lean.
Open demo.rkt from the package’s source for a very simple hole macro and two editing commands.
#:prefab) name : string?
(or/c module-path? resolved-module-path? module-path-index?) function : symbol? arguments : (listof any/c)
Additionally, if function accepts the following keyword arguments, then they will be provided as well: #:string contains the string of the region on which the command was placed, #:definitions is the DrRacket definitions window, #:editor is the text editor object in which the command was called, and #:file the path to the file being edited.
While the values passed to #:definitions and #:editor presently coincide, if editing commands are ever supported in the interactions window, then they may not. So use #:editor to get access to the widget in which the command is called, and #:definitions to get access to the program context regardless of where the command is invoked.
Only one TODO is permitted for a region: if the location fields cause multiple goals to overlap, then one will replace the other in an unspecified order.