Copyright	(c) Leon Vatthauer 2026
License	GPL-3
Maintainer	Leon Vatthauer <leon.vatthauer@fau.de>
Stability	experimental
Portability	non-portable (ghc-wasm-meta)
Safe Haskell	None
Language	GHC2024

App.Views

Contents

Views
Utilities

Description

This module defines the Miso Views of the application.

Synopsis

viewModel :: Model -> View Model Action
viewHeader :: Model -> View Model Action
viewLogoHeader :: Model -> View Model Action
viewHeaderRight :: Model -> View Model Action
viewErrorNumber :: Model -> View Model Action
viewNavigationButtons :: View Model Action
viewProofActionsHeader :: View Model Action
viewBin :: View Model Action
viewSpawnNode :: SpawnType -> MisoString -> MisoString -> View Model Action
viewMenuButton :: View Model Action
viewNewProofButton :: Model -> View Model Action
viewSidebar :: Model -> View Model Action
viewDetails :: MisoString -> MisoString -> View Model Action -> View Model Action
viewUsage :: View Model Action
viewGrammar :: Model -> View Model Action
viewRules :: Model -> View Model Action
viewExamples :: Model -> View Model Action
viewLogics :: Model -> View Model Action
viewSource :: Model -> View Model Action
viewProof :: Model -> View Model Action
viewLineNos :: Model -> View Model Action
viewRuleApplications :: Model -> View Model Action
viewErrorBox :: MisoString -> MisoString -> View Model Action
mkFormulaInputId :: NodeAddr -> Proof -> MisoString
mkRuleInputId :: NodeAddr -> Proof -> MisoString
viewLine :: Model -> NodeAddr -> Either Assumption Derivation -> View Model Action
viewMaterialIcon :: MisoString -> View Model Action
viewDropZoneAt :: Model -> Maybe MisoString -> NodeAddr -> View Model Action
interleaveWithDropZones :: Model -> Maybe MisoString -> Maybe NodeAddr -> (Int -> NodeAddr) -> [View Model Action] -> [View Model Action]

Views

viewModel :: Model -> View Model Action Source #

Takes a Model and returns the corresponding View containing a sidebar, the proof workspace and a header.

Header

viewHeader :: Model -> View Model Action Source #

Returns the header of the application.

viewLogoHeader :: Model -> View Model Action Source #

Shows the logo in the viewHeader, together with a title and navigation buttons

viewHeaderRight :: Model -> View Model Action Source #

viewErrorNumber :: Model -> View Model Action Source #

viewNavigationButtons :: View Model Action Source #

Adds navigation buttons for accessing the browsers history API.

viewProofActionsHeader :: View Model Action Source #

For use in viewHeader, returns buttons for spawning Assumption, Derivation, Proof or a trash can.

viewBin :: View Model Action Source #

For use in viewProofActionsHeader, returns a trash can, where elements can be deleted.

viewSpawnNode Source #

Arguments

:: SpawnType	Type of node to be spawned
-> MisoString	Tooltip of the button
-> MisoString	The buttons icon.
-> View Model Action

For use in viewProofActionsHeader, returns a button for spawning a Assumption, Derivation or Proof.

viewMenuButton :: View Model Action Source #

For use in viewHeader returns a button that opens and closes the sidebar.

viewNewProofButton :: Model -> View Model Action Source #

For use in viewHeader, returns a button for starting a new Proof.

Sidebar

viewSidebar :: Model -> View Model Action Source #

Returns the sidebar of the application.

viewDetails Source #

Arguments

:: MisoString	Text of the details summary.
-> MisoString	Icon of the details summary.
-> View Model Action	Content of the details element.
-> View Model Action

Wrapper for creating details elements in the sidebar.

viewUsage :: View Model Action Source #

For use in viewSidebar, returns usage instructions.

viewGrammar :: Model -> View Model Action Source #

For use in viewSidebar, returns a list of symbols that can be used, and on hover shows their aliases.

viewRules :: Model -> View Model Action Source #

For use in viewSidebar, returns a list of the logic's rules, on hover shows the rule definition.

viewExamples :: Model -> View Model Action Source #

For use in viewSidebar, returns a list of example Proofs, on hover shows the Assumptions and conclusion of the Proof.

viewLogics :: Model -> View Model Action Source #

For use in viewSidebar, returns a list of buttons that enable the user to change the underlying logic of the proof checker.

viewSource :: Model -> View Model Action Source #

For use in viewSidebar, contains a link to the repository and the documentation.

Proof

viewProof :: Model -> View Model Action Source #

Shows the proof workspace of the application, containing a list of line numbers, a list of formula inputs and a list of rule inputs.

viewLineNos :: Model -> View Model Action Source #

For use in viewProof, returns a list of line numbers that are shown to the left of the Proof.

viewRuleApplications :: Model -> View Model Action Source #

For use in viewProof, returns a list of RuleApplications (judgements), that are shown to the right of the Proof.

viewErrorBox Source #

Arguments

:: MisoString	`id` of the errorbox.
-> MisoString	Error message.
-> View Model Action

Returns a errorbox that is shown on hover, containing errors written in a code element to get monospacing.

mkFormulaInputId :: NodeAddr -> Proof -> MisoString Source #

Helper for turning a NodeAddr to a formula inputfield id.

mkRuleInputId :: NodeAddr -> Proof -> MisoString Source #

Helper for turning a NodeAddr to a rule inputfield id.

viewLine :: Model -> NodeAddr -> Either Assumption Derivation -> View Model Action Source #

For use in viewProof, shows a single line of the Proof, specified by its NodeAddr.

Utilities

viewMaterialIcon :: MisoString -> View Model Action Source #

Helper for viewing material icons based on their name, see https://fonts.google.com/icons

viewDropZoneAt Source #

Arguments

:: Model	The `Model`.
-> Maybe MisoString	Optional class for the dropzone.
-> NodeAddr	The corresponding `NodeAddr`.
-> View Model Action

Shows a dropzone for the given NodeAddr, i.e. a small empty div, where nodes can be dropped.

Expands, if a node can be dropped inside.

interleaveWithDropZones Source #

Arguments

:: Model	The `Model`.
-> Maybe MisoString	Optionally a class for the last dropzone.
-> Maybe NodeAddr	Optionally a differing `NodeAddr` for the last dropzone.
-> (Int -> NodeAddr)	A function for generating `NodeAddr` from a number (e.g. turn `n` into `NAAssumption n`).
-> [View Model Action]	The list of views to be interleaved.
-> [View Model Action]

Interleaves the list views with dropzones of the corresponding NodeAddr.