[isabelle-dev] Updating the current theory

[Michael Chan]

Hello,

I'm trying to update the current theory at the ML-level, e.g., creating 
a new table in the current theory.

For example, I have a function foo that does very much what 
Locale.register_locale does -- mainly, adding an entry into a table in 
the name space:

ML {*

val thy' = foo "x" @{theory};
Bar.get thy';

*}
thy' is therefore the updated theory (containing the new table). Let Bar be

structure Bar = Theory_Data (...)

So Bar.get thy' returns the Name_Space-table pair, in which the table is 
updated. This is fine if I call "Bar.get thy'" rather than "Bar.get 
@{theory}" because the current theory hasn't been updated. Now, what if 
I want the update to be made in the current theory such that I can get 
the updated table using Bar.get @{theory} instead?

What I have tried so far is to rebuild HOL with "datatype node = ..." 
and "val transaction ..." declared in signature TOPLEVEL and I transform 
the state using Isar.>>:

ML {*
val thy' = foo "x" @{theory};

val update_thy = Toplevel.transaction (fn int =>
    (fn Toplevel.Proof (prf, (finish,_)) => Toplevel.Proof (prf, 
(finish, Context.Theory thy'))
      | Toplevel.Theory (_,c) => Toplevel.Theory (Context.Theory thy', c)
      ));

val tr = Toplevel.name "test_tr" Toplevel.empty;
update_thy tr |> Isar.>>;

Bar.get @{theory};
*}

Here, Bar.get @{theory} still doesn't give me the updated table. 
However, if I undo one step and add

ML {*
Bar.get @{theory}
*}

then do one step, I see the updated table! I must be transforming the 
states incorrectly -- perhaps I shouldn't use Isar.>>? Also, I have a 
strong feeling that I'm not supposed to rebuild HOL with those hacks in 
TOPLEVEL...

Thanks for the help in advance.

Michael

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.