lib/browser/GraphBrowser/AbstractFontMetrics.java
author blanchet
Tue, 22 Mar 2011 19:04:32 +0100
changeset 42064 f4e53c8630c0
parent 33686 8e33ca8832b1
permissions -rw-r--r--
added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13970
4aef7117817b cleanup, comments
kleing
parents: 13968
diff changeset
     1
/***************************************************************************
4aef7117817b cleanup, comments
kleing
parents: 13968
diff changeset
     2
  Title:      GraphBrowser/AWTFontMetrics.java
4aef7117817b cleanup, comments
kleing
parents: 13968
diff changeset
     3
  Author:     Gerwin Klein, TU Muenchen
4aef7117817b cleanup, comments
kleing
parents: 13968
diff changeset
     4
4aef7117817b cleanup, comments
kleing
parents: 13968
diff changeset
     5
  AbstractFontMetrics avoids dependency on java.awt.FontMetrics in 
4aef7117817b cleanup, comments
kleing
parents: 13968
diff changeset
     6
  batch mode.
4aef7117817b cleanup, comments
kleing
parents: 13968
diff changeset
     7
  
4aef7117817b cleanup, comments
kleing
parents: 13968
diff changeset
     8
***************************************************************************/
4aef7117817b cleanup, comments
kleing
parents: 13968
diff changeset
     9
13968
689868b99bde eliminated dependencies on AWT for batch mode
kleing
parents:
diff changeset
    10
package GraphBrowser;
689868b99bde eliminated dependencies on AWT for batch mode
kleing
parents:
diff changeset
    11
689868b99bde eliminated dependencies on AWT for batch mode
kleing
parents:
diff changeset
    12
public interface AbstractFontMetrics {
689868b99bde eliminated dependencies on AWT for batch mode
kleing
parents:
diff changeset
    13
  public int stringWidth(String str);
689868b99bde eliminated dependencies on AWT for batch mode
kleing
parents:
diff changeset
    14
  public int getAscent();
689868b99bde eliminated dependencies on AWT for batch mode
kleing
parents:
diff changeset
    15
  public int getDescent();
689868b99bde eliminated dependencies on AWT for batch mode
kleing
parents:
diff changeset
    16
}