1.1 --- a/src/Tools/isac/Interpret/ctree.sml	Fri May 13 11:45:07 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Fri May 13 14:15:59 2011 +0200
     1.3 @@ -954,6 +954,8 @@
     1.4    | g_domID  _ = raise PTREE "g_metID not for PrfObj";
     1.5  fun g_metID  (PblObj {spec = (_,_,m),...}) = m
     1.6    | g_metID  _ = raise PTREE "g_metID not for PrfObj";
     1.7 +fun g_ctxt    (PblObj {ctxt, ...}) = ctxt
     1.8 +  | g_ctxt    _ = raise PTREE "g_ctxt not for PrfObj"; 
     1.9  fun g_env    (PblObj {env,...}) = env
    1.10    | g_env    _ = raise PTREE "g_env not for PrfObj"; 
    1.11  fun g_loc    (PblObj {loc = l,...}) = l
    1.12 @@ -1174,14 +1176,19 @@
    1.13      PrfObj {cell=cell,form=form,tac=tac,loc=loc,
    1.14  	    branch= b,result=result,ostate=ostate};
    1.15  
    1.16 +fun repl_ctxt x
    1.17 +      (PblObj {cell, origin, fmz, spec, probl, meth,
    1.18 +       ctxt=_, env, loc, branch, result, ostate}) =
    1.19 +         PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
    1.20 +          ctxt=x, env=env, loc=loc, branch=branch, result=result, ostate=ostate}
    1.21 +    | repl_ctxt _ _ = raise PTREE "repl_env takes no PrfObj";
    1.22 +
    1.23  fun repl_env e
    1.24 -  (PblObj {cell=cell,origin=origin,fmz=fmz,
    1.25 -	   spec=spec,probl=probl,meth=meth,ctxt=ctxt,env=_,loc=loc,
    1.26 -	   branch=branch,result=result,ostate=ostate}) =
    1.27 -  PblObj {cell=cell,origin=origin,fmz=fmz,spec=spec,probl=probl,
    1.28 -	  meth=meth,ctxt=ctxt,env=e,loc=loc,branch=branch,
    1.29 -	  result=result,ostate=ostate}
    1.30 -  | repl_env _ _ = raise PTREE "repl_ets takes no PrfObj";
    1.31 +      (PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
    1.32 +       ctxt=ctxt, env=_, loc=loc, branch=branch, result=result, ostate=ostate}) =
    1.33 +         PblObj {cell=cell, origin=origin, fmz=fmz, spec=spec, probl=probl, meth=meth,
    1.34 +          ctxt=ctxt, env=e, loc=loc, branch=branch, result=result, ostate=ostate}
    1.35 +    | repl_env _ _ = raise PTREE "repl_env takes no PrfObj";
    1.36  
    1.37  fun repl_oris oris
    1.38    (PblObj {cell=cell,origin=(_,spe,hdf),fmz=fmz,
    1.39 @@ -1271,6 +1278,7 @@
    1.40                                         1.00 not used anymore*)
    1.41  
    1.42  (*FIXME.WN.12.03: update_X X pos pt -> pt could be chained by o (efficiency?)*)
    1.43 +fun update_ctxt   pt pos x = appl_obj (repl_ctxt   x) pt pos;
    1.44  fun update_env    pt pos x = appl_obj (repl_env    x) pt pos;
    1.45  fun update_domID  pt pos x = appl_obj (repl_domID  x) pt pos;
    1.46  fun update_pblID  pt pos x = appl_obj (repl_pblID  x) pt pos;

     2.1 --- a/test/Tools/isac/Interpret/ctree.sml	Fri May 13 11:45:07 2011 +0200
     2.2 +++ b/test/Tools/isac/Interpret/ctree.sml	Fri May 13 14:15:59 2011 +0200
     2.3 @@ -10,6 +10,7 @@
     2.4  "table of contents -----------------------------------------------";
     2.5  "-----------------------------------------------------------------";
     2.6  "-----------------------------------------------------------------";
     2.7 +"-------------- fun update_ctxt, fun g_ctxt ----------------------";
     2.8  "-------------- check positions in miniscript --------------------";
     2.9  "-------------- get_allpos' (from ptree above)--------------------";
    2.10  (**#####################################################################(**)
    2.11 @@ -58,6 +59,18 @@
    2.12  "-----------------------------------------------------------------";
    2.13  
    2.14  
    2.15 +"-------------- fun update_ctxt, fun g_ctxt ----------------------";
    2.16 +"-------------- fun update_ctxt, fun g_ctxt ----------------------";
    2.17 +"-------------- fun update_ctxt, fun g_ctxt ----------------------";
    2.18 +val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) EmptyPtree;
    2.19 +if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name)
    2.20 +    = "Interpret"
    2.21 +then () else error "TODO";
    2.22 +val pt = update_ctxt pt [] (ProofContext.init_global @{theory "Isac"});
    2.23 +if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name)
    2.24 +    = "Isac"
    2.25 +then () else error "TODO";
    2.26 +
    2.27  "-------------- check positions in miniscript --------------------";
    2.28  "-------------- check positions in miniscript --------------------";
    2.29  "-------------- check positions in miniscript --------------------";

     3.1 --- a/test/Tools/isac/Test_Isac.thy	Fri May 13 11:45:07 2011 +0200
     3.2 +++ b/test/Tools/isac/Test_Isac.thy	Fri May 13 14:15:59 2011 +0200
     3.3 @@ -117,7 +117,33 @@
     3.4    ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl %%%%%%%%%%%%%%%%%%%%%%%";*}
     3.5    ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
     3.6    use "Interpret/mstools.sml"       (*new 2010*)
     3.7 -  use "Interpret/ctree.sml"         (*!...see(25)*)
     3.8 +ML {*
     3.9 +*}
    3.10 +ML {*
    3.11 +*}
    3.12 +ML {*
    3.13 +*}
    3.14 +ML {*
    3.15 +*}
    3.16 +ML {*
    3.17 +*}
    3.18 +ML {*
    3.19 +
    3.20 +*}
    3.21 +ML {*
    3.22 +*}
    3.23 +ML {*
    3.24 +*}
    3.25 +ML {*
    3.26 +*}
    3.27 +ML {*
    3.28 +
    3.29 +*}
    3.30 +ML {*
    3.31 +*}
    3.32 +ML {*
    3.33 +*}
    3.34 +  use "Interpret/ctree.sml"         (*!...!see(25)*)
    3.35    use "Interpret/ptyps.sml"         (*    *)
    3.36  (*use "Interpret/generate.sml"        new 2011*)
    3.37    use "Interpret/calchead.sml"      (*!    *)