docs: public static /*@pure@*/ String doubleToString(double value, int width,
  				      int afterDecimalPoint) {
      
      String tempString = doubleToString(value, afterDecimalPoint);
      char[] result;
      int dotPosition;
  
      if ((afterDecimalPoint >= width) 
          || (tempString.indexOf('E') != -1)) { // Protects sci notation
        return tempString;
      }
  
      // Initialize result
      result = new char[width];
      for (int i = 0; i < result.length; i++) {
        result[i] = ' ';
      }
  
      if (afterDecimalPoint > 0) {
        // Get position of decimal point and insert decimal point
        dotPosition = tempString.indexOf('.');
        if (dotPosition == -1) {
  	dotPosition = tempString.length();
        } else {
  	result[width - afterDecimalPoint - 1] = '.';
        }
      } else {
        dotPosition = tempString.length();
      }
      
  
      int offset = width - afterDecimalPoint - dotPosition;
      if (afterDecimalPoint > 0) {
        offset--;
      }
  
      // Not enough room to decimal align within the supplied width
      if (offset < 0) {
        return tempString;
      }
  
      // Copy characters before decimal point
      for (int i = 0; i < dotPosition; i++) {
        result[offset + i] = tempString.charAt(i);
      }
  
      // Copy characters after decimal point
      for (int i = dotPosition + 1; i < tempString.length(); i++) {
        result[offset + i] = tempString.charAt(i);
      }
  
      return new String(result);
    }