1.1 --- a/src/Tools/isac/Interpret/script.sml Sat Aug 27 11:26:28 2016 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Sat Aug 27 16:57:18 2016 +0200
1.3 @@ -303,6 +303,8 @@
1.4 !: FIXXXME penv: push it here in itms2args into script-evaluation*)
1.5 (* val (thy, mI, itms) = (thy, metID, itms);
1.6 *)
1.7 +val errmsg =
1.8 + "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
1.9 fun itms2args thy mI (itms:itm list) =
1.10 let val mvat = max_vt itms
1.11 fun okv mvat (_,vats,b,_,_) = member op = vats mvat andalso b
1.12 @@ -317,6 +319,7 @@
1.13 | SOME (_,_,_,_,itm_) => penvval_in itm_
1.14 fun sel_given_find (s,_) = (s = "#Given") orelse (s = "#Find")
1.15 val pats = (#ppc o get_met) mI
1.16 + val _ = if pats = [] then raise ERROR errmsg else ()
1.17 in (flat o (map (itm2arg itms))) pats end;
1.18 (*
1.19 > val sc = ... Solve_root_equation ...
1.20 @@ -1483,9 +1486,11 @@
1.21
1.22
1.23 (*.create the initial interpreter state from the items of the guard.*)
1.24 +val errmsg = "ERROR: found no actual arguments for prog. of "
1.25 fun init_scrstate thy itms metID =
1.26 let
1.27 val actuals = itms2args thy metID itms
1.28 + val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
1.29 val scr as Prog sc = (#scr o get_met) metID
1.30 val formals = formal_args sc
1.31 (*expects same sequence of (actual) args in itms and (formal) args in met*)