lingenic_text-scx_spec

--  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
--
--  Body for Scx_Spec — contains only the regular-function body of
--  Expected_Scx_Has_From.  All other functions in Scx_Spec are expression
--  functions whose bodies live in the spec.
-------------------------------------------------------------------------------

package body Lingenic_Text.Scx_Spec
   with SPARK_Mode
is

   function Expected_Scx_Has_From
     (Scx_Src      : Byte_Array;
      Pos          : Positive;
      CP           : Codepoint;
      Script_Src   : Byte_Array;
      Script_Names : UCD_Parser.Value_Name_Array;
      Script_Idx   : UCD_Parser.Property_Index) return Boolean
   is
   begin
      if Pos > Scx_Src'Last then
         return False;
      else
         return Expected_Scx_Has
           (Scx_Src, Pos, CP, Script_Src, Script_Names, Script_Idx);
      end if;
   end Expected_Scx_Has_From;

end Lingenic_Text.Scx_Spec;