1.1 --- a/src/Tools/isac/ME/script.sml Thu Aug 19 15:41:56 2010 +0200
1.2 +++ b/src/Tools/isac/ME/script.sml Fri Aug 20 12:25:37 2010 +0200
1.3 @@ -105,13 +105,6 @@
1.4 > val des = de_esc_underscore esc;
1.5 val des = de_esc_underscore esc;*)
1.6
1.7 -
1.8 -(*WN.12.5.03 not used any more,
1.9 - tacs are more stable than listepxr: subst_tacexpr
1.10 -fun is_listexpr t =
1.11 - (((ids_of o head_of) t) inter (!listexpr)) <> [];
1.12 -----*)
1.13 -
1.14 (*go at a location in a script and fetch the contents*)
1.15 fun go [] t = t
1.16 | go (D::p) (Abs(s,ty,t0)) = go (p:loc_) t0
1.17 @@ -246,7 +239,7 @@
1.18 | itr_arg _ (Const ("Script.SubProblem",_) $ _ $ _) = e_term
1.19 | itr_arg thy t = raise error
1.20 ("itr_arg not impl. for "^
1.21 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));
1.22 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));
1.23 (* val t = (term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";
1.24 > itr_arg "Script.thy" t;
1.25 val it = Free ("e_","RealDef.real") : term
1.26 @@ -595,9 +588,9 @@
1.27 (case stac of
1.28 (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
1.29 ((*writeln("3### assod: stac = "^
1.30 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));
1.31 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));
1.32 writeln("3### assod: f(m)= "^
1.33 - (Sign.string_of_term (sign_of (assoc_thy thy)) f));*)
1.34 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) f));*)
1.35 if thmID = thmID_ then
1.36 if f = f_ then ((*writeln"3### assod ..Ass";*)Ass (m,f'))
1.37 else ((*writeln"### assod ..AssWeak";
1.38 @@ -1563,7 +1556,7 @@
1.39 | appy thy ptp E (*env*) l
1.40 (Const ("Script.Repeat"(*2*),_) $ e) a v =
1.41 ((*writeln("3### appy Repeat: a= "^
1.42 - (Sign.string_of_term (sign_of (assoc_thy thy)) a));*)
1.43 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) a));*)
1.44 appy thy ptp E (*env*) (l@[R]) e a v)
1.45 (* val (thy, ptp, E, l, (t as Const ("Script.Try",_) $ e $ a), _, v)=
1.46 (thy, ptp, E, (l@[R]), e2, a, v);
1.47 @@ -1572,7 +1565,7 @@
1.48 (t as Const ("Script.Try",_) $ e $ a) _ v =
1.49 (case appy thy ptp E (l@[L,R]) e (SOME a) v of
1.50 Napp E => ((*writeln("### appy Try "^
1.51 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
1.52 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
1.53 Skip (v, E))
1.54 | ay => ay)
1.55 (* val (thy, ptp, E, l, (t as Const ("Script.Try",_) $ e), _, v)=
1.56 @@ -1584,7 +1577,7 @@
1.57 (t as Const ("Script.Try",_) $ e) a v =
1.58 (case appy thy ptp E (l@[R]) e a v of
1.59 Napp E => ((*writeln("### appy Try "^
1.60 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
1.61 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
1.62 Skip (v, E))
1.63 | ay => ay)
1.64
1.65 @@ -1688,7 +1681,7 @@
1.66 | nxt_up thy ptp scr E l ay
1.67 (t as Abs (_,_,_)) a v =
1.68 ((*writeln("### nxt_up Abs: "^
1.69 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
1.70 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
1.71 nstep_up thy ptp scr E (*enr*) l ay a v)
1.72
1.73 | nxt_up thy ptp scr E l ay
1.74 @@ -1696,7 +1689,7 @@
1.75 ((*writeln("### nxt_up Let$e$Abs: is=");
1.76 writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
1.77 (*writeln("### nxt_up Let e Abs: "^
1.78 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
1.79 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
1.80 nstep_up thy ptp scr (*upd_env*) E (*a,v)*)
1.81 (*eno,upd_env env (iar,res),iar,res,saf*) l ay a v)
1.82
1.83 @@ -1751,7 +1744,7 @@
1.84 | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
1.85 (t as Const ("Script.Try",_) $ e $ _) a v =
1.86 ((*writeln("### nxt_up Try "^
1.87 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
1.88 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
1.89 nstep_up thy ptp scr E l Skip_ a v )
1.90 (* val (thy, ptp, scr, E, l, _,(t as Const ("Script.Try",_) $ e), a, v) =
1.91 (thy, ptp, (Script sc),
1.92 @@ -1760,7 +1753,7 @@
1.93 | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
1.94 (t as Const ("Script.Try"(*2*),_) $ e) a v =
1.95 ((*writeln("### nxt_up Try "^
1.96 - (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
1.97 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
1.98 nstep_up thy ptp scr E l Skip_ a v)
1.99
1.100
1.101 @@ -1805,7 +1798,7 @@
1.102
1.103 | nxt_up (thy,_) ptp scr E l ay t a v =
1.104 raise error ("nxt_up not impl for "^
1.105 - (Sign.string_of_term (sign_of (assoc_thy thy)) t))
1.106 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t))
1.107
1.108 (* val (thy, ptp, (Script sc), E, l, ay, a, v)=
1.109 (thy, ptp, scr, E, l, Skip_, a, v);
1.110 @@ -1815,13 +1808,13 @@
1.111 and nstep_up thy ptp (Script sc) E l ay a v =
1.112 ((*writeln("### nstep_up from: "^(loc_2str l));
1.113 writeln("### nstep_up from: "^
1.114 - (Sign.string_of_term (sign_of (assoc_thy thy)) (go l sc)));*)
1.115 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) (go l sc)));*)
1.116 if 1 < length l
1.117 then
1.118 let
1.119 val up = drop_last l;
1.120 in ((*writeln("### nstep_up to: "^
1.121 - (Sign.string_of_term (sign_of (assoc_thy thy)) (go up sc)));*)
1.122 + (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) (go up sc)));*)
1.123 nxt_up thy ptp (Script sc) E up ay (go up sc) a v ) end
1.124 else (*interpreted to end*)
1.125 if ay = Skip_ then Skip (v, E) else Napp E