merge: tick in-body checkboxes from a domain script

# Conflicts:
#	AGENTS.md
This commit is contained in:
naudachu
2026-08-10 15:42:38 +05:00
9 changed files with 762 additions and 13 deletions
+20 -6
View File
@@ -30,6 +30,16 @@ def cell(v):
return v.replace("|", "\\|") or ""
def progress(body):
"""`3/7` for a body with checkboxes, "" for one without.
Counted from the body every time the index is built and stored nowhere —
the boxes are the state, and a second copy of it in a metadata field would
be wrong by the next edit."""
done, total = issue.checkbox_progress(body)
return "%d/%d" % (done, total) if total else ""
def build(root):
# An index of a store that is not there is not an empty index, it is a bad
# path. Raising beats writing INDEX.md into a directory nobody asked for.
@@ -42,6 +52,7 @@ def build(root):
rows.append({
"id": i,
"state": cell(iss.state),
"progress": progress(iss.body),
"type": cell(iss.type),
"labels": cell(rest),
"title": cell(iss.title),
@@ -57,13 +68,16 @@ def build(root):
"Every issue this project knows about. `origin: local` means it "
"exists nowhere else — a complete state, not a pending one. Any "
"other value names the tracker it also lives in; the handle is in "
"the file. Rebuild with `issue_index.py`.", ""]
"the file. `progress` counts the body's checkboxes, ticked over "
"total, and is blank for an issue that has none — read off the "
"body at build time, stored nowhere. Rebuild with `issue_index.py`; "
"tick a box with `issue_ac.py`.", ""]
if rows:
out += ["| id | state | type | labels | title | milestone | depends | origin |",
"|---|---|---|---|---|---|---|---|"]
out += ["| [%s](%s.md) | %s | %s | %s | %s | %s | %s | %s |" % (
r["id"], r["id"], r["state"], r["type"], r["labels"], r["title"],
r["milestone"], r["depends"], r["origin"]) for r in rows]
out += ["| id | state | progress | type | labels | title | milestone | depends | origin |",
"|---|---|---|---|---|---|---|---|---|"]
out += ["| [%s](%s.md) | %s | %s | %s | %s | %s | %s | %s | %s |" % (
r["id"], r["id"], r["state"], r["progress"], r["type"], r["labels"],
r["title"], r["milestone"], r["depends"], r["origin"]) for r in rows]
else:
out.append("_empty_")