src/Tools/isac/Frontend/states.sml
branchisac-update-Isa09-2
changeset 38007 d679c1f837a7
parent 38006 16d56796f5a0
child 38031 460c24a6a6ba
equal deleted inserted replaced
38006:16d56796f5a0 38007:d679c1f837a7
   147      calcstate;       (*to which ev.included 'preview' tac_s could be applied*)
   147      calcstate;       (*to which ev.included 'preview' tac_s could be applied*)
   148 val e_state = (e_pos', e_calcstate):state;
   148 val e_state = (e_pos', e_calcstate):state;
   149 val states = Unsynchronized.ref ([]:(iterID * (calcID * state) list) list);
   149 val states = Unsynchronized.ref ([]:(iterID * (calcID * state) list) list);
   150 *)
   150 *)
   151 
   151 
   152 val states = 
   152 val states = Unsynchronized.ref
   153     ref ([]:(calcID * 
   153         ([]:(calcID * 
   154 	     (calcstate * 
   154 	     (calcstate * 
   155 	      (iterID *       (*1 sets the 'active formula'*)
   155 	      (iterID *       (*1 sets the 'active formula'*)
   156 	       pos'           (*for iterator of a user     *)
   156 	       pos'           (*for iterator of a user     *)
   157 	       ) list)) list);
   157 	       ) list)) list);
   158 (*
   158 (*