diff --git a/vdmj/documentation/DesignSpec.odt b/vdmj/documentation/DesignSpec.odt index f55505bff..65a64508f 100644 Binary files a/vdmj/documentation/DesignSpec.odt and b/vdmj/documentation/DesignSpec.odt differ diff --git a/vdmj/documentation/DesignSpec.pdf b/vdmj/documentation/DesignSpec.pdf index e7969cb19..8cd791b26 100644 Binary files a/vdmj/documentation/DesignSpec.pdf and b/vdmj/documentation/DesignSpec.pdf differ diff --git a/vdmj/documentation/PluginWritersGuide.odt b/vdmj/documentation/PluginWritersGuide.odt index 2ac214abf..248451c19 100644 Binary files a/vdmj/documentation/PluginWritersGuide.odt and b/vdmj/documentation/PluginWritersGuide.odt differ diff --git a/vdmj/documentation/PluginWritersGuide.pdf b/vdmj/documentation/PluginWritersGuide.pdf index deb00a061..f01dc56de 100644 Binary files a/vdmj/documentation/PluginWritersGuide.pdf and b/vdmj/documentation/PluginWritersGuide.pdf differ diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/Lifecycle.java b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/Lifecycle.java index 253364787..9090fd098 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/Lifecycle.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/Lifecycle.java @@ -146,8 +146,6 @@ else if (argv.contains("-vdmrt")) private void usage() { - List plugins = PluginRegistry.getInstance().getPlugins(); - println("Usage: VDMJ [-vdmsl | -vdmpp | -vdmrt] [] []"); println("-vdmsl: parse files as VDM-SL (default)"); println("-vdmpp: parse files as VDM++"); @@ -161,10 +159,7 @@ private void usage() println("-q: suppress information messages"); println("-verbose: display detailed startup information"); - for (AnalysisPlugin plugin: plugins) - { - plugin.usage(); - } + PluginRegistry.getInstance().usage(); System.exit(0); } @@ -268,10 +263,7 @@ protected void processArgs() } } - for (AnalysisPlugin plugin: PluginRegistry.getInstance().getPlugins()) - { - plugin.processArgs(argv); // In priority order - } + PluginRegistry.getInstance().processArgs(argv); // In priority order } protected void loadPlugins() diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/PluginRegistry.java b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/PluginRegistry.java index 77aebec57..9eeecaefd 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/PluginRegistry.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/PluginRegistry.java @@ -97,6 +97,22 @@ public List getPlugins() return sorted; } + public void usage() + { + for (AnalysisPlugin plugin: getPlugins()) + { + plugin.usage(); + } + } + + public void processArgs(List argv) + { + for (AnalysisPlugin plugin: getPlugins()) + { + plugin.processArgs(argv); // In priority order + } + } + public AnalysisCommand getCommand(String line) { String[] argv = line.split("\\s+");