135 lines
4.6 KiB
Plaintext
135 lines
4.6 KiB
Plaintext
-- allium: 1
|
|
-- bDS Navigation Menu
|
|
-- Scope: core (read for rendering), extension Bucket F (menu editor UI)
|
|
-- File-only model: no DB table. Loaded from meta/menu.opml into a
|
|
-- transient value, mutated in memory, written back to OPML on save.
|
|
|
|
surface MenuManagementSurface {
|
|
facing _: MenuOperator
|
|
|
|
provides:
|
|
MenuLoadRequested(project_id)
|
|
UpdateMenuRequested(items)
|
|
SyncMenuFromFilesystemRequested(project_id)
|
|
}
|
|
|
|
surface MenuEditorSurface {
|
|
facing _: MenuOperator
|
|
|
|
provides:
|
|
MenuEditorOpened(project_id)
|
|
MenuEntryDraftRequested(menu, selected_item, kind)
|
|
MenuEntryDraftCompleted(menu, selection_or_label)
|
|
MenuEntryDraftCancelled(menu)
|
|
MenuTreeEditRequested(menu, selected_item, operation, target_item, drop_position)
|
|
UpdateMenuRequested(items)
|
|
|
|
@guarantee EntryCreation
|
|
-- A new page/category draft is inserted directly after the selected
|
|
-- item, or as the first child when a submenu is selected. A page draft
|
|
-- can select an existing page; submitting free text instead creates a
|
|
-- submenu. A category draft can select an existing category or create
|
|
-- a new category from non-empty free text. Cancelling removes the draft.
|
|
|
|
@guarantee TreeEditing
|
|
-- Entries may move among siblings, indent only beneath a preceding
|
|
-- submenu, unindent to immediately after their parent, or be dragged
|
|
-- before/after an entry or inside a submenu. A drop onto itself, one of
|
|
-- its descendants, or inside a non-submenu has no effect.
|
|
|
|
@guarantee HomeProtection
|
|
-- The canonical Home entry cannot be moved, indented, unindented,
|
|
-- deleted, or dragged. Those actions are unavailable while it is
|
|
-- selected and remain no-ops if invoked indirectly.
|
|
|
|
@guarantee SaveFeedback
|
|
-- Save persists the current normalized tree through UpdateMenu and
|
|
-- informs the operator that the blog menu was saved.
|
|
}
|
|
|
|
value MenuItem {
|
|
kind: page | submenu | category_archive | home
|
|
label: String
|
|
slug: String? -- pageSlug for page/home, categoryName for category_archive
|
|
children: List<MenuItem>? -- present only for submenu kind
|
|
}
|
|
|
|
value Menu {
|
|
items: List<MenuItem>
|
|
|
|
-- Derived
|
|
home_entry: items.first -- always home after normalization
|
|
}
|
|
|
|
surface MenuSurface {
|
|
context menu: Menu
|
|
|
|
exposes:
|
|
menu.items.count
|
|
menu.home_entry.label
|
|
}
|
|
|
|
invariant HomeAlwaysFirst {
|
|
-- Normalization guarantees home is always the first item.
|
|
-- UpdateMenu strips any home entries from input, then prepends one.
|
|
for menu in Menus:
|
|
menu.items.first.kind = home
|
|
}
|
|
|
|
invariant MenuPersistedAsOpml {
|
|
-- meta/menu.opml is the sole persistent store (no DB table).
|
|
-- OPML outline attributes: text (label), type (kind),
|
|
-- pageSlug (slug for page/home), categoryName (slug for category_archive).
|
|
-- Nested <outline> elements represent submenu children.
|
|
parse_opml(read_file("meta/menu.opml")) = menu.items
|
|
}
|
|
|
|
rule LoadMenu {
|
|
when: MenuLoadRequested(project_id)
|
|
-- Reads meta/menu.opml; if file missing, returns default (home-only) menu.
|
|
-- Normalizes: strips home entries from body, prepends canonical home.
|
|
ensures: MenuLoaded(project_id, normalize(parse_opml_or_empty(project_id)))
|
|
}
|
|
|
|
rule UpdateMenu {
|
|
when: UpdateMenuRequested(items)
|
|
-- Normalizes Home entry: strips all home items, prepends canonical home.
|
|
-- Writes normalized menu back to meta/menu.opml.
|
|
let without_home = items where kind != home
|
|
ensures: MenuFileWritten(normalize(without_home))
|
|
}
|
|
|
|
rule SyncMenuFromFilesystem {
|
|
when: SyncMenuFromFilesystemRequested(project_id)
|
|
-- Reloads menu from OPML, normalizes, writes back (round-trip repair).
|
|
ensures: MenuLoaded(project_id, _)
|
|
ensures: MenuFileWritten(_)
|
|
}
|
|
|
|
rule OpenMenuEditor {
|
|
when: MenuEditorOpened(project_id)
|
|
ensures: MenuLoaded(project_id, _)
|
|
ensures: MenuEditorReady(project_id)
|
|
}
|
|
|
|
rule StartMenuEntryDraft {
|
|
when: MenuEntryDraftRequested(menu, selected_item, kind)
|
|
requires: kind = page or kind = category_archive
|
|
ensures: MenuDraftInserted(menu, selected_item, kind)
|
|
}
|
|
|
|
rule CompleteMenuEntryDraft {
|
|
when: MenuEntryDraftCompleted(menu, selection_or_label)
|
|
ensures: MenuDraftResolved(menu, selection_or_label)
|
|
}
|
|
|
|
rule CancelMenuEntryDraft {
|
|
when: MenuEntryDraftCancelled(menu)
|
|
ensures: MenuDraftRemoved(menu)
|
|
}
|
|
|
|
rule EditMenuTree {
|
|
when: MenuTreeEditRequested(menu, selected_item, operation, target_item, drop_position)
|
|
ensures: MenuTreePreviewUpdated(menu)
|
|
}
|