1.1 --- a/src/Tools/isac/Frontend/interface.sml	Fri Apr 08 15:16:08 2011 +0200
     1.2 +++ b/src/Tools/isac/Frontend/interface.sml	Mon Apr 11 12:56:57 2011 +0200
     1.3 @@ -412,7 +412,7 @@
     1.4  	 else if no_thycontext guh then message2xml cI ("no thy-context for '"^
     1.5  							guh ^ "'")
     1.6  	 else let val (ptp as (pt,pold),_) = get_calc cI
     1.7 -		  val (is,_) = get_istate pt ip
     1.8 +		  val is = get_istate pt ip
     1.9  		  val subs = subs_from is "dummy" guh
    1.10  		  val tac = guh2rewtac guh subs
    1.11  	      in case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
    1.12 @@ -783,7 +783,7 @@
    1.13  	 else if no_thycontext guh then message2xml cI ("no thy-context for '"^
    1.14  							guh ^ "'")
    1.15  	 else let val (ptp as (pt,_),_) = get_calc cI
    1.16 -		  val (is,_) = get_istate pt pos
    1.17 +		  val is = get_istate pt pos
    1.18  		  val subs = subs_from is "dummy" guh
    1.19  		  val tac = guh2rewtac guh subs
    1.20  	      in contextthyOK2xml cI (context_thy (pt, pos) tac) end

     2.1 --- a/src/Tools/isac/Interpret/calchead.sml	Fri Apr 08 15:16:08 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Mon Apr 11 12:56:57 2011 +0200
     2.3 @@ -802,9 +802,9 @@
     2.4              end
     2.5        end
     2.6    | appl_add ctxt sel oris ppc pbt str =
     2.7 -      case parse (ProofContext.theory_of ctxt) str of
     2.8 +      case parseNEW ctxt str of
     2.9            NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
    2.10 -        | SOME t => case is_known ctxt sel oris (term_of t) of
    2.11 +        | SOME t => case is_known ctxt sel oris t of
    2.12              ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
    2.13                ("", itm) => Add itm
    2.14                | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
    2.15 @@ -1015,7 +1015,8 @@
    2.16        val cpI = if pI = e_pblID then pI' else pI;
    2.17        val cmI = if mI = e_metID then mI' else mI;
    2.18        val {ppc,pre,prls,...} = get_met cmI;
    2.19 -    in case appl_add (thy2ctxt thy) sel oris met ppc ct of
    2.20 +      val ctxt = get_ctxt pt (p,Met);
    2.21 +    in case appl_add ctxt sel oris met ppc ct of
    2.22        Add itm (*..union old input *) =>
    2.23  	let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
    2.24                 *)
    2.25 @@ -1048,7 +1049,7 @@
    2.26      end
    2.27  (* val (p,_) = p;
    2.28     *)
    2.29 -| specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt = 
    2.30 +| specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt = 
    2.31      let
    2.32        val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
    2.33  		  probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
    2.34 @@ -1056,7 +1057,8 @@
    2.35        val cpI = if pI = e_pblID then pI' else pI;
    2.36        val cmI = if mI = e_metID then mI' else mI;
    2.37        val {ppc,where_,prls,...} = get_pbt cpI;
    2.38 -    in case appl_add (thy2ctxt thy) sel oris pbl ppc ct of
    2.39 +      val ctxt = get_ctxt pt pos;
    2.40 +    in case appl_add ctxt sel oris pbl ppc ct of
    2.41        Add itm (*..union old input *) =>
    2.42        (* val Add itm = appl_add thy sel oris pbl ppc ct;
    2.43           *)
    2.44 @@ -1109,9 +1111,9 @@
    2.45  fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)= 
    2.46    let          (* either """"""""""""""" all empty or complete *)
    2.47      val thy = assoc_thy dI';
    2.48 -    val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
    2.49 -	       else pI' |> #ppc o get_pbt |> prep_ori fmz thy |> #1;
    2.50 -    val (pt,c) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz,(dI',pI',mI'))
    2.51 +    val (oris, ctxt) = if dI' = e_domID orelse pI' = e_pblID then ([], e_ctxt)
    2.52 +	       else pI' |> #ppc o get_pbt |> prep_ori fmz thy;
    2.53 +    val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
    2.54  				 (oris,(dI',pI',mI'),e_term);
    2.55      val {ppc,prls,where_,...} = get_pbt pI'
    2.56      (*val pbl = init_pbl ppc;  WN.9.03: done in Model/Refine_Problem
    2.57 @@ -1288,7 +1290,8 @@
    2.58  		  probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
    2.59        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    2.60        val cpI = if pI = e_pblID then pI' else pI;
    2.61 -    in case appl_add (thy2ctxt thy) sel oris pbl ((#ppc o get_pbt) cpI) ct of
    2.62 +      val ctxt = get_ctxt pt (p, Pbl);
    2.63 +    in case appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct of
    2.64  	   Add itm (*..union old input *) =>
    2.65  (* val Add itm = appl_add thy sel oris pbl ppc ct;
    2.66     *)
    2.67 @@ -1321,7 +1324,8 @@
    2.68  		  probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
    2.69        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
    2.70        val cmI = if mI = e_metID then mI' else mI;
    2.71 -    in case appl_add (thy2ctxt thy) sel oris met ((#ppc o get_met) cmI) ct of
    2.72 +      val ctxt = get_ctxt pt (p,Met);
    2.73 +    in case appl_add ctxt sel oris met ((#ppc o get_met) cmI) ct of
    2.74        Add itm (*..union old input *) =>
    2.75  	let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
    2.76                 *)
    2.77 @@ -1573,20 +1577,20 @@
    2.78    | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) = 
    2.79      let           (* both """"""""""""""""""""""""" either empty or complete *)
    2.80  	val thy = assoc_thy dI
    2.81 -	val (pI, pors, mI) = 
    2.82 +	val (pI, (pors, pctxt), mI) = 
    2.83  	    if mI = ["no_met"] 
    2.84 -	    then let val pors = get_pbt pI |> #ppc |> prep_ori fmz thy |> #1;
    2.85 +	    then let val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
    2.86  		     val pI' = refine_ori' pors pI;
    2.87 -		 in (pI', pors(*refinement over models with diff.precond only*),
    2.88 +		 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
    2.89  		     (hd o #met o get_pbt) pI') end
    2.90 -	    else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy |> #1, mI)
    2.91 +	    else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
    2.92  	val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
    2.93  	val dI = theory2theory' (maxthy thy thy');
    2.94  	val hdl = case cas of
    2.95  		      NONE => pblterm dI pI
    2.96  		    | SOME t => subst_atomic ((vars_of_pbl_' ppc) 
    2.97  						  ~~~ vals_of_oris pors) t;
    2.98 -        val (pt, _) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz, (dI, pI, mI))
    2.99 +        val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
   2.100  				      (pors, (dI, pI, mI), hdl)
   2.101      in ((pt, ([], Pbl)), 
   2.102          fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate

     3.1 --- a/src/Tools/isac/Interpret/ctree.sml	Fri Apr 08 15:16:08 2011 +0200
     3.2 +++ b/src/Tools/isac/Interpret/ctree.sml	Mon Apr 11 12:56:57 2011 +0200
     3.3 @@ -1344,7 +1344,8 @@
     3.4  	 (NONE  , SOME i) => i (*13.8.02 just copied from ^^^: too liberal ?*)
     3.5         | (NONE  , NONE) => (e_istate, e_ctxt)
     3.6         | (SOME i, _) => i);
     3.7 -val get_istate = get_loc; (*3.5.02*)
     3.8 +fun get_istate pt p = get_loc pt p |> #1;
     3.9 +fun get_ctxt pt p = get_loc pt p |> #2;
    3.10  
    3.11  (*.collect the assumptions within a problem up to a certain position.*)
    3.12  type asms = (term * pos) list;(*WN0502 should be (pos' * term) list

     4.1 --- a/src/Tools/isac/Interpret/script.sml	Fri Apr 08 15:16:08 2011 +0200
     4.2 +++ b/src/Tools/isac/Interpret/script.sml	Mon Apr 11 12:56:57 2011 +0200
     4.3 @@ -1851,12 +1851,12 @@
     4.4  	   in (*if last_elem p = 0 (*nothing written to pt yet*)
     4.5  	      then let val (is, ctxt, sc) = init_scrstate thy itms metID
     4.6  		   in (srls, is, sc) end
     4.7 -	      else*) (srls, get_istate pt (p,p_), (#scr o get_met) metID)
     4.8 +	      else*) (srls, get_loc pt (p,p_), (#scr o get_met) metID)
     4.9  	   end
    4.10         else (*3*)
    4.11  	   (e_rls, (*FIXME: get from pbl or met !!!
    4.12  		    unused for Rrls in locate_gen, next_tac*)
    4.13 -	    get_istate pt (p,p_),
    4.14 +	    get_loc pt (p,p_),
    4.15  	    case rls' of
    4.16  		Rls {scr=scr,...} => scr
    4.17  	      | Seq {scr=scr,...} => scr
    4.18 @@ -1873,7 +1873,7 @@
    4.19      in if last_elem p = 0 (*nothing written to pt yet*)
    4.20         then let val (is, ctxt, scr) = init_scrstate thy itms metID
    4.21  	    in (srls, (is, ctxt), scr) end
    4.22 -       else (srls, get_istate pt (p,p_), scr)
    4.23 +       else (srls, get_loc pt (p,p_), scr)
    4.24      end;
    4.25      
    4.26  (*.get the stactics and problems of a script as tacs
    4.27 @@ -1898,7 +1898,7 @@
    4.28  	val metID' =if metID =e_metID then(thd3 o snd3)(get_obj g_origin pt pp)
    4.29  		     else metID
    4.30  	val {scr=Script sc,srls,...} = get_met metID'
    4.31 -	val (ScrState (env,_,a,v,_,_), ctxt) = get_istate pt (p,p_);
    4.32 +	val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_);
    4.33      in map ((stac2tac pt thy) o rep_stacexpr o #2 o
    4.34  	    (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc) end;
    4.35  (*
    4.36 @@ -1925,7 +1925,7 @@
    4.37  			then (thd3 o snd3) (get_obj g_origin pt pp)
    4.38  			else metID
    4.39  	    val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'
    4.40 -	    val (ScrState (env,_,a,v,_,_), ctxt) = get_istate pt (p,p_)
    4.41 +	    val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
    4.42  	    val alltacs = (*we expect at least 1 stac in a script*)
    4.43  		map ((stac2tac pt thy) o rep_stacexpr o #2 o
    4.44  		     (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)

     5.1 --- a/src/Tools/isac/Interpret/solve.sml	Fri Apr 08 15:16:08 2011 +0200
     5.2 +++ b/src/Tools/isac/Interpret/solve.sml	Mon Apr 11 12:56:57 2011 +0200
     5.3 @@ -135,7 +135,7 @@
     5.4  
     5.5  
     5.6  fun step2taci ((tac_, _, pt, p, _):step) = (*FIXXME.040312: redesign step*)
     5.7 -    (tac_2tac tac_, tac_, (p, get_istate pt p)):taci;
     5.8 +    (tac_2tac tac_, tac_, (p, get_loc pt p)):taci;
     5.9  
    5.10  
    5.11  (*FIXME.WN050821 compare solve ... nxt_solv*)
    5.12 @@ -204,12 +204,12 @@
    5.13  	  handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
    5.14        val metID = get_obj g_metID pt pp;
    5.15        val {srls=srls,scr=sc,...} = get_met metID;
    5.16 -      val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (p,p_); 
    5.17 +      val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); 
    5.18       (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
    5.19        val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
    5.20        val thy' = get_obj g_domID pt pp;
    5.21        val thy = assoc_thy thy';
    5.22 -      val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc (is, ctxt);
    5.23 +      val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
    5.24        (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
    5.25  
    5.26      in if pp = [] then
    5.27 @@ -226,7 +226,7 @@
    5.28          val thy = assoc_thy thy';
    5.29  	val metID = get_obj g_metID pt ppp;
    5.30          val sc = (#scr o get_met) metID;
    5.31 -        val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (pp(*!/p/*),Frm); 
    5.32 +        val (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (pp(*!/p/*),Frm); 
    5.33       (*val _=tracing("### solve Check_postc, parpbl pos= "^(pos'2str(pp,Frm)));
    5.34    	val _=tracing("### solve Check_postc, is(pt)= "^(istate2str is));
    5.35    	val _=tracing("### solve Check_postc, is'= "^
    5.36 @@ -271,7 +271,7 @@
    5.37  	Form' (FormKF (~1, EdUndef, length p', Nundef, term2str r)),
    5.38  	tac_2tac tac_, Sundef,*)
    5.39  	[(End_Detail, End_Detail' t , 
    5.40 -	  ((p,p_), get_istate pt (p,p_)))], [], (pt,pr))) end
    5.41 +	  ((p,p_), get_loc pt (p,p_)))], [], (pt,pr))) end
    5.42  
    5.43    | solve (mI,m) (pt, po as (p,p_)) =
    5.44  (* val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
    5.45 @@ -360,12 +360,12 @@
    5.46  	  handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
    5.47        val metID = get_obj g_metID pt pp;
    5.48        val {srls=srls,scr=sc,...} = get_met metID;
    5.49 -      val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (p,p_); 
    5.50 +      val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_); 
    5.51       (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
    5.52        val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
    5.53        val thy' = get_obj g_domID pt pp;
    5.54        val thy = assoc_thy thy';
    5.55 -      val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc (is, ctxt);
    5.56 +      val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
    5.57        (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
    5.58      in if pp = [] then 
    5.59  	   let val is = ScrState (E,l,a,scval,scsaf,b)
    5.60 @@ -383,7 +383,7 @@
    5.61          val thy = assoc_thy thy';
    5.62  	val metID = get_obj g_metID pt ppp;
    5.63  	val {scr,...} = get_met metID;
    5.64 -        val (is as ScrState (E,l,a,_,_,b), ctxt) = get_istate pt (pp(*!/p/*),Frm)
    5.65 +        val (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (pp(*!/p/*),Frm)
    5.66          val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
    5.67  	val is = ScrState (E,l,a,scval,scsaf,b)
    5.68      (*val _= tracing"### nxt_solv3 Apply_Method: stored is =";

     6.1 --- a/test/Tools/isac/Test_Some.thy	Fri Apr 08 15:16:08 2011 +0200
     6.2 +++ b/test/Tools/isac/Test_Some.thy	Mon Apr 11 12:56:57 2011 +0200
     6.3 @@ -10,10 +10,11 @@
     6.4  (*..................................########..................................*)
     6.5  
     6.6  ML {*
     6.7 -parse;
     6.8 -parseNEW;
     6.9 -update_loc';
    6.10 -
    6.11 +get_loc;
    6.12 +g_loc;
    6.13 +get_obj;
    6.14 +specify_additem;
    6.15 +"====================== it ======================";
    6.16  val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
    6.17  val (_, ctxt) = prep_ori fmz @{theory} [];
    6.18  val to_parse = "equality (x + 1 = 2)";