--- /dev/null
+#ifndef DIMEN_HH
+#define DIMEN_HH
+
+#include "real.hh"
+#include "string.hh"
+
+Real parse_dimen(String);
+Real convert_dimen(Real, String);
+String print_dimen(Real);
+
+#endif
+
--- /dev/null
+#include <ctype.h>
+#include "dimen.hh"
+#include "debug.hh"
+#include "string.hh"
+
+Real
+parse_dimen(String dim)
+{
+ int i=dim.len()-1;
+ const char *s = dim;
+ while (i > 0 && (isspace(s[i]) || isalpha(s[i])) ){
+ i--;
+ }
+ String unit(s + i+1);
+ return convert_dimen(dim.fvalue(), unit);
+}
+
+const Real CM_TO_PT=72/2.54;
+
+Real
+convert_dimen(Real quant, String unit)
+{
+ if (unit == "cm")
+ return quant * CM_TO_PT;
+ if (unit == "pt")
+ return quant;
+ if (unit == "mm")
+ return quant*CM_TO_PT/10;
+ if (unit == "in")
+ return quant * 72;
+ error ("unknown length unit: `" + unit+"'");
+}
+
+String
+print_dimen(Real r)
+{
+ String s(r);
+ s += "pt ";
+ return s;
+}
--- /dev/null
+#include "dimen.hh"
+#include "tex.hh"
+#include "symbol.hh"
+#include "const.hh"
+
+String
+vstrut(Real h)
+{
+ return String("\\vrule height ") + print_dimen(h) + "depth 0pt width 0pt";
+}
+
+
+static void
+substitute_arg(String& r, String arg)
+{
+ int p = r.pos('%');
+ if (!p ) return ;
+ else p--;
+ r = r.left(p) + arg + r.right(r.len() - p -1);
+}
+
+
+String
+substitute_args(String source, svec<String> args)
+{
+ String retval (source);
+ for (int i = 0 ; i < args.sz(); i++)
+ substitute_arg(retval, args[i]);
+ while (retval.pos('%'))
+ substitute_arg(retval, "");
+ return retval;
+}