diff --git a/Ledger/Journal.lean b/Ledger/Journal.lean index 17113e2..43654ca 100644 --- a/Ledger/Journal.lean +++ b/Ledger/Journal.lean @@ -1599,7 +1599,9 @@ def run (input0 : String) (dcDefault : Bool := false) | .commBlock comm => let body := trimS t if body.startsWith "alias " then - let al := trimS (body.drop "alias ".length).toString + -- a `;` outside quotes begins a comment (regress/3313_2) + let al := trimS (stripCommodityComment + (body.drop "alias ".length).toString) let al := (unquote al).getD al st := { st with commAliases := (al, comm) :: st.commAliases } continue @@ -1749,14 +1751,17 @@ def run (input0 : String) (dcDefault : Bool := false) let nm := trimS (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 ((unquote nm).getD nm) } + 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 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 + -- (regress/3313) let nm := trimS (t.drop "commodity ".length).toString - st := { st with pending := .commBlock ((unquote nm).getD nm) } + st := { st with pending := .commBlock (headerSymbol nm) } else if t.startsWith "payee " || t.startsWith "tag " then st := { st with pending := .ignoreBlock } -- label declarations else if t.startsWith "@" || t.startsWith "!" then diff --git a/Ledger/Parse.lean b/Ledger/Parse.lean index 763ff77..ecd48c2 100644 --- a/Ledger/Parse.lean +++ b/Ledger/Parse.lean @@ -297,6 +297,41 @@ def unquote (s : String) : Option String := else none | _ => none +/-- The commodity that a `commodity` header names: a quoted symbol up + to its closing quote, or else the leading run of characters up to + whitespace or a `;`, which begins a comment. As in an amount, a + backslash puts the character after it into the run, so `A\;B` names + `A;B`, and the rest of the line is ignored (C++ + `commodity_t::parse_symbol(char*&)`, regress/3313). -/ +def headerSymbol (s : String) : String := + match s.toList with + | '"' :: rest => String.ofList (rest.takeWhile (ยท != '"')) + | cs => + let rec go : List Char โ†’ List Char + | [] => [] + | '\\' :: c :: rest => c :: go rest + | c :: rest => + if c == ' ' || c == '\t' || c == ';' then [] else c :: go rest + String.ofList (go cs) + +/-- Cut the comment from the argument of a commodity block's `alias` + line. It begins at the first `;` that is neither inside a quoted + symbol nor escaped with a backslash, the only places that a + commodity symbol can hold one (C++ `strip_commodity_comment` in + textual_directives.cc, regress/3313_2). -/ +def stripCommodityComment (s : String) : String := + let rec go (quoted : Bool) : List Char โ†’ List Char + | [] => [] + | '"' :: rest => '"' :: go (!quoted) rest + | ';' :: rest => if quoted then ';' :: go quoted rest else [] + | '\\' :: rest => + if quoted then '\\' :: go quoted rest + else match rest with + | c :: rest' => '\\' :: c :: go quoted rest' + | [] => ['\\'] + | c :: rest => c :: go quoted rest + String.ofList (go false s.toList) + /-- Time-unit commodities canonicalize to seconds. -/ def timeFactor (s : String) : Option โ„š := if s == "s" then some 1