src/Tools/WWW_Find/scgi_req.ML
changeset 41491 a2ad5b824051
parent 40152 51e026049e4d
child 43703 c37a1f29bbc0
equal deleted inserted replaced
41490:0f1e411a1448 41491:a2ad5b824051
    78 fun split_fields vec =
    78 fun split_fields vec =
    79   let
    79   let
    80     val nulls = ~1 :: (Word8Vector.foldri find_nulls [] vec);
    80     val nulls = ~1 :: (Word8Vector.foldri find_nulls [] vec);
    81 
    81 
    82     fun pr NONE = "NONE"
    82     fun pr NONE = "NONE"
    83       | pr (SOME i) = "SOME " ^ Int.toString i;
    83       | pr (SOME i) = "SOME " ^ string_of_int i;
    84 
    84 
    85     fun hd_diff (i1::i2::_) = SOME (i2 - i1 - 1)
    85     fun hd_diff (i1::i2::_) = SOME (i2 - i1 - 1)
    86       | hd_diff _ = NONE;
    86       | hd_diff _ = NONE;
    87 
    87 
    88     fun slice [] = []
    88     fun slice [] = []