Allow progressive insight, and apply two to the bus record

A record can assert a fact that goes stale while the decision it supports
stays right. Superseding for that buries a sound record under a second one
and makes every reader work out which is live. So a correction of fact is
now made in place, marked and dated, with the old wording quoted — bounded
by three conditions and checked by records.py, which fires on an unmarked,
undated or back-dated note. Judgements still supersede.

Applied to 0115: no conformance suite exists to recapture, and the full
genesis bed cannot run until the links exist. Designs 25 and 28 follow.

00-META/checks/records.py

@@ -284,6 +284,59 @@ def check_numbering(failures, records):
             )
 
 
+def check_progressive_insights(failures, records):
+    """A correction made inside a record is marked and dated, or it is a silent rewrite.
+
+    A record may be corrected in place when a *fact* in it went stale and the decision still
+    stands (`02-DECISIONS/README.md`, "Progressive insight"). The whole safety of that allowance
+    is that the correction is legible in the record rather than only in a diff nobody reads, so
+    the form is what is checked here: every mention of an insight is the marker, the marker
+    carries an ISO date, and that date is not earlier than the decision's own — an insight
+    predating the decision it corrects is a copied marker, not a correction.
+
+    What this cannot check is an edit made with no marker at all. Nothing mechanical can; that
+    one is the reviewer's, reading the diff. The check keeps the *marked* path honest so that an
+    unmarked change stands out as the anomaly it is.
+    """
+    phrase = re.compile(r"progressive insight", re.I)
+    marker = re.compile(r"\*\*Progressive insights?\s*[\u2014\u2013-]\s*(\d{4}-\d{2}-\d{2})\.?\*\*")
+    loose = re.compile(r"\*\*[^*]*[Pp]rogressive insights?[^*]*\*\*")
+    iso = re.compile(r"^\d{4}-\d{2}-\d{2}$")
+
+    for number, record in sorted(records.items()):
+        text = record["text"]
+        if not phrase.search(text):
+            continue
+        decided = str(record["front"].get("date", ""))
+        good = [(m.start(), m.end(), m.group(1)) for m in marker.finditer(text)]
+
+        for m in loose.finditer(text):
+            if any(s <= m.start() and m.end() <= e for s, e, _ in good):
+                continue
+            failures.add("insights", rel(record["path"]),
+                         "a progressive insight is not in the dated marked form "
+                         "'**Progressive insight \u2014 YYYY-MM-DD.**': %s" % m.group(0))
+
+        for _, _, stamp in good:
+            if decided and iso.match(decided) and stamp < decided:
+                failures.add("insights", rel(record["path"]),
+                             "a progressive insight dated %s predates the decision (%s)"
+                             % (stamp, decided))
+
+        covered = [(s, e) for s, e, _ in good]
+        for m in phrase.finditer(text):
+            if any(s <= m.start() and m.end() <= e for s, e in covered):
+                continue
+            line = text.rfind("\n", 0, m.start()) + 1
+            if text[line:m.start()].lstrip().startswith("#"):
+                continue
+            if loose.search(text, line, text.find("\n", m.end()) + 1 or len(text)):
+                continue
+            failures.add("insights", rel(record["path"]),
+                         "'progressive insight' appears unmarked; a correction is marked and "
+                         "dated, or it is a silent rewrite")
+
+
 def check_status_against_code(failures):
     """A design document naming specific code may not still call itself `designed`.
 
@@ -325,6 +378,7 @@ def main():
     check_numbering(failures, records)
     check_topics(failures, records)
     check_status_against_code(failures)
+    check_progressive_insights(failures, records)
     print(f"records: {len(records)} decision records checked")
     return failures.report()