diff --git a/Ledger/Journal.lean b/Ledger/Journal.lean index 3508666..5c46a68 100644 --- a/Ledger/Journal.lean +++ b/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 diff --git a/Ledger/Parse.lean b/Ledger/Parse.lean index ecd48c2..e8a1f08 100644 --- a/Ledger/Parse.lean +++ b/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. -/