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
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:
Old but relevant Zulip