I'm fine with separate exceptions for these two if we make a common base
class so we can catch them together if we ever want to.
On Mar 7, 2014 11:36 AM, "Yilong Li" <notifications@github.com> wrote:

> In
> src/javasources/KTool/src/org/kframework/backend/java/builtins/MetaK.java:
>
> > +     * Checks if the subject term matches the pattern.
> > +     *
> > +     * @param subject
> > +     *            the subject term
> > +     * @param pattern
> > +     *            the pattern term
> > +     * @param context
> > +     *            the term context
> > +     * @return {@link BoolToken#TRUE} if the two terms can be matched;
> > +     *         otherwise, {@link BoolToken#FALSE}
> > +     */
> > +    public static BoolToken matchable(Term subject, Term pattern, TermContext context) {
> > +        PatternMatcher matcher = new PatternMatcher(context);
> > +        try {
> > +            matcher.match(subject, pattern);
> > +        } catch (PatternMatchingFailure e) {
>
> I can combine UnificationFailure and PatternMatchingFailure but I prefer
> to keep it this way.
>
> --
> Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/270/files#r10396456>
> .
>