Looks good to me. I left one minor comment in the PR.

The code for this issue is at
https://bitbucket.org/PatFer/downward/pull-requests/9 .

I'm happy with the changes. Any comments from the rest of the nosy people?

As summary from todays meeting:

We would like to have unique names within {Plugins, Predefinitions,
PluginGroups, PluginTypes}, but the names can be reused between those 4 groups.
 (we can have a plugin and predefinition of name ff).

Given that there are clashes where some text could mean a predefinition and
plugin, the predefinition will be chosen.

This also allows us to uniquely tell from name what plugin/predefinition it
refers to.

I like the suggestions. It would be tempting to also require that predefinitions
and plugins have disjoint names, but I think it would not be nice if users have
their predefinitions break just because someone later introduces a plugin that
happens to clash with that name. So I think it's good for predefinitions to have
priority. If we think of the command-line syntax as essentially Python syntax,
which is more or less already is, then this also agrees nicely with Python
semantics where I can write "h=ff()" to shadow a global function "h" if it exists.

The registry allows to reuse the same name for multiple plugins, if those
plugins are defined for different classes.
The same holds for predefinitions.
When a plugin is registered with its class and name, the DocStore overwrites any
previous Documentation stored for the same name, but possibly a different class.

Issues:
1. The DocStore overwritting shall not be
2. Ambigious keys are currently resolved through the expected class. This allows
reusing of keys in different context (e.g. max), but at the same time makes
understanding the arguments more confusing.

Solution suggestions:
Make those keys unique. For each cmd line argument, we know now what is means
without thinking about the context. The DocStore issue is also solved. If
multiple plugins have the same name, maybe they should have been given a better
name in the first place.

Shall the keys be unique between predefinitions and registry?
I think no. First, for backwards compatibility, users might have commands
defining known plugin names. Second, if we have ambigouities whether to use a
plugin or a predefinition at some place, we can define the easy rule, prefere
predefinitions, the user could always append '()' to make clear it is a plugin.
This does not infere with the DocStore issue, because predefinitions have
nothing to do with the documentation.


What are your thoughts?