[isabelle] Methods with informative failure messages


I would like to implement a method that gives an informative error message
when application fails (e.g., imagine an algebra tactic returning "subgoal
should not contain <=" or something like that).

I see possibilities how a method can indicate a failure:

   - Raise an exception
   - Return a (Seq.Error (K "error message")) result.
   - Return Seq.empty (this is what is done by most methods)

According to my experiments, the first two options are not suitable because
they break method combinators like "method+" and "method?" (I would need
that these will suppress the error.) And the third option does not support
giving an error message.

Is there any best practice how to return informative messages on method
I feel that this would be very helpful for the user of the method because
often one has to do a lot of try and error to find out why a method didn't
work on a given subgoal.

Best wishes,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.