equal
deleted
inserted
replaced
69 fun get_calc (cI: calcID) = |
69 fun get_calc (cI: calcID) = |
70 case assoc (Synchronized.value states, cI) of |
70 case assoc (Synchronized.value states, cI) of |
71 NONE => raise ERROR ("get_calc " ^ string_of_int cI ^ " not existent") |
71 NONE => raise ERROR ("get_calc " ^ string_of_int cI ^ " not existent") |
72 | SOME (c, _) => |
72 | SOME (c, _) => |
73 let |
73 let |
74 val (_, tacis) = c |
74 (*val (_, tacis) = c |
75 (*val _ = if length tacis > 1 then raise ERROR "length tacis > 1" else () |
75 val _ = if length tacis > 1 then raise ERROR "length tacis > 1" else () |
76 in Test_Isac.thy raise ERROR in Interpret/inform.sml*) |
76 in Test_Isac.thy raise ERROR in Interpret/inform.sml*) |
77 in c end; |
77 in c end; |
78 fun get_pos (cI: calcID) (uI: iterID) = |
78 fun get_pos (cI: calcID) (uI: iterID) = |
79 case assoc (Synchronized.value states, cI) of |
79 case assoc (Synchronized.value states, cI) of |
80 NONE => raise ERROR ("get_pos: calc " ^ (string_of_int cI) |
80 NONE => raise ERROR ("get_pos: calc " ^ (string_of_int cI) |
86 | SOME p => p); |
86 | SOME p => p); |
87 |
87 |
88 |
88 |
89 fun del_assoc ([],_) = [] |
89 fun del_assoc ([],_) = [] |
90 | del_assoc a = |
90 | del_assoc a = |
91 let fun del ([], key) ps = ps |
91 let fun del ([], _) ps = ps |
92 | del ((keyi, xi) :: pairs, key) ps = |
92 | del ((keyi, xi) :: pairs, key) ps = |
93 if key = keyi then ps @ pairs |
93 if key = keyi then ps @ pairs |
94 else del (pairs, key) (ps @ [(keyi, xi)]) |
94 else del (pairs, key) (ps @ [(keyi, xi)]) |
95 in del a [] end; |
95 in del a [] end; |
96 (* |
96 (* |
169 in states:= overwrite2 ((!states), ((uI, pI), (ip, calc))) end;*) |
169 in states:= overwrite2 ((!states), ((uI, pI), (ip, calc))) end;*) |
170 fun upd_ipos (cI: calcID) (uI: iterID) (ip: Pos.pos') = Synchronized.change states |
170 fun upd_ipos (cI: calcID) (uI: iterID) (ip: Pos.pos') = Synchronized.change states |
171 (fn s => case assoc (s, cI) of |
171 (fn s => case assoc (s, cI) of |
172 NONE => |
172 NONE => |
173 raise ERROR ("upd_ipos: calctree " ^ (string_of_int cI) ^ " not existent") |
173 raise ERROR ("upd_ipos: calctree " ^ (string_of_int cI) ^ " not existent") |
174 | SOME (cs, us) => overwrite2 (s, ((cI, uI), ip))); |
174 | SOME _ => overwrite2 (s, ((cI, uI), ip))); |
175 |
175 |
176 |
176 |
177 (** add and delete calcs **) |
177 (** add and delete calcs **) |
178 |
178 |
179 (*///7.10 |
179 (*///7.10 |
202 new_calcID end; *) |
202 new_calcID end; *) |
203 fun add_user (cI: calcID) = Synchronized.change_result states |
203 fun add_user (cI: calcID) = Synchronized.change_result states |
204 (fn s => case assoc (s, cI) of |
204 (fn s => case assoc (s, cI) of |
205 NONE => |
205 NONE => |
206 raise ERROR ("add_user: calctree " ^ (string_of_int cI) ^ " not existent") |
206 raise ERROR ("add_user: calctree " ^ (string_of_int cI) ^ " not existent") |
207 | SOME (cs, us) => |
207 | SOME (_, us) => |
208 let |
208 let |
209 val new_uI = new_key us 1 |
209 val new_uI = new_key us 1 |
210 in (new_uI: iterID, overwrite2 (s, ((cI, new_uI), Pos.e_pos'))) end); |
210 in (new_uI: iterID, overwrite2 (s, ((cI, new_uI), Pos.e_pos'))) end); |
211 |
211 |
212 (*///10.10. |
212 (*///10.10. |