Add String formatting

Add String formatting by extending the String object with a
format method.

Now we can do stuff like "Text: %s, %d".format(somevar, 5)

This is required for proper translation of some strings.

https://bugzilla.gnome.org/show_bug.cgi?id=595661

js/ui/environment.js

@@ -4,6 +4,8 @@ const St = imports.gi.St;
 
 const Tweener = imports.ui.tweener;
 
+const Format = imports.misc.format;
+
 // "monkey patch" in some varargs ClutterContainer methods; we need
 // to do this per-container class since there is no representation
 // of interfaces in Javascript
@@ -30,4 +32,5 @@ _patchContainerClass(St.Table);
 
 function init() {
     Tweener.init();
+    String.prototype.format = Format.format;
 }