src/HOL/Matrix/cplex/Cplex_tools.ML
changeset 17521 0f1c48de39f5
parent 17412 e26cb20ef0cc
child 21056 2cfe839e8d58
equal deleted inserted replaced
17520:8581c151adea 17521:0f1c48de39f5
   967 	    end
   967 	    end
   968 	
   968 	
   969 	val header = readHeader () 
   969 	val header = readHeader () 
   970 
   970 
   971 	val result = 
   971 	val result = 
   972 	    case assoc (header, "STATUS") of
   972 	    case AList.lookup (op =) header "STATUS" of
   973 		SOME "INFEASIBLE" => Infeasible
   973 		SOME "INFEASIBLE" => Infeasible
   974 	      | SOME "UNBOUNDED" => Unbounded
   974 	      | SOME "UNBOUNDED" => Unbounded
   975 	      | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")), 
   975 	      | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"), 
   976 					   (skip_until_sep (); 
   976 					   (skip_until_sep (); 
   977 					    skip_until_sep ();
   977 					    skip_until_sep ();
   978 					    load_values ()))
   978 					    load_values ()))
   979 	      | _ => Undefined
   979 	      | _ => Undefined
   980 
   980 
  1116 	    end
  1116 	    end
  1117 	
  1117 	
  1118 	val header = readHeader ()
  1118 	val header = readHeader ()
  1119 
  1119 
  1120 	val result = 
  1120 	val result = 
  1121 	    case assoc (header, "STATUS") of
  1121 	    case AList.lookup (op =) header "STATUS" of
  1122 		SOME "INFEASIBLE" => Infeasible
  1122 		SOME "INFEASIBLE" => Infeasible
  1123 	      | SOME "NONOPTIMAL" => Unbounded
  1123 	      | SOME "NONOPTIMAL" => Unbounded
  1124 	      | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")), 
  1124 	      | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"), 
  1125 					   (skip_paragraph (); 
  1125 					   (skip_paragraph (); 
  1126 					    skip_paragraph (); 
  1126 					    skip_paragraph (); 
  1127 					    skip_paragraph (); 
  1127 					    skip_paragraph (); 
  1128 					    skip_paragraph (); 
  1128 					    skip_paragraph (); 
  1129 					    skip_paragraph ();
  1129 					    skip_paragraph ();