Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] apparently spurious error re antiquotations

Email Gateway (Aug 22 2022 at 17:54):

From: Makarius <makarius@sketis.net>
On 14/08/18 06:40, Jeremy Dawson wrote:

I'm "use"-ing a file, and get the following error:

No context -- cannot expand ML antiquotations (line 1 of "hologic.ML")
Exception- ERROR "ML error" raised

The Poly/ML "use" function is for raw Standard ML.

Isabelle/ML works within a formal theory context, via ML/ML_file commands.

thirdly, is there a way of using antiquotations in isabelle console?

No. You should use Isabelle/jEdit for interacting with Isabelle/ML.

Makarius

Email Gateway (Aug 22 2022 at 18:16):

From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi,

I'm "use"-ing a file, and get the following error:

No context -- cannot expand ML antiquotations (line 1 of "hologic.ML")
Exception- ERROR "ML error" raised

Now, firstly, the line number is nonsense - I can add a whole lot of
blank lines at the start of the file, and the error message doesn't change

secondly, there aren't any antiquotations in the file (there were, but
I've cleaned them out)

thirdly, is there a way of using antiquotations in isabelle console?

I've found functions ML_Context.eval[_source][_in] some of which seem to
recognise antiquotations and some of which seem to remember declarations
made in the ML source given them, but none do both.

Cheers,

Jeremy

Last updated: Nov 21 2024 at 12:39 UTC