lingenic_text-eaw

--  Copyright © 2026 Lingenic LLC. All rights reserved.
--  Licensed under the Lingenic Source-Available License v2.3.
--  Production use requires a separate license from Licensor.
--  See LICENSE.md and COPYRIGHT in the project root.
--

-------------------------------------------------------------------------------
--  Lingenic-Text
--  Formally Verified Unicode Text Processing Library
--
--  East Asian Width display width (UAX #11).
--
--  Provides O(1) display width lookup for any codepoint.
--  Wide and Fullwidth characters return 2; all others return 1.
-------------------------------------------------------------------------------

with Lingenic_Text.EAW_Spec;
with Lingenic_Text.Properties;

package Lingenic_Text.EAW
   with SPARK_Mode
is

   ---------------------------------------------------------------------------
   --  Display_Width
   --
   --  Returns the display width of a codepoint in fixed-pitch cells.
   --  Wide (W) and Fullwidth (F) characters return 2.
   --  All others (Neutral, Ambiguous, Halfwidth, Narrow) return 1.
   --
   --  Platinum postcondition: the result IS the Cell_Width of the
   --  codepoint's East_Asian_Width property per the ghost spec.
   ---------------------------------------------------------------------------

   function Display_Width (CP : Codepoint) return Natural
     with Pre  => Properties.Initialized,
          Post => Display_Width'Result =
                    EAW_Spec.Cell_Width
                      (Properties.EAW_To_Abstract (Properties.Get_EAW (CP)));

end Lingenic_Text.EAW;