user session management now parallel
authorMathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
Mon, 10 Mar 2014 21:07:35 +0100
changeset 55402d580d7fc9b8e
parent 55401 7961cffaafcf
child 55403 d2d4125a92ad
user session management now parallel

appendFormula uses futures.
src/Tools/isac/Frontend/interface.sml
test/Tools/isac/Frontend/use-cases.sml
test/Tools/isac/Interpret/generate.sml
test/Tools/isac/Interpret/inform.sml
test/Tools/isac/Knowledge/diff.sml
test/Tools/isac/Knowledge/simplify.sml
     1.1 --- a/src/Tools/isac/Frontend/interface.sml	Sat Mar 08 11:07:52 2014 +0100
     1.2 +++ b/src/Tools/isac/Frontend/interface.sml	Mon Mar 10 21:07:35 2014 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4      val DEconstrCalcTree : calcID -> unit
     1.5      val Iterator : calcID -> unit
     1.6      val IteratorTEST : calcID -> iterID
     1.7 -    val appendFormula : calcID -> cterm' -> unit
     1.8 +    val appendFormula : calcID -> cterm' -> unit future
     1.9      val autoCalculate : calcID -> auto -> unit
    1.10      val checkContext : calcID -> pos' -> guh -> unit
    1.11      val fetchApplicableTactics : calcID -> int -> pos' -> unit
    1.12 @@ -71,7 +71,7 @@
    1.13     encode "^" ---> "^^^"; see Knowledge/Atools.thy;
    1.14     called for each cterm', icalhd, fmz in this interface;
    1.15     + see "fun decode" in xmlsrc/mathml.sml *)
    1.16 -fun encode (str : cterm') = 
    1.17 +fun encode (str : cterm') =
    1.18      let fun enc [] = []
    1.19  	  | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)
    1.20  	  | enc (c :: cs) = c :: (enc cs)
    1.21 @@ -137,7 +137,7 @@
    1.22     val (cI, tac) = (1, Rewrite_Set "Test_simplify");
    1.23      *)
    1.24  fun setNextTactic (cI:calcID) tac =
    1.25 -  let 
    1.26 +  let
    1.27      val ((pt, _), _) = get_calc cI
    1.28  	  val ip = get_pos cI 1
    1.29    in case locatetac tac (pt, ip) of
    1.30 @@ -159,7 +159,7 @@
    1.31    let
    1.32      val ((pt, _), _) = get_calc cI
    1.33  	  val p = get_pos cI 1
    1.34 -  in 
    1.35 +  in
    1.36      case locatetac tac (pt, ip) of
    1.37  	    ("ok", (_, c, ptp as (_,p'))) =>
    1.38  	      (upd_calc cI (ptp, []);
    1.39 @@ -214,7 +214,7 @@
    1.40  	  | (str, _, _) => autocalculateERROR2xml cI str
    1.41    end)
    1.42    handle _ => sysERROR2xml cI "error in kernel";
    1.43 -    
    1.44 +
    1.45  
    1.46  (* val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
    1.47         (1, (([],Pbl), "not used here",
    1.48 @@ -233,7 +233,7 @@
    1.49   val (cI:calcID, ichd as ((p,_),_,_,_,_):icalhd) =
    1.50         (1, (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], [])));
    1.51   val (cI, p:pos')=(1, ([1],Frm));
    1.52 - val (cI, p:pos')=(1, ([1,2,1,3],Res)); 
    1.53 + val (cI, p:pos')=(1, ([1,2,1,3],Res));
    1.54     *)
    1.55  fun getTactic cI (p:pos') =
    1.56      (let val ((pt,_),_) = get_calc cI
    1.57 @@ -256,16 +256,16 @@
    1.58  fun fetchApplicableTactics cI (scope:int) (p:pos') =
    1.59      (let val ((pt, _), _) = get_calc cI
    1.60      in (applicabletacticsOK cI (sel_rules pt p))
    1.61 -       handle PTREE str => sysERROR2xml cI str 
    1.62 +       handle PTREE str => sysERROR2xml cI str
    1.63       end)
    1.64      handle _ => sysERROR2xml cI "error in kernel";
    1.65  (*WN120611 took version 1 again
    1.66 -  version 2: fetch _applicable_ _elementary_ (ie. recursively 
    1.67 +  version 2: fetch _applicable_ _elementary_ (ie. recursively
    1.68                decompose rule-sets) Rewrite*, Calculate
    1.69  fun fetchApplicableTactics cI (scope:int) (p:pos') =
    1.70      (let val ((pt, _), _) = get_calc cI
    1.71      in (applicabletacticsOK cI (sel_appl_atomic_tacs pt p))
    1.72 -       handle PTREE str => sysERROR2xml cI str 
    1.73 +       handle PTREE str => sysERROR2xml cI str
    1.74       end)
    1.75      handle _ => sysERROR2xml cI "error in kernel";
    1.76  *)
    1.77 @@ -294,7 +294,7 @@
    1.78      in refformulaOK2xml cI p form end)
    1.79      handle _ => sysERROR2xml cI "error in kernel";
    1.80  
    1.81 -(*.get formulae 'from' 'to' w.r.t. ordering in Position#compareTo(Position p); 
    1.82 +(*.get formulae 'from' 'to' w.r.t. ordering in Position#compareTo(Position p);
    1.83     in case of CalcHeads only the headline is taken
    1.84     (the pos' allows distinction between PrfObj and PblObj anyway);
    1.85     'level' is adjusted such that an 'interval' of formulae is returned;
    1.86 @@ -364,62 +364,62 @@
    1.87  fun modifyCalcHead (cI:calcID) (ichd as ((p,_),_,_,_,_):icalhd) =
    1.88      (let val ((pt,_),_) = get_calc cI
    1.89  	val (pt, chd as (_,p_,_,_,_,_)) = input_icalhd pt ichd
    1.90 -    in (upd_calc cI ((pt, (p,p_)), []); 
    1.91 +    in (upd_calc cI ((pt, (p,p_)), []);
    1.92  	modifycalcheadOK2xml cI chd) end)
    1.93      handle _ => sysERROR2xml cI "error in kernel";
    1.94  
    1.95 -(*.at the activeFormula set the Model, the Guard and the Specification 
    1.96 +(*.at the activeFormula set the Model, the Guard and the Specification
    1.97     to empty and return a CalcHead;
    1.98     the 'origin' remains (for reconstructing all that).*)
    1.99 -fun resetCalcHead (cI:calcID) = 
   1.100 +fun resetCalcHead (cI:calcID) =
   1.101      (let val (ptp,_) = get_calc cI
   1.102  	val ptp = reset_calchead ptp
   1.103 -    in (upd_calc cI (ptp, []); 
   1.104 +    in (upd_calc cI (ptp, []);
   1.105  	modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
   1.106      handle _ => sysERROR2xml cI "error in kernel";
   1.107  
   1.108 -(*.at the activeFormula insert all the Descriptions in the Model 
   1.109 +(*.at the activeFormula insert all the Descriptions in the Model
   1.110     (_not_ in the Guard) and return a CalcHead;
   1.111 -   the Descriptions are for user-guidance; the rest of the items 
   1.112 -   are left empty for user-input; 
   1.113 +   the Descriptions are for user-guidance; the rest of the items
   1.114 +   are left empty for user-input;
   1.115     includes a resetCalcHead for the Model and the Guard.*)
   1.116 -fun modelProblem (cI:calcID) = 
   1.117 +fun modelProblem (cI:calcID) =
   1.118      (let val (ptp, _) = get_calc cI
   1.119  	val ptp = reset_calchead ptp
   1.120  	val (_, _, ptp) = nxt_specif Model_Problem ptp
   1.121 -    in (upd_calc cI (ptp, []); 
   1.122 +    in (upd_calc cI (ptp, []);
   1.123  	modifycalcheadOK2xml cI (get_ocalhd ptp)) end)
   1.124      handle _ => sysERROR2xml cI "error in kernel";
   1.125  
   1.126  
   1.127  (* set the UContext determined on a knowledgebrowser to the current calc *)
   1.128  fun setContext (cI:calcID) (ip as (_,p_):pos') (guh:guh) =
   1.129 -  (case (implode o (take_fromto 1 4) o Symbol.explode) guh of 
   1.130 +  (case (implode o (take_fromto 1 4) o Symbol.explode) guh of
   1.131       "thy_" =>
   1.132  	     if member op = [Pbl,Met] p_
   1.133         then message2xml cI "thy-context not to calchead"
   1.134         else if ip = ([],Res) then message2xml cI "no thy-context at result"
   1.135  	     else if no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")
   1.136 -  	   else 
   1.137 +  	   else
   1.138           let
   1.139             val (ptp as (pt, pold), _) = get_calc cI
   1.140  		       val is = get_istate pt ip
   1.141  		       val subs = subs_from is "dummy" guh
   1.142  		       val tac = guh2rewtac guh subs
   1.143 -  	     in 
   1.144 +  	     in
   1.145             case locatetac tac (pt, ip) of (*='fun setNextTactic'+step*)
   1.146  		         ("ok", (tacis, c, ptp as (_,p))) =>
   1.147 -		           (upd_calc cI ((pt,p), []); 
   1.148 +		           (upd_calc cI ((pt,p), []);
   1.149  		            autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
   1.150  		       | ("unsafe-ok", (tacis, c, ptp as (_,p))) =>
   1.151 -  		         (upd_calc cI ((pt,p), []); 
   1.152 +  		         (upd_calc cI ((pt,p), []);
   1.153  	  	          autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)
   1.154  		       | ("end-of-calculation",_) => message2xml cI "end-of-calculation"
   1.155  		       | ("failure",_) => sysERROR2xml cI "failure"
   1.156  		       | ("not-applicable",_) => (*the rule comes from anywhere..*)
   1.157 -		           (case applicable_in ip pt tac of 
   1.158 +		           (case applicable_in ip pt tac of
   1.159  		              Notappl e => message2xml cI ("'" ^ tac2str tac ^ "' not-applicable")
   1.160 -	              | Appl m => 
   1.161 +	              | Appl m =>
   1.162  		                let
   1.163                        val ctxt = get_ctxt pt pold
   1.164                        val (p,c,_,pt) =
   1.165 @@ -433,7 +433,7 @@
   1.166           val pI = guh2kestoreID guh
   1.167  	       val ((pt, _), _) = get_calc cI
   1.168  	       in
   1.169 -           if member op = [Pbl, Met] p_ 
   1.170 +           if member op = [Pbl, Met] p_
   1.171  	         then
   1.172               let val (pt, chd) = set_problem pI (pt, ip)
   1.173  		         in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end
   1.174 @@ -456,12 +456,12 @@
   1.175  (*.specify the Method at the activeFormula and return a CalcHead
   1.176     containing the Guard.
   1.177     WN0512 impl.incomplete, see 'nxt_specif (Specify_Method '.*)
   1.178 -fun setMethod (cI:calcID) (mI:metID) = 
   1.179 +fun setMethod (cI:calcID) (mI:metID) =
   1.180  (* val (cI, mI) = (1, ["Test","solve_linear"]);
   1.181     *)
   1.182      (let val ((pt, _), _) = get_calc cI
   1.183  	val ip as (_, p_) = get_pos cI 1
   1.184 -    in if member op = [Pbl,Met] p_ 
   1.185 +    in if member op = [Pbl,Met] p_
   1.186         then let val (pt, chd) = set_method mI (pt, ip)
   1.187  	    in (upd_calc cI ((pt, ip), []);
   1.188  		modifycalcheadOK2xml cI chd) end
   1.189 @@ -500,7 +500,7 @@
   1.190  
   1.191  (**. without update of CalcTree .**)
   1.192  
   1.193 -(*.match the model of a problem at pos p 
   1.194 +(*.match the model of a problem at pos p
   1.195     with the model-pattern of the problem with pblID*)
   1.196  (*fun tryMatchProblem cI pblID =
   1.197      (let val ((pt,_),_) = get_calc cI
   1.198 @@ -521,7 +521,7 @@
   1.199      handle _ => sysERROR2xml cI "error in kernel";
   1.200  
   1.201  (* append a formula to the calculation *)
   1.202 -fun appendFormula cI (ifo:cterm') =
   1.203 +fun appendFormula' cI (ifo:cterm') =
   1.204    (let
   1.205      val cs = get_calc cI
   1.206      val pos as (_,p_) = get_pos cI 1
   1.207 @@ -540,6 +540,8 @@
   1.208    end)
   1.209    handle _ => sysERROR2xml cI "error in kernel";
   1.210  
   1.211 +fun appendFormula cI ifo = Future.fork (fn () => appendFormula' cI ifo);
   1.212 +
   1.213  (* replace a formula with_in_ a calculation;
   1.214     this situation applies for initial CAS-commands, too *)
   1.215  fun replaceFormula cI (ifo:cterm') =
   1.216 @@ -671,7 +673,7 @@
   1.217      handle _ => sysERROR2xml cI "error in kernel";
   1.218  
   1.219  
   1.220 -(*.initContext Thy_ is conceptually impossible at [Pbl,Met] 
   1.221 +(*.initContext Thy_ is conceptually impossible at [Pbl,Met]
   1.222     and at positions with Check_Postcond and End_Trans;
   1.223     at possible pos's there can be NO rewrite (returned as a context, too).*)
   1.224  (* val (cI, Thy_, (pos as (p,p_):pos')) = (1, Thy_, ([1], Frm));
   1.225 @@ -687,7 +689,7 @@
   1.226  	   in if exist_lev_on' pt pos
   1.227  	      then let val pos' = lev_on' pt pos
   1.228  		       val tac = get_tac_checked pt pos'
   1.229 -		   in if is_rewtac tac 
   1.230 +		   in if is_rewtac tac
   1.231  		      then contextthyOK2xml cI (context_thy (pt,pos) tac)
   1.232  		      else message2xml cI ("no thy-context at tac '" ^
   1.233  					   tac2str tac ^ "'")
   1.234 @@ -699,8 +701,8 @@
   1.235     *)
   1.236  		       ("ok", (tacis, _, (pt,_))) =>
   1.237  		       let val tac = fst3 (last_elem tacis)
   1.238 -		       in if is_rewtac tac 
   1.239 -			  then contextthyOK2xml 
   1.240 +		       in if is_rewtac tac
   1.241 +			  then contextthyOK2xml
   1.242  				   cI (context_thy ptp tac)
   1.243  			  else message2xml cI ("no thy-context at tac '" ^
   1.244  					       tac2str tac ^ "'")
   1.245 @@ -712,7 +714,7 @@
   1.246  
   1.247  (* val (cI, Pbl_, pos as (p,p_)) = (1, Pbl_, ([],Pbl));
   1.248     *)
   1.249 -  | initContext cI Pbl_ (pos as (p,p_):pos') = 
   1.250 +  | initContext cI Pbl_ (pos as (p,p_):pos') =
   1.251      ((let val ((pt,_),_) = get_calc cI
   1.252  	  val pp = par_pblobj pt p
   1.253  	  val chd = initcontext_pbl pt (pp,p_)
   1.254 @@ -748,8 +750,8 @@
   1.255  		  val subs = subs_from is "dummy" guh
   1.256  		  val tac = guh2rewtac guh subs
   1.257  	      in contextthyOK2xml cI (context_thy (pt, pos) tac) end
   1.258 -		  
   1.259 -       (*.match the model of a problem at pos p 
   1.260 +
   1.261 +       (*.match the model of a problem at pos p
   1.262            with the model-pattern of the problem with pblID.*)
   1.263  (* val (cI, pos:pos' as (p,p_), guh) =
   1.264         (1, p, kestoreID2guh Pbl_ ["univariate","equation"]);
   1.265 @@ -758,16 +760,16 @@
   1.266     val (cI, pos:pos' as (p,p_), guh) =
   1.267         (1, ([],Pbl), "pbl_equ_univ");
   1.268     *)
   1.269 -       | "pbl_" => 
   1.270 +       | "pbl_" =>
   1.271  	 let val ((pt,_),_) = get_calc cI
   1.272  	     val pp = par_pblobj pt p
   1.273  	     val keID = guh2kestoreID guh
   1.274  	     val chd = context_pbl keID pt pp
   1.275  	 in matchpbl2xml cI chd end
   1.276 -(* val (cI, pos:pos' as (p,p_), guh) = 
   1.277 +(* val (cI, pos:pos' as (p,p_), guh) =
   1.278         (1, ([],Pbl), kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
   1.279     *)
   1.280 -       | "met_" => 
   1.281 +       | "met_" =>
   1.282  	 let val ((pt,_),_) = get_calc cI
   1.283  	     val pp = par_pblobj pt p
   1.284  	     val keID = guh2kestoreID guh
   1.285 @@ -775,9 +777,9 @@
   1.286  	 in matchmet2xml cI chd end)
   1.287      handle _ => sysERROR2xml cI "error in kernel";
   1.288  
   1.289 -(* for an errpatID find "(fillpatID, fillform)" list 
   1.290 +(* for an errpatID find "(fillpatID, fillform)" list
   1.291    which dedicated to this errpat and which is applicable at current formula*)
   1.292 -fun findFillpatterns cI errpatID = 
   1.293 +fun findFillpatterns cI errpatID =
   1.294    let
   1.295      val ((pt, _), _) = get_calc cI
   1.296  		    val pos = get_pos cI 1;
   1.297 @@ -794,9 +796,9 @@
   1.298    let
   1.299      val ((pt, _), _) = get_calc cI
   1.300  		val pos = get_pos cI 1
   1.301 -    val fillforms = find_fillpatterns (pt, pos) errpatID 
   1.302 +    val fillforms = find_fillpatterns (pt, pos) errpatID
   1.303    in
   1.304 -    case filter ((curry op = fillpatID) o 
   1.305 +    case filter ((curry op = fillpatID) o
   1.306          (#1: (fillpatID * term * thm * (subs option) -> fillpatID))) fillforms of
   1.307        (_, fillform, thm, sube_opt) :: _ =>
   1.308          let
   1.309 @@ -806,8 +808,8 @@
   1.310            (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
   1.311             autocalculateOK2xml cI pos pos' pos')
   1.312          end
   1.313 -    | _ => autocalculateERROR2xml cI "no fillpattern found"    
   1.314 -  end;    
   1.315 +    | _ => autocalculateERROR2xml cI "no fillpattern found"
   1.316 +  end;
   1.317  
   1.318  (* input a formula which exactly fills the gaps in a "fillformula"
   1.319     presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
     2.1 --- a/test/Tools/isac/Frontend/use-cases.sml	Sat Mar 08 11:07:52 2014 +0100
     2.2 +++ b/test/Tools/isac/Frontend/use-cases.sml	Mon Mar 10 21:07:35 2014 +0100
     2.3 @@ -1128,7 +1128,7 @@
     2.4   autoCalculate 1 CompleteCalcHead;
     2.5   autoCalculate 1 (Step 1);
     2.6   autoCalculate 1 (Step 1);
     2.7 - appendFormula 1 "-1 + x = 0";  
     2.8 + appendFormula 1 "-1 + x = 0" |> Future.join;  
     2.9   (*... returns calcChangedEvent with*)
    2.10   val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
    2.11   getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
    2.12 @@ -1151,7 +1151,7 @@
    2.13   autoCalculate 1 CompleteCalcHead;
    2.14   autoCalculate 1 (Step 1);
    2.15   autoCalculate 1 (Step 1);
    2.16 - appendFormula 1 "x - 1 = 0"; 
    2.17 + appendFormula 1 "x - 1 = 0" |> Future.join; 
    2.18   val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
    2.19   getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
    2.20   (*11 elements !!!*)
    2.21 @@ -1174,7 +1174,7 @@
    2.22   autoCalculate 1 CompleteCalcHead;
    2.23   autoCalculate 1 (Step 1);
    2.24   autoCalculate 1 (Step 1);
    2.25 - appendFormula 1 "x = 1"; 
    2.26 + appendFormula 1 "x = 1" |> Future.join; 
    2.27   (*... returns calcChangedEvent with*)
    2.28   val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
    2.29   getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
    2.30 @@ -1198,7 +1198,7 @@
    2.31   autoCalculate 1 CompleteCalcHead;
    2.32   autoCalculate 1 (Step 1);
    2.33   autoCalculate 1 (Step 1);
    2.34 - appendFormula 1 "x - 4711 = 0"; 
    2.35 + appendFormula 1 "x - 4711 = 0" |> Future.join; 
    2.36   (*... returns <ERROR> no derivation found </ERROR>*)
    2.37  
    2.38   val ((pt,_),_) = get_calc 1;
    2.39 @@ -1354,7 +1354,7 @@
    2.40  autoCalculate 1 CompleteCalcHead;
    2.41  autoCalculate 1 (Step 1);
    2.42  autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
    2.43 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; (*<<<<<<<=========================*)
    2.44 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" |> Future.join; (*<<<<<<<=========================*)
    2.45  (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
    2.46    would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
    2.47    results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
    2.48 @@ -1434,7 +1434,7 @@
    2.49  replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
    2.50  autoCalculate 1 CompleteCalcHead;
    2.51  autoCalculate 1 (Step 1);
    2.52 -appendFormula 1 "8 * x / (8 * y)";
    2.53 +appendFormula 1 "8 * x / (8 * y)" |> Future.join;
    2.54  (*<CALCMESSAGE> no derivation found </CALCMESSAGE> 
    2.55  --- but in BridgeLog Java <=> SML:
    2.56  <CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
     3.1 --- a/test/Tools/isac/Interpret/generate.sml	Sat Mar 08 11:07:52 2014 +0100
     3.2 +++ b/test/Tools/isac/Interpret/generate.sml	Mon Mar 10 21:07:35 2014 +0100
     3.3 @@ -23,7 +23,7 @@
     3.4  autoCalculate 1 CompleteCalcHead;
     3.5  autoCalculate 1 (Step 1);
     3.6  autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
     3.7 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
     3.8 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" |> Future.join;
     3.9  (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
    3.10    would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
    3.11    results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
     4.1 --- a/test/Tools/isac/Interpret/inform.sml	Sat Mar 08 11:07:52 2014 +0100
     4.2 +++ b/test/Tools/isac/Interpret/inform.sml	Mon Mar 10 21:07:35 2014 +0100
     4.3 @@ -60,7 +60,7 @@
     4.4   autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
     4.5   autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
     4.6  
     4.7 - appendFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
     4.8 + appendFormula 1 "-2 * 1 + (1 + x) = 0" |> Future.join; refFormula 1 (get_pos 1 1);
     4.9   val ((pt,_),_) = get_calc 1;
    4.10   val str = pr_ptree pr_short pt;
    4.11  if str =
    4.12 @@ -143,7 +143,7 @@
    4.13   Iterator 1; moveActiveRoot 1;
    4.14   autoCalculate 1 CompleteCalcHead;
    4.15   autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
    4.16 - appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1);
    4.17 + appendFormula 1 "2+ -1 + x = 2" |> Future.join; refFormula 1 (get_pos 1 1);
    4.18  
    4.19   moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
    4.20  
    4.21 @@ -180,7 +180,7 @@
    4.22   autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
    4.23   autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
    4.24  
    4.25 - appendFormula 1 "x = 2";
    4.26 + appendFormula 1 "x = 2" |> Future.join;
    4.27   val ((pt,p),_) = get_calc 1;
    4.28   val str = pr_ptree pr_short pt;
    4.29   writeln str;
    4.30 @@ -210,7 +210,7 @@
    4.31   autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
    4.32   autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
    4.33  
    4.34 - appendFormula 1 "x = 1";
    4.35 + appendFormula 1 "x = 1" |> Future.join;
    4.36   val ((pt,p),_) = get_calc 1;
    4.37   val str = pr_ptree pr_short pt;
    4.38   writeln str;
    4.39 @@ -239,7 +239,7 @@
    4.40   autoCalculate 1 CompleteCalcHead;
    4.41   autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
    4.42   autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
    4.43 - appendFormula 1 "[x = 3 + -2*1]";
    4.44 + appendFormula 1 "[x = 3 + -2*1]" |> Future.join;
    4.45   val ((pt,p),_) = get_calc 1;
    4.46   val str = pr_ptree pr_short pt;
    4.47   writeln str;
    4.48 @@ -525,7 +525,7 @@
    4.49  (([1], Res), a / b + c / d + e / f)] 
    4.50  *)
    4.51  "--- (1) input an arbitrary next formula";
    4.52 -appendFormula 1 "((a * d) + (c * b)) / (b * d) + e / f";
    4.53 +appendFormula 1 "((a * d) + (c * b)) / (b * d) + e / f" |> Future.join;
    4.54  val ((pt, p), _) = get_calc 1;
    4.55  (*show_pt pt;
    4.56  [
    4.57 @@ -556,7 +556,7 @@
    4.58  (([2], Res), (a * d + c * b) / (b * d) + e / f),
    4.59  (([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))]   <--- input this
    4.60  *)
    4.61 -appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)";
    4.62 +appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" |> Future.join;
    4.63  val ((pt, p), _) = get_calc 1;
    4.64  (*show_pt pt;
    4.65  [
    4.66 @@ -573,7 +573,7 @@
    4.67  else error ("inform.sml: [rational,simplification] 2");
    4.68  
    4.69  "--- (3) input the exact final result";
    4.70 -appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)";
    4.71 +appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" |> Future.join;
    4.72  val ((pt, p), _) = get_calc 1;
    4.73  (*show_pt pt;
    4.74  [
    4.75 @@ -1119,7 +1119,7 @@
    4.76  autoCalculate 1 CompleteCalcHead;
    4.77  autoCalculate 1 (Step 1);
    4.78  autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
    4.79 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)";
    4.80 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" |> Future.join;
    4.81    (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
    4.82    (*or
    4.83      <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
    4.84 @@ -1201,7 +1201,7 @@
    4.85  autoCalculate 1 CompleteCalcHead;
    4.86  autoCalculate 1 (Step 1);
    4.87  autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
    4.88 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; (*<<<<<<<=========================*)
    4.89 +appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" |> Future.join; (*<<<<<<<=========================*)
    4.90  (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
    4.91    would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
    4.92    results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
     5.1 --- a/test/Tools/isac/Knowledge/diff.sml	Sat Mar 08 11:07:52 2014 +0100
     5.2 +++ b/test/Tools/isac/Knowledge/diff.sml	Mon Mar 10 21:07:35 2014 +0100
     5.3 @@ -464,7 +464,7 @@
     5.4  autoCalculate 1 (Step 1);
     5.5  autoCalculate 1 (Step 1);
     5.6  val ((pt,p),_) = get_calc 1; show_pt pt;
     5.7 -appendFormula 1 "2*x + d_d x x + d_d x 1";
     5.8 +appendFormula 1 "2*x + d_d x x + d_d x 1" |> Future.join;
     5.9  val ((pt,p),_) = get_calc 1; show_pt pt;
    5.10  if existpt' ([3], Res) pt then ()
    5.11  else error  "diff.sml: inform d_d x (x^2 + x + 1) doesnt work";
     6.1 --- a/test/Tools/isac/Knowledge/simplify.sml	Sat Mar 08 11:07:52 2014 +0100
     6.2 +++ b/test/Tools/isac/Knowledge/simplify.sml	Mon Mar 10 21:07:35 2014 +0100
     6.3 @@ -59,7 +59,7 @@
     6.4  (([], Frm), Simplify (14 * x * y / (x * y))),
     6.5  (([1], Frm), 14 * x * y / (x * y))] *)
     6.6  
     6.7 -appendFormula 1 "14";
     6.8 +appendFormula 1 "14" |> Future.join;
     6.9  val ((pt,p),_) = get_calc 1; show_pt pt;
    6.10  (*[
    6.11  (([], Frm), Simplify (14 * x * y / (x * y))),