add i18n command

I18n.lean

@@ -1,6 +1,9 @@
+import I18n.Cli
 import I18n.EnvExtension
 import I18n.InterpolatedStr
+import I18n.Json
 import I18n.Language
 import I18n.PO
+import I18n.Template
 import I18n.Translate
 import I18n.Utils

I18n/Cli.lean

@@ -0,0 +1,53 @@
+import Cli.Basic
+import I18n.Std.Path
+import I18n.Template
+
+namespace I18n
+
+open Lean Cli
+
+open IO.FS IO.Process Name Core in
+/-- Implementation of `lake exe i18n` command. -/
+unsafe def i18nCLI (args : Cli.Parsed) : IO UInt32 := do
+  if args.flags.size == 0 then
+    IO.println <| IO.userError <| "i18n: expected at least one flag, see `lake exe i18n --help`!"
+
+  if  args.hasFlag "template" then
+    let module : Import := {module := (← getCurrentModule)}
+
+    searchPathRef.set compile_time_search_path%
+    try withImportModules #[module] {} (trustLevel := 1024) fun env => do
+      -- same as `createTemplate` but we're not in `CommandElabM`, but have the `env` explicitely
+      let keys := untranslatedKeysExt.getState env
+      let path ← createTemplateAux keys
+      IO.println s!"i18n: File created at {path}"
+    catch err =>
+      throw <| IO.userError <| s!"{err}\n" ++
+        "i18n: You might want to `lake build` your project first!\n"
+      throw err
+
+  if args.hasFlag "export-json" then
+    let files ← findFilesWithExtension ".i18n" "po"
+
+    for file in files do
+      let outFile := file.withExtension "json"
+      let po ← POFile.read file
+      po.saveAsJson outFile
+      IO.println s!"i18n: exported {file} to {outFile}."
+  return 0
+
+/-- Setting up command line options and help text for `lake exe graph`. -/
+unsafe def i18n : Cmd := `[Cli|
+  i18n VIA I18n.i18nCLI; ["0.1.0"]
+  "I18n CLI
+  Tool for internationalisation of Lean projects.
+  "
+
+  FLAGS:
+    t, "template";     "Create an output template `.i18n/en/Game.pot`."
+    e, "export-json"; "Exports all `.po` files in `.i18n/` to i18next-compatible `.json` format."
+]
+
+/-- `lake exe graph` -/
+unsafe def main (args : List String) : IO UInt32 :=
+  i18n.validate args

I18n/EnvExtension.lean

@@ -91,7 +91,7 @@ def readLanguageConfig (lang? : Option Language := none) : IO LanguageState := d
     IO.FS.writeFile file <| "{\n" ++
       "  \"sourceLang\": \"en\",\n" ++
       -- s!"  \"lang\": \"{lang}\",\n" ++
-      "  \"translationContactEmail\": \"\"\n" ++
+      "  \"translationContactEmail\": \"\",\n" ++
       "  \"useJson\": false\n" ++
       "}\n"
     return {}

I18n/Json.lean

@@ -0,0 +1,2 @@
+import I18n.Json.Read
+import I18n.Json.Write

I18n/I18next/Write.lean → I18n/Json/Write.lean

@@ -14,6 +14,6 @@ def POFile.toJson (poFile : POFile) : Json :=
 
 open Elab.Command in
 
-def POFile.saveAsJson (poFile : POFile) (path : FilePath) : CommandElabM Unit := do
+def POFile.saveAsJson (poFile : POFile) (path : FilePath) : IO Unit := do
   -- TODO: add overwrite-check
   IO.FS.writeFile path poFile.toJson.pretty

I18n/PO.lean

@@ -1,16 +1,3 @@
 import I18n.PO.Definition
 import I18n.PO.Read
-import I18n.PO.ToString
 import I18n.PO.Write
-
-namespace I18n
-
-open Lake
-
-open Lean.Elab.Command in
-
-
--- Bug: Introduces too many \n
-def poToJson (path : FilePath) (out : FilePath) : CommandElabM Unit := do
-  let po ← POFile.read path
-  po.saveAsJson out

I18n/PO/Write.lean

@@ -1,62 +1,120 @@
-import I18n.I18next.Write
-import I18n.PO.ToString
-import I18n.Translate
-import Time
--- import DateTime
-
-/-! # Create PO-file
-
-To create a template PO-file, one needs to call `createPOTemplate`. This can for example
-be done by adding `#create_pot` at the very end of the main file of the package.
-The template is written to a folder `.i18n/` in the package's directory as a `.pot` file
-(or optionally as `.json`).
+import I18n.PO.Definition
+
+/-!
+This file contains the tools to turn `POEntry` objects into strings.
+
+The other direction, i.e. parsing, happens in `I18n.PO.Read` using `Parsec`.
 -/
 
-open Lean System
 namespace I18n
 
-/-- Write a PO-file to disk. -/
-def POFile.save (poFile : POFile) (path : FilePath) : IO Unit :=
-  -- TODO: add overwrite-check
-  IO.FS.writeFile path poFile.toString
+namespace POEntry
+
+/-- A file name containing spaces is wrapped in U+2068 and U+2069. -/
+def escapeRef (s : String) : String := if
+  s.contains ' ' then s!"⁨{s}⁩" else s
+-- TODO: remove these characters when parsing a file!
+
+-- TODO: escape '"' everywhere
+/-- Turn a PO-entry intro a string as it would appear in the PO-file. Such a string
+starts with a bunch of comment lines, followed by `msgid` and `msgstr` (and other options):
+
+```
+#  some comment
+#: Project.MyFile
+msgid "untranslated sentence"
+msgstr "übersetzter Satz"
+
+Note that even the comments are sometimes parsed, depending on the second character after `#`.
+```
+ -/
+def toString (e : POEntry) : String := Id.run do
+  let mut out := ""
+  if let some comment := e.comment then
+    out := out.append <| "".intercalate <| (escape comment).trim.split (· == '\n') |>.map (s!"\n#  {·}")
+  if let some extrComment := e.extrComment then
+    out := out.append <| "".intercalate <| (escape extrComment).trim.split (· == '\n') |>.map (s!"\n#. {·}")
+  -- print the refs
+  if let some ref := e.ref then
+    -- TODO: One example shows `#: src/msgcmp.c:338 src/po-lex.c:699` which is
+    -- different to what's implemented here.
+    let formattedRefs := ref.map (fun (file, line?) => match line? with
+      | none => s!"\n#: {escapeRef file}"
+      | some line => s!"\n#: {escapeRef file}:{line}" )
+    out := out.append <| "".intercalate formattedRefs
+  -- print the flags
+  if let some flags := e.flags then
+    out := out.append <| "\n#, " ++ ", ".intercalate flags
+
+  if let some prevMsgCtxt := e.prevMsgCtxt then
+    out := out.append <| s!"\n#| msgctxt \"{escape prevMsgCtxt}\""
+  if let some prevMsgId := e.prevMsgId then
+      out := out.append <|
+        "\n#| msgid \"" ++
+        ("\\n\"\n#| \"".intercalate <| (escape prevMsgId).split (· == '\n')) ++ "\""
+  if let some msgCtx := e.msgCtxt then
+    out := out.append <| s!"\nmsgctxt \"{escape msgCtx}\""
+  -- print the translation
+  let msgId := "\"" ++ ("\\n\"\n\"".intercalate <| (escape e.msgId).split (· == '\n')) ++ "\""
+  let msgStr := "\"" ++ ("\\n\"\n\"".intercalate <| (escape e.msgStr).split (· == '\n')) ++ "\""
+  out := out.append <| "\nmsgid " ++ msgId
+  out := out.append <| "\nmsgstr " ++ msgStr
+  return out.trim
+
+instance : ToString POEntry := ⟨POEntry.toString⟩
 
-open Elab.Command in
+/-- Paring the header entry into a `POHeaderEntry`. -/
+def toPOHeaderEntry (header : POEntry): POHeaderEntry := Id.run do
+  return {
+    -- TODO: implement!
+    projectIdVersion := ""
+    reportMsgidBugsTo := ""
+    potCreationDate := ""
+    poRevisionDate := ""
+    lastTranslator := ""
+    languageTeam := ""
+    language := ""
+    contentType := ""
+    contentTransferEncoding := ""
+    pluralForms := ""
+  }
 
-/--
-Write all collected untranslated strings into a template file.
+end POEntry
+
+namespace POHeaderEntry
+
+/-- The header entry is marked in the PO-file with `msgid = ""`. -/
+def toPOEntry (header : POHeaderEntry): POEntry := Id.run do
+  let mut msgStr := ""
+  msgStr := msgStr.append s!"Project-Id-Version: {header.projectIdVersion}"
+  msgStr := msgStr.append s!"\nReport-Msgid-Bugs-To: {header.reportMsgidBugsTo}"
+  msgStr := msgStr.append s!"\nPOT-Creation-Date: {header.potCreationDate}"
+  if let some revisionDate := header.poRevisionDate then
+    msgStr := msgStr.append s!"\nPO-Revision-Date: {revisionDate}"
+  msgStr := msgStr.append s!"\nLast-Translator: {header.lastTranslator}"
+  msgStr := msgStr.append s!"\nLanguage-Team: {header.languageTeam}"
+  msgStr := msgStr.append s!"\nLanguage: {header.language}"
+  msgStr := msgStr.append s!"\nContent-Type: {header.contentType}"
+  msgStr := msgStr.append s!"\nContent-Transfer-Encoding: {header.contentTransferEncoding}"
+  if let some pluralForms := header.pluralForms then
+    msgStr := msgStr.append s!"\nPlural-Forms: {pluralForms}"
+  return {msgId := "", msgStr := msgStr}
+
+end POHeaderEntry
+
+namespace POFile
+
+/-- Print a PO file as string.
+A PO file is a series of po-entries, the first one should come from the header.
 -/
-def createTemplate : CommandElabM Unit := do
-  let projectName ← liftCoreM getProjectName
-
-  -- read config instead of `languageState` because that state only
-  -- gets initialised if `set_language` is used in the document.
-  let langConfig ← readLanguageConfig
-
-  let sourceLang := langConfig.sourceLang.toString
-  let ending := if langConfig.useJson then "json" else "po"
-  let fileName := s!"{projectName}.{ending}"
-  let path := (← IO.currentDir) / ".i18n" / sourceLang
-  IO.FS.createDirAll path
-
-  let keys := untranslatedKeysExt.getState (← getEnv)
-
-  let poFile : POFile := {
-    header := {
-      projectIdVersion := s!"{projectName} v{Lean.versionString}"
-      reportMsgidBugsTo := langConfig.translationContactEmail
-      potCreationDate := ← Time.getLocalTime -- (← DateTime.now).extended_format
-      language := sourceLang }
-    entries := keys }
-
-  if langConfig.useJson then
-    poFile.saveAsJson (path / fileName)
-    logInfo s!"Json-file created at {path / fileName}"
-  else
-    poFile.save (path / fileName)
-    logInfo s!"PO-file created at {path / fileName}"
-  -- -- save a copy as Json file for i18next support
-  -- poFile.saveAsJson
-
-/-- Create a i18n-template-file now! -/
-elab "#export_i18n" : command => do
-  createTemplate
+def toString (f : POFile) : String :=
+  ("\n\n".intercalate (([f.header.toPOEntry] ++ f.entries.toList).map (fun e => s!"{e}"))) ++ "\n"
+
+instance : ToString POFile := ⟨POFile.toString⟩
+
+open Lean System
+
+/-- Write a PO-file to disk. -/
+def save (poFile : POFile) (path : FilePath) : IO Unit :=
+  -- TODO: add overwrite-check
+  IO.FS.writeFile path poFile.toString