Skip to content

feat: Locally saved preamble #89

@SnirBroshi

Description

@SnirBroshi

Feature request: Add a "preamble" section (like in LaTeX) to the settings panel, containing a small Monaco editor whose contents will be automatically concatenated before the main editor's contents.

This will be saved locally, and I think it should not appear in the URL, but a prominent "PREAMBLE ENABLED" should be visible at all times to avoid confusion when running code from Zulip or sharing code.
I also think a checkbox "enable preamble" would be useful to quickly enable/disable it without deleting it.

An example of a preamble which I find useful:

import Mathlib
set_option autoImplicit false
variable {α : Type*} [Group α] {x y z : α}
variable {V : Type*} {G : SimpleGraph V}

Old but relevant Zulip

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions