Homestyx hydra

R1:28fe9f4eca8c

User preferences ported from tools

Summary:

Internal tools, e.g., differential and diffusion have user defined
preferences for monospaced font and the option for showing either the
name of the tool or the glyph of the tool in the title.

These preferences were ported to phabricator. These preferences can be
modified in /preferences/ and they both affect diffusion and differential
at the moment.

Test Plan:

* Created an empty database
* Loaded /preferences/ and modified the monospaced font and clicked…
Repository: R1 hydra
Commit Date: Mar 31 2011