1.1 --- a/src/Tools/isac/Interpret/mathengine.sml	Sat Aug 27 09:40:52 2016 +0200
     1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml	Sat Aug 27 10:38:26 2016 +0200
     1.3 @@ -199,7 +199,8 @@
     1.4  		        in ("ok", (tacis, c', (pt', p'))) end
     1.5  	        else (case (if member op = [Pbl,Met] p_
     1.6  		                  then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
     1.7 -		                  handle _ => ([],[],ptp)(*e.g. Add_Given "equality///"*) of
     1.8 +		                  handle ERROR msg => (writeln ("*** " ^ msg);
     1.9 +		                    ([],[],ptp))(*e.g. Add_Given "equality///"*) of
    1.10  		              cs as ([],_,_) => ("helpless", cs)
    1.11  		            | cs => ("ok", cs))
    1.12  	    | _ => (case pIopt of
    1.13 @@ -210,7 +211,8 @@
    1.14  			                        (*^^^^^^^^: Apply_Method without init_form*)
    1.15  			                 then nxt_specify_ (pt, ip) 
    1.16                         else nxt_solve_ (pt,ip) )
    1.17 -			                handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality///"*) of
    1.18 +		                  handle ERROR msg => (writeln ("*** " ^ msg);
    1.19 +		                    ([],[],ptp))(*e.g. Add_Given "equality///"*) of
    1.20  		               cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*)
    1.21  			           | cs => ("ok", cs)))
    1.22    end;

     2.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Sat Aug 27 09:40:52 2016 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Sat Aug 27 10:38:26 2016 +0200
     2.3 @@ -96,7 +96,11 @@
     2.4        (["Programming","sort"], [],
     2.5          {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = e_rls, prls = e_rls,
     2.6            crls = Atools_crls, errpats = [], nrls = norm_Rational},
     2.7 -        "Script Sortprog (u_u::int xlist) = (Rewrite_Set ins_sort False) u_u")
     2.8 +        "Script Sortprog (unso :: int xlist) = " ^
     2.9 +        "  (let uns = Take (sort unso) " ^
    2.10 +        "  in " ^
    2.11 +        "    (Rewrite_Set ins_sort False) uns" ^
    2.12 +        "  )")
    2.13    ]
    2.14  *}
    2.15  end

     3.1 --- a/test/Tools/isac/Test_Some.thy	Sat Aug 27 09:40:52 2016 +0200
     3.2 +++ b/test/Tools/isac/Test_Some.thy	Sat Aug 27 10:38:26 2016 +0200
     3.3 @@ -32,6 +32,29 @@
     3.4  section {* ===================================================================================*}
     3.5  ML {*
     3.6  *} ML {*
     3.7 +"----------- insertion sort with MathEngine: DONE insert \<longrightarrow> 200-start-method.sml-------------";
     3.8 +"----------- insertion sort with MathEngine: TODO ----------------------------";
     3.9 +val fmz = ["unsorted [||1, 3, 2||]", "sorted s_s"];
    3.10 +val (dI',pI',mI') = ("InsSort", ["insertion","sort","Programming"], ["Programming","sort"]);
    3.11 +val p = e_pos'; val c = []; 
    3.12 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = ("Model_Problem",..*)
    3.13 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    3.14 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    3.15 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    3.16 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Specify_Problem",..*)
    3.17 +"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
    3.18 +val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt p [] pt; (* (@1) nxt'''' = ("Specify_Method",..*)
    3.19 +(*val..nxt..*)me nxt'''' p'''' [] pt''''; (* nxt = ERROR("Empty_Tac", SHOULD BE("Apply_Method",..*)
    3.20 +"~~~~~ we continue with (@1) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
    3.21 +val (p, f, nxt, pt) = (p'''',f'''',nxt'''',pt'''');
    3.22 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
    3.23 +    val (pt, p) = 
    3.24 +	    (*locatetac is here for testing by me; step would suffice in me*)
    3.25 +	    case locatetac tac (pt,p) of
    3.26 +		    ("ok", (_, _, ptp)) => ptp | _ => error "CHANGED --- Minisubplb/200-start-method 1"
    3.27 +(* step p ((pt, e_pos'),[])  ..ERROR  = ("helpless",  NOW STOPPED ! ! ! ! ! ! ! ! ! ! ! ! ! ! *);
    3.28 +*} ML {*
    3.29 +step p ((pt, e_pos'),[])(*INSTEAD '("helpless"..' STOPPED WITH "ERROR in creating the environment"*)
    3.30  *} ML {*
    3.31  *} ML {*
    3.32  *}