Add Reflection.TypeChecking.Format.errorPartFmt (#1307)

Author: UlfNorell

CHANGELOG.md

@@ -35,6 +35,8 @@ Other major changes
 Other minor additions
 ---------------------
 
+* Added `Reflection.TypeChecking.Format.errorPartFmt`.
+
 * Added new records to `Algebra.Bundles`:
   ```agda
   RawNearSemiring c ℓ : Set (suc (c ⊔ ℓ))

src/Reflection/TypeChecking/Format.agda

@@ -79,3 +79,7 @@ typeErrorFmt fmt = mapPrintf (lexer fmt) (typeError ∘ concat) (printf fmt)
 
 debugPrintFmt : String → ℕ → (fmt : String) → Printf (lexer fmt) (TC ⊤)
 debugPrintFmt tag lvl fmt = mapPrintf (lexer fmt) (debugPrint tag lvl ∘ concat) (printf fmt)
+
+-- Combine with "%e" format for nested format calls.
+errorPartFmt : (fmt : String) → Printf (lexer fmt) (List ErrorPart)
+errorPartFmt fmt = mapPrintf (lexer fmt) concat (printf fmt)

src/Reflection/TypeChecking/Monad.agda

@@ -33,7 +33,7 @@ open Builtin public
   renaming (returnTC to return)
 
 open Format public
-  using (typeErrorFmt; debugPrintFmt)
+  using (typeErrorFmt; debugPrintFmt; errorPartFmt)
 
 ------------------------------------------------------------------------
 -- Utility functions