Texttag.Theme
Such a theme associates properties to text tags. These properties are used by Textview.textview
widget to display characters according to their tags. A theme also has properties, to get default values for properties not associated to text tags.
val pp : Stdlib.Format.formatter -> t -> unit
Initialization. It is called by App.init
.
val default : t
The default tag theme, with name "default"
.
val name : t -> string
Get theme name.
val get_by_name : string -> t option
Get theme by name, if it exists.
create name
creates a new theme. Optional arguments:
tags
: initialize theme with a mapping of text tags to properties,props
: global properties of theme.If a theme with the same name
already exists, a warning is issued and the existing theme is returned.
opt_props theme tag
returns properties of tag
in theme
, if tag is defined in theme.
tag_props theme tag
gets the properties of tag
in theme
. If tag
has no properties, then an empty Props.t
is associated to this tag in theme
and is returned.
val set_tag_prop : t -> T.t -> 'a Props.prop -> 'a -> unit
set_tag_prop theme tag p v
sets value v
to property p
of tag
in theme
.
merge_tag_props theme set props
merge tags properties with initial props
properties. Properties of first created tags are merged first. This function is used by Textview.textview
widget to compute the properties of a character according to its tags.
get_or_create name
gets theme with given name
if it exists, or else create it. Optional arguments:
tags
: a mapping of text tags to properties. It is set as initial map if theme is created. If theme already exists, properties of each tag in the theme are merged with the properties of the same tag in the map.props
: global properties of theme. If the theme already exists, its properties are merged with props
.val prop : string Props.prop
Property "tagtheme"
to store the name of the tag theme. Default is "default"
. Inherited.
val to_json : t -> Yojson.Safe.t
to_json t
returns a JSON representation of t
.
val from_json : string -> Yojson.Safe.t -> t
from_json name json
creates theme name
and sets properties and text tags properties from json
description. The function uses get_or_create
so an existing theme with the same name will be modified by this function.