# HG changeset patch
# User wenzelm
# Date 1380406505 -7200
# Node ID 22ee3fb9d596fee3569915cfe59fcee4eca473a3
# Parent  61250526325725ef5b25c65e342ae01638fae6c0
backout c6297fa1031a -- strange parsers are required to make this work;

diff -r 612505263257 -r 22ee3fb9d596 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Sep 28 22:47:17 2013 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sun Sep 29 00:15:05 2013 +0200
@@ -275,9 +275,11 @@
    end
  end;
 
+
 fun isnum x = member (op =) ["0","1","2","3","4","5","6","7","8","9"] x;
 
-(* More parser basics.                                                       *)
+(* More parser basics. *)
+(* FIXME improper use of parser combinators ahead *)
 
  val numeral = Scan.one isnum
  val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
@@ -298,17 +300,20 @@
  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.                                                      *)
+(* FIXME improper use of parser combinators ahead *)
 
  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
-
- 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))
+ 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    *)