# HG changeset patch
# User wenzelm
# Date 1468939839 -7200
# Node ID 54e932f0c30a298a1c2257cc37a1b24b430b65ad
# Parent  2000e11586675bcbe0de9e96f032726e38430054
misc tuning and simplification;

diff -r 2000e1158667 -r 54e932f0c30a src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue Jul 19 16:35:51 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Tue Jul 19 16:50:39 2016 +0200
@@ -290,7 +290,7 @@
 structure Inttriplefunc = FuncFun(type key = int * int * int val ord = triple_int_ord);
 
 
-(* More parser basics. *)
+(* Parse back csdp output. *)
 
 local
 
@@ -306,29 +306,22 @@
 fun signed neg parse = $$ "-" |-- parse >> neg || $$ "+" |-- parse || parse;
 val exponent = ($$ "e" || $$ "E") |-- signed ~ decimal_nat;
 
-in
-
 val decimal =
   signed ~ decimal_sig -- Scan.optional exponent 0
     >> (fn (a, b) => a * rat_pow @10 b);
 
+val csdp_output =
+  decimal -- Scan.repeat (Scan.$$ " " |-- Scan.option decimal) --| Scan.many Symbol.not_eof
+    >> (fn (a, bs) => vector_of_list (a :: map_filter I bs));
+
+in
+
+fun parse_csdpoutput s =
+  Symbol.scanner "Malformed CSDP output" csdp_output (raw_explode s);
+
 end;
 
 
-(* Parse back csdp output. *)
-
-(* FIXME improper use of parser combinators ahead *)
-
-fun mkparser p s =
-  let val (x,rst) = p (raw_explode s)
-  in if null rst then x else error "mkparser: unparsed input" end;
-
-fun ignore _ = ((),[])
-fun csdpoutput inp =
-  ((decimal -- Scan.repeat (Scan.$$ " " |-- Scan.option decimal) >>
-    (fn (h,to) => map_filter I ((SOME h)::to))) --| ignore >> vector_of_list) inp
-val parse_csdpoutput = mkparser csdpoutput
-
 (* Try some apparently sensible scaling first. Note that this is purely to   *)
 (* get a cleaner translation to floating-point, and doesn't affect any of    *)
 (* the results, in principle. In practice it seems a lot better when there   *)