|
The DragNDropInstantiator interpretes drag'n drop actions as taclet
instantiations. The behaviour is described below (excluding some
"optimisation" details)
Let "source" denote the formula/term which is dragged and dropped on another
term called "target". The DragNDropInstantiation of a taclet "t" is now
defined as follows:
- t must have exactly one formula/term in the find part and
assumes sequent (in particular it must have an assumes -part)
- and
- if t's goal descriptions do not contain any replacewith then
"source" is matched against the find part of the taclet and
"target" has to match the "if" part.
- if t's goal descriptions contain at least one replacewith
then "target" is matched against the find part and "source"
against the assumes part
*
or
- t must have a find part, no assumes and at least one
addrule. In this case source is merged against find part and
target has to be the complete sequent. Dropping on the sequent arrow is
interpreted as applying an addrule(treats hide rules)
The DragNDropInstantiator now determines all taclets, which have a valid
drag'n drop instantiation for a given (source, target) position pair. If
there is only one taclet with a valid dnd-instantiation this one is executed
otherwise the user is presented a list of possible taclets from which she/he
can select one.
|
