--- 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 *)