1.1 --- a/src/Tools/isac/Frontend/states.sml Thu Jun 05 18:10:46 2014 +0200
1.2 +++ b/src/Tools/isac/Frontend/states.sml Fri Jun 06 06:50:02 2014 +0200
1.3 @@ -141,14 +141,6 @@
1.4 type iterID = int;
1.5 type calcID = int;
1.6
1.7 -(*FIXME.WN.9.03: ev. resdesign calcstate + pos for CalcIterator
1.8 -type state =
1.9 - (*pos' * set by the CalcIterator ---> for each user*)
1.10 - calcstate; (*to which ev.included 'preview' tac_s could be applied*)
1.11 -val e_state = (e_pos', e_calcstate):state;
1.12 -val states = Unsynchronized.ref ([]:(iterID * (calcID * state) list) list);
1.13 -*)
1.14 -
1.15 val states = Unsynchronized.ref
1.16 ([]:(calcID *
1.17 (calcstate *
2.1 --- a/src/Tools/isac/Interpret/ctree.sml Thu Jun 05 18:10:46 2014 +0200
2.2 +++ b/src/Tools/isac/Interpret/ctree.sml Fri Jun 06 06:50:02 2014 +0200
2.3 @@ -850,7 +850,7 @@
2.4 in pr_pt f [] pt end;
2.5 (*
2.6 > fun prfn ps b = (pr_pos ps)^" "^b(*TODO*)^"\n";
2.7 -> val pt = Unsynchronized.ref EmptyPtree;
2.8 +(*val pt = Unsynchronized.ref EmptyPtree;*)
2.9 > pt:=Nd("root'",
2.10 [Nd("xx1",[]),
2.11 Nd("xx2",
2.12 @@ -1048,7 +1048,7 @@
2.13 (*
2.14 > type ppobj = string;
2.15 > tracing (pr_ptree prfn (!pt));
2.16 - val pt = Unsynchronized.ref Empty;
2.17 +(*val pt = Unsynchronized.ref Empty;*)
2.18 pt:= insert_pt ("root'":ppobj) EmptyPtree [];
2.19 pt:= insert_pt ("xx1":ppobj) (!pt) [1];
2.20 pt:= insert_pt ("xx2":ppobj) (!pt) [2];
3.1 --- a/src/Tools/isac/Interpret/script.sml Thu Jun 05 18:10:46 2014 +0200
3.2 +++ b/src/Tools/isac/Interpret/script.sml Fri Jun 06 06:50:02 2014 +0200
3.3 @@ -160,10 +160,6 @@
3.4 > get [] (eq_str "e_") sss; [R,R]
3.5 *)
3.6
3.7 -fun test_negotiable t =
3.8 - member op = (!negotiable)
3.9 - ((strip_thy o (term_str (Thy_Info.get_theory "Script")) o head_of) t);
3.10 -
3.11 (*.get argument of first stactic in a script for init_form.*)
3.12 fun get_stac thy (h $ body) =
3.13 let
4.1 --- a/src/Tools/isac/ProgLang/Script.thy Thu Jun 05 18:10:46 2014 +0200
4.2 +++ b/src/Tools/isac/ProgLang/Script.thy Fri Jun 06 06:50:02 2014 +0200
4.3 @@ -142,42 +142,4 @@
4.4 *** ("_Letpar" ("_bind" x a) e) -> (Letpar a ("_abs" x e))
4.5 *** At command "translations" (line 140 of "/usr/local/isabisac/src/Pure/isac/Scripts/Script").
4.6 *)
4.7 -
4.8 -ML {* (*the former Script.ML*)
4.9 -
4.10 -(*--vvv----- SHIFT? or delete ?*)
4.11 -val IDTyp = Type("Script.ID",[]);
4.12 -
4.13 -val tacs = Unsynchronized.ref (distinct (remove op = ""
4.14 - ["Calculate",
4.15 - "Rewrite","Rewrite'_Inst","Rewrite'_Set","Rewrite'_Set'_Inst",
4.16 - "Substitute","Tac","Check'_elementswise",
4.17 - "Take","Subproblem","Or'_to'_List"]));
4.18 -
4.19 -val screxpr = Unsynchronized.ref (distinct (remove op = ""
4.20 - ["Let","If","Repeat","While","Try","Or"]));
4.21 -
4.22 -val listfuns = Unsynchronized.ref [(*_all_ functions in Isa99.List.thy *)
4.23 - "@","filter","concat","foldl","hd","last","set","list_all",
4.24 - "map","mem","nth","list_update","take","drop",
4.25 - "takeWhile","dropWhile","tl","butlast",
4.26 - "rev","zip","upt","remdups","nodups","replicate",
4.27 -
4.28 - "Cons","Nil"];
4.29 -
4.30 -val scrfuns = Unsynchronized.ref ([]: string list);
4.31 -
4.32 -val listexpr = Unsynchronized.ref (union op = (!listfuns) (!scrfuns));
4.33 -
4.34 -val notsimp = Unsynchronized.ref
4.35 - (distinct (remove op = ""
4.36 - (!tacs @ !screxpr @ (*!subpbls @*) !scrfuns @ !listfuns)));
4.37 -
4.38 -val negotiable = Unsynchronized.ref ((!tacs (*@ !subpbls*)));
4.39 -
4.40 -val tacpbl = Unsynchronized.ref
4.41 - (distinct (remove op = "" (!tacs (*@ !subpbls*))));
4.42 -(*--^^^----- SHIFT? or delete ?*)
4.43 -*}
4.44 -
4.45 end
5.1 --- a/src/Tools/isac/calcelems.sml Thu Jun 05 18:10:46 2014 +0200
5.2 +++ b/src/Tools/isac/calcelems.sml Fri Jun 06 06:50:02 2014 +0200
5.3 @@ -427,16 +427,10 @@
5.4 (*see 'How to manage theorys in subproblems' at 'type thyID'*)
5.5 val theory' = Unsynchronized.ref ([]:(theory' * theory) list);
5.6
5.7 -(* theories for html representation: Isabelle, Knowledge, ProgLang *)
5.8 -val isabthys = Unsynchronized.ref ([] : theory list);
5.9 -val knowthys = Unsynchronized.ref ([] : theory list);
5.10 -val progthys = Unsynchronized.ref ([] : theory list);
5.11 -
5.12 (*rewrite orders, also stored in 'type met' and type 'and rls'
5.13 The association list is required for 'rewrite.."rew_ord"..'
5.14 WN0509 tests not well-organized: see smltest/Knowledge/termorder.sml*)
5.15 -val rew_ord' =
5.16 - Unsynchronized.ref
5.17 +val rew_ord' = Unsynchronized.ref
5.18 ([]:(rew_ord' * (*the key for the association list *)
5.19 (subst (*the bound variables - they get high order*)
5.20 -> (term * term) (*(t1, t2) to be compared *)
5.21 @@ -499,9 +493,6 @@
5.22 val isab_thm_thy = Unsynchronized.ref ([] : (thmDeriv * term) list);
5.23 val isabthys = Unsynchronized.ref ([] : theory list);
5.24
5.25 -val first_ProgLang_thy = Unsynchronized.ref (@{theory Pure});
5.26 -val first_Knowledge_thy = Unsynchronized.ref (@{theory Pure});
5.27 -
5.28
5.29 type path = string;
5.30 type filename = string;
5.31 @@ -887,17 +878,8 @@
5.32 scr = EmptyScr: scr}:met;
5.33
5.34
5.35 -(** problem-types stored in format for usage in specify **)
5.36 -(*25.8.01 ----
5.37 -val pbltypes = Unsynchronized.ref ([(e_pblID,[])]:(pblID * ((string * (* field "#Given",..*)
5.38 - (term * (* description *)
5.39 - term)) (* id | struct-var *)
5.40 - list)
5.41 - ) list);*)
5.42 -
5.43 val e_Mets = Ptyp ("e_metID",[e_met],[]);
5.44
5.45 -
5.46 type mets = (met ptyp) list;
5.47
5.48 fun coll_metguhs mets =