Read a commodity header's symbol as its first token

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

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