1.1 --- a/src/Tools/isac/Isac_Mathengine.thy	Fri Aug 20 17:02:49 2010 +0200
     1.2 +++ b/src/Tools/isac/Isac_Mathengine.thy	Fri Aug 20 17:18:59 2010 +0200
     1.3 @@ -40,25 +40,21 @@
     1.4  use "ME/appl.sml"
     1.5  use "ME/rewtools.sml"
     1.6  use "ME/script.sml"
     1.7 -
     1.8 +use "ME/solve.sml"
     1.9 +use "ME/inform.sml"
    1.10 +use "ME/mathengine.sml"
    1.11  
    1.12  ML {*
    1.13  val thy = @{theory "Script"};
    1.14 -Syntax.string_of_term;
    1.15 -Syntax.string_of_term (thy2ctxt thy);
    1.16 +
    1.17  *}
    1.18  
    1.19  ML {*
    1.20 -Syntax.string_of_term (thy2ctxt thy);
    1.21 +val thy = @{theory "Script"};
    1.22  
    1.23  *}
    1.24  
    1.25 -
    1.26 -
    1.27  (*
    1.28 -use "ME/solve.sml"
    1.29 -use "ME/inform.sml"
    1.30 -use "ME/mathengine.sml"
    1.31  
    1.32  use "xmlsrc/mathml.sml"
    1.33  use "xmlsrc/datatypes.sml"

     2.1 --- a/src/Tools/isac/ME/inform.sml	Fri Aug 20 17:02:49 2010 +0200
     2.2 +++ b/src/Tools/isac/ME/inform.sml	Fri Aug 20 17:18:59 2010 +0200
     2.3 @@ -226,7 +226,7 @@
     2.4  fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) =
     2.5  (* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl;
     2.6     *)
     2.7 -    (let val t = (term_of o comp_dts (Isac "delay")) (d,ts);
     2.8 +    (let val t = (comp_dts (Isac "delay")) (d,ts);
     2.9  	 val s = Syntax.string_of_term (thy2ctxt dI) t;
    2.10       (*this    ^ should raise the exn on unability of re-parsing dts*)
    2.11       in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    2.12 @@ -237,12 +237,12 @@
    2.13      (let val t = (term_of o the o (parse dI)) str
    2.14       in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str))
    2.15    | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) =
    2.16 -    (let val t = (term_of o comp_dts (Isac "delay")) (d,ts);
    2.17 +    (let val t = (comp_dts (Isac "delay")) (d,ts);
    2.18  	 val s = Syntax.string_of_term (thy2ctxt dI) t;
    2.19       (*this    ^ should raise the exn on unability of re-parsing dts*)
    2.20       in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    2.21    | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) =
    2.22 -    (let val t = (term_of o comp_dts (Isac"delay" )) (d,ts);
    2.23 +    (let val t = (comp_dts (Isac"delay" )) (d,ts);
    2.24  	 val s = Syntax.string_of_term (thy2ctxt dI) t;
    2.25       (*this    ^ should raise the exn on unability of re-parsing dts*)
    2.26       in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    2.27 @@ -252,7 +252,7 @@
    2.28       (*this    ^ should raise the exn on unability of re-parsing dts*)
    2.29       in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
    2.30    | parsitm dI (itm as (i,v,_,f, Par _)) = 
    2.31 -    raise error ("parsitm ("^itm2str_ dI itm^
    2.32 +    raise error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm^
    2.33  		 "): Par should be internal");
    2.34  
    2.35  (*separate a list to a pair of elements that do NOT satisfy the predicate,
    2.36 @@ -392,8 +392,8 @@
    2.37  
    2.38  
    2.39  fun par2fstr ((_,_,_,f, Par s):itm) = (f, s)
    2.40 -  | par2fstr itm = raise error ("par2fstr: called with "^
    2.41 -			      itm2str_ (assoc_thy "Isac.thy") itm);
    2.42 +  | par2fstr itm = raise error ("par2fstr: called with " ^
    2.43 +			      itm2str_ (thy2ctxt' "Isac") itm);
    2.44  fun itms2fstr ((_,_,_,f, Cor ((d,ts),_)):itm) = (f, comp_dts'' (d,ts))
    2.45    | itms2fstr (_,_,_,f, Syn str) = (f, str)
    2.46    | itms2fstr (_,_,_,f, Typ str) = (f, str)
    2.47 @@ -401,7 +401,7 @@
    2.48    | itms2fstr (_,_,_,f, Sup (d,ts)) = (f, comp_dts'' (d,ts))
    2.49    | itms2fstr (_,_,_,f, Mis (d,t)) = (f, term2str (d $ t))
    2.50    | itms2fstr (itm as (_,_,_,f, Par _)) = 
    2.51 -    raise error ("parsitm ("^itm2str_ (assoc_thy "Isac.thy") itm^
    2.52 +    raise error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^
    2.53  		 "): Par should be internal");
    2.54  
    2.55  fun imodel2fstr iitems = 

     3.1 --- a/src/Tools/isac/ME/mathengine.sml	Fri Aug 20 17:02:49 2010 +0200
     3.2 +++ b/src/Tools/isac/ME/mathengine.sml	Fri Aug 20 17:18:59 2010 +0200
     3.3 @@ -171,17 +171,17 @@
     3.4  			      probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
     3.5      in if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
     3.6         then case mI' of
     3.7 -	 ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p,Pbl))
     3.8 +	 ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
     3.9         | _ => nxt_specif Model_Problem (pt, (p,Pbl))
    3.10         else let val cpI = if pI = e_pblID then pI' else pI;
    3.11  		val cmI = if mI = e_metID then mI' else mI;
    3.12  		val {ppc,prls,where_,...} = get_pbt cpI;
    3.13 -		val pre = check_preconds thy prls where_ probl;
    3.14 +		val pre = check_preconds "thy 100820" prls where_ probl;
    3.15  		val pb = foldl and_ (true, map fst pre);
    3.16  		(*FIXME.WN0308:    ~~~~~: just check true in itms of pbl/met?*)
    3.17  		val (_,tac) =
    3.18 -		    nxt_spec p_ pb oris (dI',pI',mI') (probl,meth) 
    3.19 -			     (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
    3.20 +		    nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) 
    3.21 +			     (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
    3.22  	    in case tac of
    3.23  		   Apply_Method mI => 
    3.24  (* val Apply_Method mI = tac;
    3.25 @@ -305,8 +305,8 @@
    3.26       then let val ptp = all_modspec (pt, pos);
    3.27  	  in all_solve auto c ptp end
    3.28       else
    3.29 -	 if p_ mem [Pbl, Met]
    3.30 -	 then if not (is_complete_mod (pt, pos))
    3.31 +	 if member op = [Pbl, Met] p_
    3.32 + 	 then if not (is_complete_mod (pt, pos))
    3.33  	      then let val ptp = complete_mod (pt, pos)
    3.34  		   in if autoord auto < 3 then ("ok", c, ptp)
    3.35  		      else