intermed. ctxt ..: taken from fun init_scrstate decompose-isar
authorWalther Neuper <neuper@ist.tugraz.at>
Fri, 20 May 2011 08:32:57 +0200
branchdecompose-isar
changeset 420142863ed75b595
parent 42013 e9ef067fcf2a
child 42015 e9af6f1bc0fc
intermed. ctxt ..: taken from fun init_scrstate

but no preconds yet; done next
src/Tools/isac/Interpret/script.sml
src/Tools/isac/Interpret/solve.sml
test/Tools/isac/Test_Isac.thy
     1.1 --- a/src/Tools/isac/Interpret/script.sml	Fri May 20 08:20:53 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri May 20 08:32:57 2011 +0200
     1.3 @@ -1632,13 +1632,13 @@
     1.4    let
     1.5      val p' = par_pblobj pt p
     1.6  	  val thy = assoc_thy thy'
     1.7 -	  val PblObj {meth=itms, ctxt, ...} = get_obj I pt p'
     1.8 +	  val PblObj {meth=itms, ...} = get_obj I pt p'
     1.9  	  val metID = get_obj g_metID pt p'
    1.10  	  val {srls,scr,...} = get_met metID
    1.11    in
    1.12      if last_elem p = 0 (*nothing written to pt yet*)
    1.13      then
    1.14 -       let val (is, _, scr) = init_scrstate thy itms metID
    1.15 +       let val (is, ctxt, scr) = init_scrstate thy itms metID
    1.16  	     in (srls, (is, ctxt), scr) end
    1.17         else (srls, get_loc pt (p,p_), scr)
    1.18      end;
     2.1 --- a/src/Tools/isac/Interpret/solve.sml	Fri May 20 08:20:53 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/solve.sml	Fri May 20 08:32:57 2011 +0200
     2.3 @@ -144,10 +144,10 @@
     2.4     *)
     2.5  fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ptree, (pos as (p,_))) =
     2.6        let val {srls, ...} = get_met mI;
     2.7 -        val PblObj {meth=itms, ctxt, ...} = get_obj I pt p;
     2.8 +        val PblObj {meth=itms, ...} = get_obj I pt p;
     2.9          val thy' = get_obj g_domID pt p;
    2.10          val thy = assoc_thy thy';
    2.11 -        val (is as ScrState (env,_,_,_,_,_), _, sc) = init_scrstate thy itms mI;
    2.12 +        val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
    2.13          val ini = init_form thy sc env;
    2.14          val p = lev_dn p;
    2.15        in 
    2.16 @@ -274,11 +274,11 @@
    2.17  fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) =
    2.18        let
    2.19          val {srls,ppc,...} = get_met mI;
    2.20 -        val PblObj{meth=itms,origin=(oris,_,_),probl, ctxt, ...} = get_obj I pt p;
    2.21 +        val PblObj{meth=itms,origin=(oris,_,_),probl, ...} = get_obj I pt p;
    2.22          val itms = if itms <> [] then itms else complete_metitms oris probl [] ppc
    2.23          val thy' = get_obj g_domID pt p;
    2.24          val thy = assoc_thy thy';
    2.25 -        val (is as ScrState (env,_,_,_,_,_), _, scr) = init_scrstate thy itms mI;
    2.26 +        val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = init_scrstate thy itms mI;
    2.27          val ini = init_form thy scr env;
    2.28        in 
    2.29          case ini of
     3.1 --- a/test/Tools/isac/Test_Isac.thy	Fri May 20 08:20:53 2011 +0200
     3.2 +++ b/test/Tools/isac/Test_Isac.thy	Fri May 20 08:32:57 2011 +0200
     3.3 @@ -167,11 +167,6 @@
     3.4  ML {*
     3.5  *}
     3.6  ML {*
     3.7 -"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
     3.8 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
     3.9 -val (dI',pI',mI') =
    3.10 -  ("Test", ["sqroot-test","univariate","equation","test"],
    3.11 -   ["Test","squ-equ-test-subpbl1"]);
    3.12  *}
    3.13  ML {*
    3.14  *}