1.1 --- a/src/sml/FE-interface/interface.sml	Thu Nov 02 16:08:45 2006 +0100
     1.2 +++ b/src/sml/FE-interface/interface.sml	Thu Nov 02 16:51:12 2006 +0100
     1.3 @@ -531,28 +531,8 @@
     1.4  	  | (msg, cs') => appendformulaERROR2xml cI msg
     1.5       end)
     1.6      handle _ => sysERROR2xml cI "error in kernel";
     1.7 -(*
     1.8 -fun appendFormula cI (ifo:cterm') =
     1.9 -    (let val cs = get_calc cI
    1.10 -	 val pos as (_,p_) = get_pos cI 1
    1.11 -     in case step pos cs of
    1.12 -(* val (str, cs') = step pos cs;
    1.13 -   *)
    1.14 -	    ("ok", cs') =>
    1.15 -	    (case inform cs' (encode ifo) of
    1.16 -(* val (str, (_, c, ptp as (_,p))) = inform cs' (encode ifo);
    1.17 -   *)
    1.18 -		 ("ok", (_(*use in DG !!!*), c, ptp as (_,p))) =>
    1.19 -		 (upd_calc cI (ptp, []); upd_ipos cI 1 p;
    1.20 -		  appendformulaOK2xml cI pos (if null c then pos
    1.21 -					      else last_elem c) p)
    1.22 -	       | ("same-formula", (_(*use in DG !!!*), c, ptp as (_,p))) => 
    1.23 -		 (appendformulaOK2xml cI pos pos p)
    1.24 -	       | (msg, _) => appendformulaERROR2xml cI msg)
    1.25 -	  | (msg, cs') => appendformulaERROR2xml cI msg
    1.26 -     end)
    1.27 -    handle _ => sysERROR2xml cI "error in kernel";
    1.28 -*)
    1.29 +
    1.30 +
    1.31  
    1.32  (*.replace a formula with_in_ a calculation;
    1.33     this situation applies for initial CAS-commands, too.*)

     2.1 --- a/src/sml/ME/inform.sml	Thu Nov 02 16:08:45 2006 +0100
     2.2 +++ b/src/sml/ME/inform.sml	Thu Nov 02 16:51:12 2006 +0100
     2.3 @@ -706,36 +706,7 @@
     2.4  					 lev_back pos)) ifo
     2.5  	end
     2.6        | None => ("syntax error in '"^istr^"'", e_calcstate');
     2.7 -(* val ((cs as (tacis, _, ptp as (pt, pos as (p, p_)))), istr) =
     2.8 -       (cs', (encode ifo));
     2.9 -   *)
    2.10 -(*
    2.11 -fun inform (cs as (tacis, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
    2.12 -    case parse (assoc_thy "Isac.thy") istr of
    2.13 -(* val Some ifo = parse (assoc_thy "Isac.thy") istr;
    2.14 -   *)
    2.15 -	Some ifo =>
    2.16 -	let val ifo = term_of ifo
    2.17 -	    val fo = case p_ of Frm => get_obj g_form pt p
    2.18 -			      | Res => (fst o (get_obj g_result pt)) p
    2.19 -			      | _ => #3 (get_obj g_origin pt p)
    2.20 -	in if ifo = fo
    2.21 -	   then ("same-formula", cs)
    2.22 -	   (*thus ctree not cut with replaceFormula!*)
    2.23 -	   else if ifo = (fst o res_from_taci o hd) tacis
    2.24 -	   (*fo calculated by step before*)
    2.25 -	   then ("ok", cs)
    2.26 -	   else case cas_input ifo of
    2.27 -(* val Some (pt, _) = cas_input ifo;
    2.28 -   *)
    2.29 -		    Some (pt, _) => ("ok",([],[],(pt, (p, Pbl))))
    2.30 -		  | None =>
    2.31 -		    compare_step ([],[],(pt,
    2.32 -				     (*last step re-calc in compare_step TODO*)
    2.33 -					 lev_back pos)) ifo
    2.34 -	end
    2.35 -      | None => ("syntax error in '"^istr^"'", e_calcstate');
    2.36 -*)
    2.37 +
    2.38  
    2.39  (*------------------------------------------------------------------(**)
    2.40  end

     3.1 --- a/src/smltest/ME/inform.sml	Thu Nov 02 16:08:45 2006 +0100
     3.2 +++ b/src/smltest/ME/inform.sml	Thu Nov 02 16:51:12 2006 +0100
     3.3 @@ -477,8 +477,11 @@
     3.4  autoCalculate 1 (Step 1);
     3.5  autoCalculate 1 (Step 1);
     3.6  autoCalculate 1 (Step 1);
     3.7 +"--- input the next formula that _should_ be presented by mat-engine";
     3.8 +appendFormula 1 "(4 * y + -3 * x) / (x * y) + -1";
     3.9  "--- input the next formula that would be presented by mat-engine";
    3.10 -appendFormula 1 "(4 * y + -3 * x) / (x * y) + -1";
    3.11 +(*autoCalculate 1 (Step 1);*)
    3.12 +appendFormula 1 "(4 * y + -3 * x + -1 * (x * y)) / (x * y)";
    3.13  
    3.14  val ((pt,p),_) = get_calc 1;
    3.15  show_pt pt;