1.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml	Tue May 19 12:33:35 2020 +0200
     1.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml	Wed May 20 12:52:09 2020 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4  "----------- change to parse ctxt -----------------------";
     1.5  "----------- change to parse ctxt -----------------------";
     1.6  "===== start calculation: from problem description (fmz) to origin";
     1.7 -val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
     1.8 +val fmz = ["realTestGiven (((1+2)*4/3)^^^2)", "realTestFind s"];
     1.9  val (thyID, pblID, metID) =
    1.10    ("Test", ["calculate", "test"], ["Test", "test_calculate"]);
    1.11  (*======= Isabelle2013-2 --> Isabelle2014: unclear, why this test ever run =====================*)
    1.12 @@ -34,9 +34,9 @@
    1.13  "----------- debugging setContext..pbl_ -----------------";
    1.14  "----------- debugging setContext..pbl_ -----------------";
    1.15  reset_states ();
    1.16 -CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
    1.17 -  ("Test", ["sqroot-test","univariate","equation","test"],
    1.18 -   ["Test","squ-equ-test-subpbl1"]))];
    1.19 +CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], 
    1.20 +  ("Test", ["sqroot-test", "univariate", "equation", "test"],
    1.21 +   ["Test", "squ-equ-test-subpbl1"]))];
    1.22  Iterator 1;
    1.23  moveActiveRoot 1; modelProblem 1;
    1.24  
    1.25 @@ -46,14 +46,14 @@
    1.26  val ((pt,_),_) = get_calc 1;
    1.27  val pp = par_pblobj pt p;
    1.28  val keID = Ptool.guh2kestoreID guh;
    1.29 -case context_pbl keID pt pp of (true,["univariate","equation"],_,_,_)=>()
    1.30 +case context_pbl keID pt pp of (true,["univariate", "equation"],_,_,_)=>()
    1.31  | _ => error "mathengine.sml: context_pbl .. pbl_equ_univ checked";
    1.32  
    1.33  case get_obj g_spec pt p of (_, ["empty_probl_id"], _) => ()
    1.34  | _ => error "mathengine.sml: context_pbl .. pbl still empty";
    1.35  setContext 1 pos guh;
    1.36  val ((pt,_),_) = get_calc 1;
    1.37 -case get_obj g_spec pt p of (_, ["univariate","equation"], _) => ()
    1.38 +case get_obj g_spec pt p of (_, ["univariate", "equation"], _) => ()
    1.39  | _ => error "mathengine.sml: context_pbl .. pbl set";
    1.40  
    1.41  
    1.42 @@ -69,21 +69,21 @@
    1.43  reset_states ();
    1.44  CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", 
    1.45  	    "solveFor x", "solutions L"],
    1.46 -	   ("RatEq",["univariate","equation"],["no_met"]))];
    1.47 +	   ("RatEq",["univariate", "equation"],["no_met"]))];
    1.48  Iterator 1;
    1.49  moveActiveRoot 1; autoCalculate 1 CompleteCalc;
    1.50  
    1.51  refineProblem 1 ([1],Res) "pbl_equ_univ" 
    1.52  (*gives "pbl_equ_univ_rat" correct*);
    1.53  
    1.54 -refineProblem 1 ([1],Res) (Ptool.pblID2guh ["LINEAR","univariate","equation"])
    1.55 +refineProblem 1 ([1],Res) (Ptool.pblID2guh ["LINEAR", "univariate", "equation"])
    1.56  (*gives "pbl_equ_univ_lin" incorrect*);
    1.57  
    1.58  "--------- search for Or_to_List ------------------------";
    1.59  "--------- search for Or_to_List ------------------------";
    1.60  "--------- search for Or_to_List ------------------------";
    1.61 -val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"];
    1.62 -val (dI',pI',mI') = ("Isac_Knowledge", ["univariate","equation"], ["no_met"])
    1.63 +val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x", "solutions L"];
    1.64 +val (dI',pI',mI') = ("Isac_Knowledge", ["univariate", "equation"], ["no_met"])
    1.65  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.66  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.67  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.68 @@ -139,7 +139,7 @@
    1.69  val fmz = ["filterExpression (X  = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", "boundVariable z",
    1.70    "stepResponse (x[n::real]::bool)"];
    1.71  val (dI,pI,mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"], 
    1.72 -  ["SignalProcessing","Z_Transform","Inverse"]);
    1.73 +  ["SignalProcessing", "Z_Transform", "Inverse"]);
    1.74  
    1.75  val (p,_,fb,nxt,_,pt)  = CalcTreeTEST [(fmz, (dI,pI,mI))]; 
    1.76  (*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
    1.77 @@ -177,7 +177,7 @@
    1.78  "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
    1.79  reset_states ();
    1.80  CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
    1.81 -  ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
    1.82 +  ("Test",["sqroot-test", "univariate", "equation", "test"],["Test", "squ-equ-test-subpbl1"]))];
    1.83  moveActiveRoot 1;
    1.84  autoCalculate 1 CompleteCalcHead;
    1.85  autoCalculate 1 (Steps 1);
    1.86 @@ -298,7 +298,7 @@
    1.87  "----------- improved fun getTactic for interSteps and numeral calculations --";
    1.88  reset_states (); val cI = 1;
    1.89  CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
    1.90 -  ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
    1.91 +  ("Test",["sqroot-test", "univariate", "equation", "test"],["Test", "squ-equ-test-subpbl1"]))];
    1.92  moveActiveRoot 1;
    1.93  autoCalculate 1 CompleteCalcHead;
    1.94  autoCalculate 1 (Steps 1);