[isabelle] ML - How to handle ERROR exception



Hi all,

I would like to learn a bit more about the ML basis of Isabelle.
Recently, I have tried to catch and handle the user exception "ERROR of
string" defined in exn.ML in the following example:

ML {*
       type isar_record =  {context: Proof.context, facts: thm list, goal:
thm}

       fun goal_display ctxt (isar_goal:isar_record) =
            Pretty.writeln(Goal_Display.pretty_goal ctxt (#goal(isar_goal)))
       handle Exn.ERROR _    =>   ();
*}

Now I would like to insert the function using ML_val and antiquotations
anywhere in a theory file, i.e. inside and outside of proofs:

ML_val {*
               goal_display @{context} @{Isar.goal}
             *}

However, the exception ERROR "No proof state" is printed as an error
message in Isabelle, although I’ve installed the corresponding error
handler. Am I doing something wrong here?

Thank you for your time and help!

Best regards,
Janik Benzin



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