1.1 --- a/src/Tools/isac/Interpret/script.sml	Wed May 18 09:45:45 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Wed May 18 10:20:11 2011 +0200
     1.3 @@ -1218,72 +1218,40 @@
     1.4     NotLocatable: thus generate_hard
     1.5  *)
     1.6  fun locate_gen (thy',_) (Rewrite'(_,ro,er,pa,(id,str),f,_)) (pt,p) 
     1.7 -	       (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) = 
     1.8 -    (case lo rss f (Thm (id, mk_thm (assoc_thy thy') str)) of
     1.9 -	 [] => NotLocatable
    1.10 +	  (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) = 
    1.11 +      (case lo rss f (Thm (id, mk_thm (assoc_thy thy') str)) of
    1.12 +	       [] => NotLocatable
    1.13         | rts' => 
    1.14 -	 Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
    1.15 +	         Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
    1.16  
    1.17    | locate_gen (ts as (thy',srls)) (m:tac_) ((pt,p):ptree * pos') 
    1.18 -	       (scr as Script (h $ body),d) (ScrState (E,l,a,v,S,b), ctxt)  = 
    1.19 -  let (*val _= tracing("### locate_gen-----------------: is=");
    1.20 -      val _= tracing( istate2str (ScrState (E,l,a,v,S,b)));
    1.21 -      val _= tracing("### locate_gen: l= "^loc_2str l^", p= "^pos'2str p)*)
    1.22 -      val thy = assoc_thy thy';
    1.23 -  in case if l=[] orelse ((*init.in solve..Apply_Method...*)
    1.24 -			  (last_elem o fst) p = 0 andalso snd p = Res)
    1.25 -	  then (assy ((ts,d),Aundef) ((E,[R],a,v,S,b),
    1.26 -				      [(m,EmptyMout,pt,p,[])]) body)
    1.27 -(* val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
    1.28 -       (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b),[(m,EmptyMout,pt,p,[])]));
    1.29 -       (assy ((ts,d),Aundef) ((E,[R],a,v,S,b),[(m,EmptyMout,pt,p,[])]) body);
    1.30 -  *)
    1.31 -	  else (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b),
    1.32 -					    [(m,EmptyMout,pt,p,[])]) ) of
    1.33 -	 Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =>
    1.34 -(* val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
    1.35 -       (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b),
    1.36 -				    [(m,EmptyMout,pt,p,[])]) );
    1.37 -   *)
    1.38 -	 ((*tracing("### locate_gen Assoc: p'="^(pos'2str p'));*)
    1.39 -	  if bb then Steps (ScrState is, ss)
    1.40 -	  else if rew_only ss (*andalso 'not bb'= associated weakly*)
    1.41 -	  then let val (po,p_) = p
    1.42 +	  (scr as Script (h $ body),d) (ScrState (E,l,a,v,S,b), ctxt)  = 
    1.43 +      let val thy = assoc_thy thy';
    1.44 +      in
    1.45 +        case if l = [] orelse ((*init.in solve..Apply_Method...*)
    1.46 +			         (last_elem o fst) p = 0 andalso snd p = Res)
    1.47 +	           then (assy ((ts,d),Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body)
    1.48 +	           else (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) of
    1.49 +	        Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =>
    1.50 +	          (if bb
    1.51 +             then Steps (ScrState is, ss)
    1.52 +	           else
    1.53 +               if rew_only ss (*andalso 'not bb'= associated weakly*)
    1.54 +	             then
    1.55 +                 let
    1.56 +                   val (po,p_) = p
    1.57                     val po' = case p_ of Frm => po | Res => lev_on po
    1.58 -		  (*WN.12.03: noticed, that pos is also updated in assy !?!
    1.59 -		   instead take p' from Assoc ?????????????????????????????*)
    1.60 -                  val (p'',c'',f'',pt'') = 
    1.61 -		      generate1 thy m (ScrState is, ctxt) (po',p_) pt;
    1.62 -	      (*val _=tracing("### locate_gen, aft g1: p''="^(pos'2str p''));*)
    1.63 -	      (*drop the intermediate steps !*)
    1.64 -	      in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
    1.65 -	 else Steps (ScrState is, ss))
    1.66 +                   val (p'',c'',f'',pt'') = 
    1.67 +		                 generate1 thy m (ScrState is, ctxt) (po',p_) pt;
    1.68 +	               in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
    1.69 +	             else Steps (ScrState is, ss))
    1.70  	
    1.71 -     | NasApp _ (*[((E,l,a,v,S,bb),(m',f',pt',p',c'))] => 
    1.72 -	   error ("locate_gen: should not have got NasApp, ets =")*)
    1.73 -       => NotLocatable
    1.74 -     | NasNap (_,_) =>
    1.75 -       if l=[] then NotLocatable
    1.76 -       else (*scan from begin of script for rew_only*)
    1.77 -	   (case assy ((ts,d),Aundef) ((E,[R],a,v,Unsafe,b),
    1.78 -					 [(m,EmptyMout,pt,p,[])]) body  of
    1.79 -		Assoc (iss as (is as (_,_,_,_,_,bb), 
    1.80 -			       ss as ((m',f',pt',p',c')::_))) =>
    1.81 -		    ((*tracing"4### locate_gen Assoc after Fini";*)
    1.82 -		     if rew_only ss
    1.83 -		     then let val(p'',c'',f'',pt'') = 
    1.84 -				 generate1 thy m (ScrState is, ctxt) p' pt;
    1.85 -			  (*drop the intermediate steps !*)
    1.86 -			  in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
    1.87 -		     else NotLocatable)
    1.88 -	      | _ => ((*tracing ("#### locate_gen: after Fini");*)
    1.89 -		      NotLocatable))
    1.90 -  end
    1.91 +        | NasApp _ => NotLocatable
    1.92 +      end
    1.93 +
    1.94    | locate_gen _ m _ (sc,_) (is, _) = 
    1.95 -    error ("locate_gen: wrong arguments,\n tac= "^(tac_2str m)^
    1.96 -		 ",\n scr= "^(scr2str sc)^",\n istate= "^(istate2str is));
    1.97 -
    1.98 -
    1.99 +      error ("locate_gen: wrong arguments,\n tac= " ^ tac_2str m ^ ",\n " ^
   1.100 +		    "scr= " ^ scr2str sc ^ ",\n istate= " ^ istate2str is);
   1.101  
   1.102  (** find the next stactic in a script **)
   1.103  

     2.1 --- a/src/Tools/isac/Interpret/solve.sml	Wed May 18 09:45:45 2011 +0200
     2.2 +++ b/src/Tools/isac/Interpret/solve.sml	Wed May 18 10:20:11 2011 +0200
     2.3 @@ -242,11 +242,13 @@
     2.4    | solve (mI,m) (pt, po as (p,p_)) =
     2.5        if e_metID = get_obj g_metID pt (par_pblobj pt p)(*29.8.02: could be detail, too !!*)
     2.6        then
     2.7 -        let val ((p,p_),ps,f,pt) = 
     2.8 -		      generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) 
     2.9 -			      m (e_istate, e_ctxt) (p,p_) pt;
    2.10 +        let
    2.11 +          val ctxt = get_ctxt pt po
    2.12 +          val ((p,p_),ps,f,pt) = 
    2.13 +		        generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) 
    2.14 +			        m (e_istate, ctxt) (p,p_) pt;
    2.15  	      in ("no-method-specified", (*Free_Solve*)
    2.16 -	        ([(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, e_ctxt)))], ps, (pt,(p,p_))))
    2.17 +	        ([(Empty_Tac,Empty_Tac_, ((p,p_),(Uistate, ctxt)))], ps, (pt,(p,p_))))
    2.18          end
    2.19        else
    2.20  	      let 
    2.21 @@ -272,11 +274,10 @@
    2.22  fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) =
    2.23        let
    2.24          val {srls,ppc,...} = get_met mI;
    2.25 -        val PblObj{meth=itms,origin=(oris,_,_),probl,...} = get_obj I pt p;
    2.26 +        val PblObj{meth=itms,origin=(oris,_,_),probl, ctxt, ...} = get_obj I pt p;
    2.27          val itms = if itms <> [] then itms else complete_metitms oris probl [] ppc
    2.28          val thy' = get_obj g_domID pt p;
    2.29          val thy = assoc_thy thy';
    2.30 -        val ctxt = get_ctxt pt pos
    2.31          val (is as ScrState (env,_,_,_,_,_), _, scr) = init_scrstate thy itms mI;
    2.32          val ini = init_form thy scr env;
    2.33        in