Re: [isabelle] File.use function
On Sun, 30 Apr 2006, Clément Hurlin wrote:
> I'm trying to use a file containing ML code using "File.use".
Why use the internal File.use instead of the toplevel use (which is
> The file used contained the following code :
> val proof_congr = X
> val proof_inst = Y
> And at the ML level, I do :
> val proof_congr = 
> val proof_inst = 
> val _ = File.use (Path.unpack proof_hints_fn)
> Even if the *isabelle* buffer in proofgeneral shows that proof_congr and
> proof_inst are filled with X and Y, it is actually not the case at the
> ML level : proof_congr and proof_inst are still the empty list :O( Why ?
I do not fully understand your setup. There might be a misunderstanding
concerning the meaning of ML toplevel declarations: proof_congr and
proof_inst cannot be ``filled'' with other values, because they are
statically fixed bindings to immutable values. Maybe you were actually
thinking about assignable references.
On the other hand, you may actually want to store your data within the
theory or proof context of Isabelle in a value oriented fashion. See
TheoryDataFun/ProofDataFun in src/Pure/context.ML and existing
applications in the sources. Especially see src/ZF/Tools/typechk.ML in
the development version for an up-to-date example.
This archive was generated by a fusion of
Pipermail (Mailman edition) and