Editor Componentization

[Negabinary]

Editor Componentization

Warning: this is a huge change to the Haz3lweb portion of the codebase. I've tried to provide a guide below for merging this into your branch.

Motivation:

The goal of this refactor is to turn Haz3lWeb into a tree of re-usable, independent components. There is both a short-term, and long-term motivation to do this.

In the short-term, being able to re-use the editors, and statics highlighting in particular will allow us to select / edit outputs. This is important for the interactions that will be in the proof stepper but also for the flexibility to copy results back into code etc.

In the long-term, this componentization gets us closer to good coding practices in the hazel codebase. It creates a separation of concerns where each component can consider only its local state/updates, instead of needing to worry about global state/update.

The Big Changes

• A lot of files in Haz3lweb have moved. I'm hoping git will handle this automatically.

• Model.re, UpdateAction.re and Update.re have been deleted. Each component of the UI now has its own Model and Update modules. If you had added any actions to UpdateAction.re, you will now want to add them to the Update module of the component in the ui tree "where the action takes place".

• DHDoc_Exp, and other functions for printing dynamic expressions are gone. Anything that was previously output that way will need to be output using one of the following:

  • new syntax in user expressions (e.g. users can now type fix, but this allows us to show them in output)
  • static errors (e.g. failed casts are now shown using static type errors in the results)
  • or wait until #1218 is merged in (e.g. we'll use projectors to hide functions when projectors are merged in)

Design:

Each component is a file that contains four modules:

• Model: stores the model of this component, along with initializers and serialization methods
• Update: gives the available actions on this component, and functions that perform those actions. There is also a function to re-calculate all the dependent data.
• Selection: has methods for working out which editor on a screen is currently "active" and dispatches key events to the correct place
• View: has methods for viewing the model and connecting up actions to the correct update.

Open Bugs:

• [ ] ExplainThis drop-down doesn't work
• [ ] School mode evaluation doesn't always work, and is slow
• [ ] Spacing around output code is not consistent
• [ ] Casts are not output
• [ ] Steppers don't save
• [ ] TyDi is disabled
• [ ] Holes don't print in cursor info types

todo: check that I haven't broken:

• Assistant / Resetting Assistant
• School mode secrecy