Lines Matching defs:width
64 /** The width (in characters) of line numbers (for padding). */
65 private static int width = 0;
138 * <dt><code>linenumbering.width</code></dt>
139 * <dd>Specifies the width of the numbers. If the specified width is too
159 width = 3;
174 // Get the width
175 varString = getVariable(context, "linenumbering.width");
177 width = Integer.parseInt(varString);
179 System.out.println("$linenumbering.width is not a number: " + varString);
204 * $linenumbering.width, $linenumbering.separator, and
214 * <p>Every line number will be right justified in a string 'width'
216 * environment is too long to fit in the specified width, the width
225 * are preceded by a 'width' blank string and the separator.</p>
255 int listingWidth = width < log10numLines+1
257 : width;