End an account header's name at a hard-separated comment

Ledger/Journal.lean

@@ -1578,7 +1578,9 @@ def run (input0 : String) (dcDefault : Bool := false)
           let frames := frames.filter fun (i, _) => i < ind
           let name := ((frames.head?).map (·.2)).getD ""
           if body.startsWith "account " then
-            let nm := trimS (body.drop "account ".length).toString
+            -- a nested name ends before a hard-separated `;` comment, as
+            -- a top-level one does (regress/3320)
+            let nm := headerAccount (body.drop "account ".length).toString
             let nm := (unquote nm).getD nm
             let full := if name.isEmpty then nm else name ++ ":" ++ nm
             st := { st with pending := .acctBlock ((ind, full) :: frames) }
@@ -1614,8 +1616,10 @@ def run (input0 : String) (dcDefault : Bool := false)
             continue
           else if body.startsWith "format " then
             -- the format subdirective DECLARES the display precision
-            -- and locks it against migration (opt-round, 1795, 628)
-            let sample := trimS (body.drop "format ".length).toString
+            -- and locks it against migration (opt-round, 1795, 628);
+            -- it may spell the block's symbol bare (3312)
+            let sample :=
+              quoteBareSymbol (trimS (body.drop "format ".length).toString) comm
             match (parseAmount st.amt n sample) with
             | .ok r =>
                 st := lockPrecision st
@@ -1755,14 +1759,17 @@ def run (input0 : String) (dcDefault : Bool := false)
           || t.startsWith "b " then
         continue  -- historical timelog compatibility: ignored
       else if t.startsWith "@account " || t.startsWith "!account " then
-        let nm := trimS (t.drop "@account ".length).toString
+        -- read as a plain `account` header (regress/3320_3)
+        let nm := headerAccount (t.drop "@account ".length).toString
         st := { st with pending := .acctBlock [(0, (unquote nm).getD nm)] }
       else if t.startsWith "@commodity " || t.startsWith "!commodity " then
         -- read as a plain `commodity` header (regress/3313)
         let nm := trimS (t.drop "@commodity ".length).toString
         st := { st with pending := .commBlock (headerSymbol nm) }
       else if t.startsWith "account " || t.startsWith "account\t" then
-        let nm := trimS (t.drop "account ".length).toString
+        -- the name ends before a `;` that follows a hard separator,
+        -- which begins a comment (regress/3320, regress/3320_3)
+        let nm := headerAccount (t.drop "account ".length).toString
         st := { st with pending := .acctBlock [(0, (unquote nm).getD nm)] }
       else if t.startsWith "commodity " || t.startsWith "commodity\t" then
         -- the symbol is the first token, and a `;` ends a bare one

Ledger/Parse.lean

@@ -183,6 +183,24 @@ def splitField (s : String) : String × Option String :=
 
 def trimS (s : String) : String := s.trimAscii.toString
 
+/-- The account that an `account` line names: the text up to the first
+    `;` that follows a hard separator (a tab, or two or more spaces),
+    which begins a comment, as a note begins after a transaction's
+    payee. A `;` after a single space, or after none, is part of the
+    name, as it is in a posting (C++ `split_inline_note` in utils.h,
+    called by `account_directive_body`; regress/3320). -/
+def headerAccount (s : String) : String :=
+  let rec go (spaces : Nat) (tab : Bool) : List Char → List Char
+    | [] => []
+    | ';' :: rest =>
+        if tab || spaces ≥ 2 then [] else ';' :: go 0 false rest
+    | ' ' :: rest => ' ' :: go (spaces + 1) tab rest
+    | '\t' :: rest => '\t' :: go spaces true rest
+    | c :: rest => c :: go 0 false rest
+  -- the scan starts at the name, as C++ skips the blanks before it
+  let cs := s.toList.dropWhile fun c => c == ' ' || c == '\t'
+  trimS (String.ofList (go 0 false cs))
+
 /-! ## Numbers under commodity styles -/
 
 private def digitsVal (cs : List Char) : ℕ :=
@@ -349,6 +367,46 @@ def resolveCommodity (line : Nat) (raw : String) : Except String String := do
       if validCommodity raw then pure raw
       else err line s!"malformed commodity '{raw}'"
 
+/-- Does an amount have to quote this symbol? The C++ table, not this
+    reader's `validCommodity`: commodity.cc `invalid_chars`, the
+    characters that end a bare symbol there. -/
+def symbolNeedsQuotes (s : String) : Bool :=
+  s.toList.any fun c =>
+    c.isDigit || c == ' ' || c == '\t' || c == '\n' || c == '\r'
+      || c.toNat == 127 || "!&()*+,-./:;<=>?@[]^{|}~".toList.contains c
+
+/-- Would a bare symbol and a number that meet at characters `a` and
+    `b` run together? Only when both are characters `parse_quantity`
+    reads as part of a number (amount.cc). -/
+def runsTogether (a b : Char) : Bool :=
+  let inNumber (c : Char) : Bool :=
+    c.isDigit || c == '.' || c == ',' || c == '\''
+  inNumber a && inNumber b
+
+/-- A `format` sample may spell its block's symbol bare, as the
+    `commodity` header does, though an amount must quote it:
+    `commodity N1` with `format 1,000.00 N1` (regress/3312;
+    textual_directives.cc `quote_bare_symbol`). The bare symbol is
+    quoted at either end of the sample, unless the sample quotes
+    already or the symbol runs into the number (`N11,000.00`), where
+    nothing marks where it ends. -/
+def quoteBareSymbol (sample sym : String) : String :=
+  if !symbolNeedsQuotes sym || sample.contains '"' then sample else
+  let s := sample.toList
+  let y := sym.toList
+  let n := y.length
+  let quoted := "\"" ++ sym ++ "\""
+  let touches (a b : Option Char) : Bool :=
+    match a, b with
+    | some a, some b => runsTogether a b
+    | _, _ => false
+  if s.take n == y && !touches y.getLast? (s.drop n).head? then
+    quoted ++ String.ofList (s.drop n)
+  else if s.length > n && s.drop (s.length - n) == y
+      && !touches (s.take (s.length - n)).getLast? y.head? then
+    String.ofList (s.take (s.length - n)) ++ quoted
+  else sample
+
 /-! ## Amounts -/
 
 /-- Style/definition context threaded through amount parsing. -/