jack.plugin.compile
Class PoGeneratorErrorHandler

java.lang.Object
  jml2b.util.Profiler
      jml2b.exceptions.ErrorHandler
          jack.plugin.compile.PoGeneratorErrorHandler

public class PoGeneratorErrorHandler

extends ErrorHandler

Error handler that adds markers for errors instead of just printing errors to stderr.

Author:

A. Requet, L. Burdy

Constructor Summary

PoGeneratorErrorHandler(org.eclipse.core.resources.IProject prj)

Method Summary

static java.lang.String

getRelativeFile(java.io.File root, java.io.File children) Return the path of children relative to root.

Methods inherited from class jml2b.exceptions.ErrorHandler

error, getErrorCount, getWarningCount, reset, setHandler, warning

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

PoGeneratorErrorHandler

public PoGeneratorErrorHandler(org.eclipse.core.resources.IProject prj)

Method Detail

getRelativeFile

public static java.lang.String getRelativeFile(java.io.File root,
                                               java.io.File children)

Return the path of children relative to root. Return null if children is not located in a subdirectory of root.