8 /** parameter substitution in TeXstrings.
9 this function provides a simple macro mechanism:
11 if source == "tex%bla%", then
12 substitute_args(source, {"X","Y"}) == "texXblaY"
15 substitute_args(String source
, Array
<String
> args
);
17 /// parameter substitution in TeXstrings
19 substitute_args(String source
, Array
<Scalar
> args
);
22 String
vstrut(Real h
);