src/Tools/isac/Specify/p-spec.sml
changeset 60741 22586d7fedb0
parent 60729 43d11e7742e1
child 60744 8f153b365de2
equal deleted inserted replaced
60740:51b4f393518d 60741:22586d7fedb0
   203 	                (#2 (References.select_input ospec spec))
   203 	                (#2 (References.select_input ospec spec))
   204 		            val (_, where_) = Pre_Conds.check ctxt where_rls where_ pits 0
   204 		            val (_, where_) = Pre_Conds.check ctxt where_rls where_ pits 0
   205 ( *T_TEST**)
   205 ( *T_TEST**)
   206 	              val {where_rls, where_, model, ...} = Problem.from_store ctxt
   206 	              val {where_rls, where_, model, ...} = Problem.from_store ctxt
   207 	                (#2 (References.select_input ospec spec))
   207 	                (#2 (References.select_input ospec spec))
   208 		            val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_
   208 		            val (_, where_) = Pre_Conds.check ctxt where_rls where_
   209 		              (model, I_Model.OLD_to_TEST pits)
   209 		              (model, I_Model.OLD_to_TEST pits)
   210 (*T_TESTnew*)
   210 (*T_TESTnew*)
   211 	            in (Ctree.update_pbl pt p pits,
   211 	            in (Ctree.update_pbl pt p pits,
   212 		                 (SpecificationC.is_complete' pits where_ spec, Pos.Pbl, hdf', pits, where_, spec)) 
   212 		                 (SpecificationC.is_complete' pits where_ spec, Pos.Pbl, hdf', pits, where_, spec)) 
   213               end
   213               end
   218 	                (#3 (References.select_input ospec spec))
   218 	                (#3 (References.select_input ospec spec))
   219 		            val (_, where_) = Pre_Conds.check ctxt where_rls where_ mits 0
   219 		            val (_, where_) = Pre_Conds.check ctxt where_rls where_ mits 0
   220 ( *T_TEST**)
   220 ( *T_TEST**)
   221 	              val {where_rls,where_, model, ...} = MethodC.from_store ctxt 
   221 	              val {where_rls,where_, model, ...} = MethodC.from_store ctxt 
   222 	                (#3 (References.select_input ospec spec))
   222 	                (#3 (References.select_input ospec spec))
   223 		            val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_
   223 		            val (_, where_) = Pre_Conds.check ctxt where_rls where_
   224 		              (model, I_Model.OLD_to_TEST mits)
   224 		              (model, I_Model.OLD_to_TEST mits)
   225 (*T_TESTnew*)
   225 (*T_TESTnew*)
   226 	            in (Ctree.update_met pt p mits,
   226 	            in (Ctree.update_met pt p mits,
   227 		                  (SpecificationC.is_complete' mits where_ spec, Pos.Met, hdf', mits, where_, spec))
   227 		                  (SpecificationC.is_complete' mits where_ spec, Pos.Met, hdf', mits, where_, spec))
   228               end
   228               end