module FF.CSS.Spec.Safe.Value.Base where

open import Agda.Builtin.String using (String)
open import Agda.Primitive using (lzero) renaming (Set to Type)

record RawValue : Type lzero where
  constructor raw
  field rawValue : String

open RawValue public

renderRawValue : RawValue -> String
renderRawValue (raw value) = value

record Identifier : Type lzero where
  constructor ident
  field rawIdentifier : String

open Identifier public

renderIdentifier : Identifier -> String
renderIdentifier (ident value) = value

record CustomIdent : Type lzero where
  constructor customIdent
  field rawCustomIdent : String

open CustomIdent public

renderCustomIdent : CustomIdent -> String
renderCustomIdent (customIdent value) = value

record Url : Type lzero where
  constructor url
  field rawUrl : String

open Url public

renderUrl : Url -> String
renderUrl (url value) = value

record StringToken : Type lzero where
  constructor stringToken
  field rawStringToken : String

open StringToken public

renderStringToken : StringToken -> String
renderStringToken (stringToken value) = value