8 /// parameter substitution in TeXstrings
10 this function provides a simple macro mechanism:
12 if source == "tex%bla%", then
13 substitute_args(source, {"X","Y"}) == "texXblaY"
16 substitute_args(String source, Array<String> args);
18 /// parameter substitution in TeXstrings
20 substitute_args(String source, Array<Scalar> args);
23 String vstrut(Real h);