diff --git a/src/org/rascalmpl/debug/IRascalMonitor.java b/src/org/rascalmpl/debug/IRascalMonitor.java index ec87c7f114a..2709021dc18 100644 --- a/src/org/rascalmpl/debug/IRascalMonitor.java +++ b/src/org/rascalmpl/debug/IRascalMonitor.java @@ -40,6 +40,10 @@ default void jobStart(String name, int totalWork) { jobStart(name, 1, totalWork); } + /** + * This utility method is not to be implemented by clients. It's a convenience + * function that helps to guarantee jobs that are started, are always ended. + */ default void job(String name, int totalWork, Supplier block) { boolean result = false; try { @@ -50,7 +54,13 @@ default void job(String name, int totalWork, Supplier block) { jobEnd(name, result); } } - + + /** + * This utility method is not to be implemented by clients. It's a convenience + * function that helps to guarantee jobs that are started, are always ended. + * Also it provides easy access to the name of the current job, such that + * this "magic" constant does not need to be repeated or stored elsewhere. + */ default void job(String name, int totalWork, Function block) { boolean result = false; try {