# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1305288959 -7200
# Node ID 235f3990c9b70e881112db0394ebe8d5756aea2c
# Parent  0a13bda82a57c0d30e062b2ae102c0683a9b9a28
tuned

diff -r 0a13bda82a57 -r 235f3990c9b7 src/Tools/isac/Interpret/ctree.sml
--- a/src/Tools/isac/Interpret/ctree.sml	Fri May 13 11:45:07 2011 +0200
+++ b/src/Tools/isac/Interpret/ctree.sml	Fri May 13 14:15:59 2011 +0200
@@ -954,6 +954,8 @@
   | g_domID  _ = raise PTREE "g_metID not for PrfObj";
 fun g_metID  (PblObj {spec = (_,_,m),...}) = m
   | g_metID  _ = raise PTREE "g_metID not for PrfObj";
+fun g_ctxt    (PblObj {ctxt, ...}) = ctxt
+  | g_ctxt    _ = raise PTREE "g_ctxt not for PrfObj"; 
 fun g_env    (PblObj {env,...}) = env
   | g_env    _ = raise PTREE "g_env not for PrfObj"; 
 fun g_loc    (PblObj {loc = l,...}) = l
@@ -1174,14 +1176,19 @@
     PrfObj {cell=cell,form=form,tac=tac,loc=loc,
 	    branch= b,result=result,ostate=ostate};
 
+fun repl_ctxt x
+      (PblObj {cell, origin, fmz, spec, probl, meth,
+       ctxt=_, env, loc, branch, result, ostate}) =
+         PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
+          ctxt=x, env=env, loc=loc, branch=branch, result=result, ostate=ostate}
+    | repl_ctxt _ _ = raise PTREE "repl_env takes no PrfObj";
+
 fun repl_env e
-  (PblObj {cell=cell,origin=origin,fmz=fmz,
-	   spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=_,loc=loc,
-	   branch=branch,result=result,ostate=ostate}) =
-  PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
-	  meth=meth,ctxt=ctxt,env=e,loc=loc,branch=branch,
-	  result=result,ostate=ostate}
-  | repl_env _ _ = raise PTREE "repl_ets takes no PrfObj";
+      (PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
+       ctxt=ctxt, env=_, loc=loc, branch=branch, result=result, ostate=ostate}) =
+         PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
+          ctxt=ctxt, env=e, loc=loc, branch=branch, result=result, ostate=ostate}
+    | repl_env _ _ = raise PTREE "repl_env takes no PrfObj";
 
 fun repl_oris oris
   (PblObj {cell=cell,origin=(_,spe,hdf),fmz=fmz,
@@ -1271,6 +1278,7 @@
                                        1.00 not used anymore*)
 
 (*FIXME.WN.12.03: update_X X pos pt -> pt could be chained by o (efficiency?)*)
+fun update_ctxt   pt pos x = appl_obj (repl_ctxt   x) pt pos;
 fun update_env    pt pos x = appl_obj (repl_env    x) pt pos;
 fun update_domID  pt pos x = appl_obj (repl_domID  x) pt pos;
 fun update_pblID  pt pos x = appl_obj (repl_pblID  x) pt pos;
diff -r 0a13bda82a57 -r 235f3990c9b7 test/Tools/isac/Interpret/ctree.sml
--- a/test/Tools/isac/Interpret/ctree.sml	Fri May 13 11:45:07 2011 +0200
+++ b/test/Tools/isac/Interpret/ctree.sml	Fri May 13 14:15:59 2011 +0200
@@ -10,6 +10,7 @@
 "table of contents -----------------------------------------------";
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
+"-------------- fun update_ctxt, fun g_ctxt ----------------------";
 "-------------- check positions in miniscript --------------------";
 "-------------- get_allpos' (from ptree above)--------------------";
 (**#####################################################################(**)
@@ -58,6 +59,18 @@
 "-----------------------------------------------------------------";
 
 
+"-------------- fun update_ctxt, fun g_ctxt ----------------------";
+"-------------- fun update_ctxt, fun g_ctxt ----------------------";
+"-------------- fun update_ctxt, fun g_ctxt ----------------------";
+val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) EmptyPtree;
+if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name)
+    = "Interpret"
+then () else error "TODO";
+val pt = update_ctxt pt [] (ProofContext.init_global @{theory "Isac"});
+if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name)
+    = "Isac"
+then () else error "TODO";
+
 "-------------- check positions in miniscript --------------------";
 "-------------- check positions in miniscript --------------------";
 "-------------- check positions in miniscript --------------------";
diff -r 0a13bda82a57 -r 235f3990c9b7 test/Tools/isac/Test_Isac.thy
--- a/test/Tools/isac/Test_Isac.thy	Fri May 13 11:45:07 2011 +0200
+++ b/test/Tools/isac/Test_Isac.thy	Fri May 13 14:15:59 2011 +0200
@@ -117,7 +117,33 @@
   ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*}
   ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
   use "Interpret/mstools.sml"       (*new 2010*)
-  use "Interpret/ctree.sml"         (*!...see(25)*)
+ML {*
+*}
+ML {*
+*}
+ML {*
+*}
+ML {*
+*}
+ML {*
+*}
+ML {*
+
+*}
+ML {*
+*}
+ML {*
+*}
+ML {*
+*}
+ML {*
+
+*}
+ML {*
+*}
+ML {*
+*}
+  use "Interpret/ctree.sml"         (*!...!see(25)*)
   use "Interpret/ptyps.sml"         (*    *)
 (*use "Interpret/generate.sml"        new 2011*)
   use "Interpret/calchead.sml"      (*!    *)