Todo List for DrRacket

7.7

top ← prev up next →

Todo List for DrRacket

David Thrane Christiansen

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.

Screenshot of the Todo List

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.

The following syntax properties are recognized by the Todo List:

'todo: the complete task to be shown in the Todo List. A TODO is either a string, an instance of the todo-item prefab struct, or an instance of located with a todo-item inside.
'editing-command: an editing command to be shown in a region. A command is a cons tree of instances of command or instances of located with a command inside.

To avoid a runtime dependency between your language and the Todo List, it is better to paste in the source for the prefab structs todo-item, command, and located than to require them directly.

struct
(struct todo-item (full summary)
    #:prefab)
  full : string?
  summary : (or/c #f string?)

A todo-item represents an item to be shown in the todo list. The contents of full are used as the contents of the details pane, and if summary is #f, then full is also used as the summary for the Todo List. If summary is a string, then it is used as the summary.

struct
(struct command (name module-path function arguments)
    #:prefab)
  name : string?
   module-path :
(or/c module-path?
      resolved-module-path?
      module-path-index?)
  function : symbol?
  arguments : (listof any/c)

An editing command. The name is a string to be shown to users in a menu, the module-path will be loaded with dynamic-require to find the implementation of the command, and function (which must be provided by the module) will be called with arguments. If it returns a string, then the string is used to replace the region that was clicked on.

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.

struct
(struct located (location value)
    #:prefab)
  location : source-location?
  value : any/c

A an item in the Todo List or a command can be put inside a located struct. The location field contains the region to associate it with, and the value field contains the TODO or command.

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.

top ← prev up next →