# HG changeset patch
# User wenzelm
# Date 1380378977 -7200
# Node ID c6297fa1031aac101dc943502aa77731b330c531
# Parent  c4156b37627f1652c3fc632870bd3f2992e13b28
proper wrapper for parser -- more explicit error;

diff -r c4156b37627f -r c6297fa1031a src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Sep 28 16:10:26 2013 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Sep 28 16:36:17 2013 +0200
@@ -298,19 +298,17 @@
  val decimal = signed decimalsig -- (emptyin rat_0|| exponent)
     >> (fn (h, x) => h */ pow10 (int_of_rat x));
 
- fun mkparser p s =
-  let val (x,rst) = p (raw_explode s)
-  in if null rst then x
-     else error "mkparser: unparsed input"
-  end;;
-
 (* Parse back csdp output.                                                      *)
 
  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
+
+ fun parse_csdpoutput s =
+  (case Scan.read Symbol.stopper csdpoutput (raw_explode s) of
+    SOME x => x
+  | NONE => error ("Failed to parse CSDP output: " ^ quote s))
 
 (* 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    *)