1.1 --- a/src/sml/ME/ctree.sml	Fri Mar 04 19:47:04 2005 +0100
     1.2 +++ b/src/sml/ME/ctree.sml	Sat Mar 05 14:18:11 2005 +0100
     1.3 @@ -204,12 +204,12 @@
     1.4    | ldr2str D = "D";
     1.5  fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;
     1.6  
     1.7 -(*26.4.02: never used after introduction of scripts !!!*)
     1.8 +(*26.4.02: never used after introduction of scripts !!!
     1.9  type loc =  loc_ *        (* + interpreter-state          *)
    1.10  	    (loc_ * rls') (* -"- for script of the ruleset*)
    1.11  		option;
    1.12  val e_loc = ([],None):loc;
    1.13 -val ee_loc = (e_loc,e_loc);
    1.14 +val ee_loc = (e_loc,e_loc);*)
    1.15  
    1.16  
    1.17  datatype safe = Sundef | Safe | Unsafe | Helpless;
    1.18 @@ -1869,6 +1869,14 @@
    1.19  (writeln("##@cappend_atomic: pos ="^pos2str p);
    1.20    apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
    1.21  );
    1.22 +fun cappend_atomic pt p loc f r f' s = 
    1.23 +let val _= writeln("##@cappend_atomic: pos ="^pos2str p)
    1.24 +    val _= writeln("##@cappend_atomic before cut_tree: loc ="^istate2str loc)
    1.25 +    val (pt', cs) = cut_tree pt (p,Frm)
    1.26 +    val pt'' = append_atomic p loc f r f' s pt'
    1.27 +    val _= writeln("##@cappend_atomic after append: loc ="^
    1.28 +		   istates2str (get_obj g_loc pt'' p))
    1.29 +in (pt'', cs) end;
    1.30  
    1.31  (* called by Take *)
    1.32  fun append_form p l f pt = 
    1.33 @@ -1891,6 +1899,14 @@
    1.34  (writeln("##@cappend_form: pos ="^pos2str p);
    1.35    apfst (append_form p loc f) (cut_tree pt (p,Frm))
    1.36  );
    1.37 +fun cappend_form pt p loc f =
    1.38 +let val _= writeln("##@cappend_form: pos ="^pos2str p)
    1.39 +    val _= writeln("##@cappend_form before cut_tree: loc ="^istate2str loc)
    1.40 +    val (pt', cs) = cut_tree pt (p,Frm)
    1.41 +    val pt'' = append_form p loc f pt'
    1.42 +    val _= writeln("##@cappend_form after append: loc ="^
    1.43 +		   istates2str (get_obj g_loc pt'' p))
    1.44 +in (pt'', cs) end;
    1.45  
    1.46  
    1.47      

     2.1 --- a/src/sml/systest/auto-inform.sml	Fri Mar 04 19:47:04 2005 +0100
     2.2 +++ b/src/sml/systest/auto-inform.sml	Sat Mar 05 14:18:11 2005 +0100
     2.3 @@ -300,7 +300,7 @@
     2.4  "--------- appendFormula: on Frm + equ_nrls ----------------------";
     2.5  "--------- appendFormula: on Frm + equ_nrls ----------------------";
     2.6  "--------- appendFormula: on Frm + equ_nrls ----------------------";
     2.7 -(**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@(**) 
     2.8 +(**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**) 
     2.9   states:=[];
    2.10   CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], 
    2.11  	    ("Test.thy", 
    2.12 @@ -309,9 +309,49 @@
    2.13   Iterator 1; moveActiveRoot 1;
    2.14   autoCalculate 1 CompleteCalcHead;
    2.15   autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
    2.16 - 
    2.17 + (*> ###generate1 Apply_Method': pos = ([1], Frm)
    2.18 +###generate1 Apply_Method': topt= Some x + 1 = 2
    2.19 +###generate1 Apply_Method': is  = ScrState (["
    2.20 +(e_, x + 1 = 2)","
    2.21 +(v_, x)"],
    2.22 + [], None,
    2.23 + ??.empty, Safe, true)
    2.24 +##@cappend_form: pos =[1]
    2.25 +##@cappend_form before cut_tree: loc =ScrState (["
    2.26 +(e_, x + 1 = 2)","
    2.27 +(v_, x)"],
    2.28 + [], None,
    2.29 + ??.empty, Safe, true)
    2.30 +##@append_form: pos =[1]
    2.31 +##@cappend_form after append: loc =(#Some ScrState (["
    2.32 +(e_, x + 1 = 2)","
    2.33 +(v_, x)"],
    2.34 + [], None,
    2.35 + ??.empty, Safe, true),
    2.36 + #None)
    2.37 +###generate1 Apply_Method: after cappend
    2.38 +*)
    2.39   appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1);
    2.40 -(**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**) 
    2.41 +(**)@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@;(**) 
    2.42 +(*
    2.43 +>  appendFormula 1 "2+ -1 + x = 2";
    2.44 +###generate1 Rewrite_Set': pos= ([1], Frm)
    2.45 +##@cappend_atomic: pos =[1]
    2.46 +##@cappend_atomic before cut_tree: loc =ScrState (["
    2.47 +(e_, x + 1 = 2)","
    2.48 +(v_, x)"],
    2.49 + [R,L,R,L,L,R,R], Some e_,
    2.50 + x + 1 + -1 * 2 = 0, Sundef, false)
    2.51 +#@append_atomic: pos =[1]
    2.52 +##@cappend_atomic after append: loc =(#None,
    2.53 +#Some ScrState (["
    2.54 +(e_, x + 1 = 2)","
    2.55 +(v_, x)"],
    2.56 + [R,L,R,L,L,R,R], Some e_,
    2.57 + x + 1 + -1 * 2 = 0, Sundef, false))
    2.58 +Exception- Bind raised
    2.59 +*)
    2.60 +
    2.61  
    2.62   moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
    2.63  
    2.64 @@ -334,7 +374,7 @@
    2.65   val ((pt,_),_) = get_calc 1;
    2.66   if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
    2.67   else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 3";
    2.68 -(**)@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**) 
    2.69 +(**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**) 
    2.70   
    2.71  
    2.72