From c71eebde8ca96a9660cfd3d26d685b985e0b387a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Dec 2020 18:07:28 -0800
Subject: [PATCH] chore: remove `util/buffer.h` dependency from `runtime`

---
 src/include/lean/utf8.h  | 4 ++--
 src/kernel/inductive.cpp | 2 +-
 src/runtime/object.cpp   | 2 +-
 src/runtime/utf8.cpp     | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/include/lean/utf8.h b/src/include/lean/utf8.h
index 798c444b32..e92cc47c7c 100644
--- a/src/include/lean/utf8.h
+++ b/src/include/lean/utf8.h
@@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <vector>
 #include <string>
 #include <lean/optional.h>
-#include "util/buffer.h"
 
 namespace lean {
 using uchar = unsigned char;
@@ -42,7 +42,7 @@ unsigned next_utf8(std::string const & str, size_t & i);
 unsigned next_utf8(char const * str, size_t size, size_t & i);
 
 /* Decode a UTF-8 encoded string `str` into unicode scalar values */
-void utf8_decode(std::string const & str, buffer<unsigned> & out);
+void utf8_decode(std::string const & str, std::vector<unsigned> & out);
 
 /* Push a unicode scalar value into a utf-8 encoded string */
 void push_unicode_scalar(std::string & s, unsigned code);
diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp
index 1128d4c036..d4daf5cc27 100644
--- a/src/kernel/inductive.cpp
+++ b/src/kernel/inductive.cpp
@@ -1129,7 +1129,7 @@ expr nat_lit_to_constructor(expr const & e) {
 expr string_lit_to_constructor(expr const & e) {
     lean_assert(is_string_lit(e));
     string_ref const & s = lit_value(e).get_string();
-    buffer<unsigned> cs;
+    std::vector<unsigned> cs;
     utf8_decode(s.to_std_string(), cs);
     expr r = *g_list_nil_char;
     unsigned i = cs.size();
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index ac41324d28..4d542deeb7 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -1614,7 +1614,7 @@ static std::string list_as_string(b_obj_arg lst) {
 }
 
 static obj_res string_to_list_core(std::string const & s, bool reverse = false) {
-    buffer<unsigned> tmp;
+    std::vector<unsigned> tmp;
     utf8_decode(s, tmp);
     if (reverse)
         std::reverse(tmp.begin(), tmp.end());
diff --git a/src/runtime/utf8.cpp b/src/runtime/utf8.cpp
index 9862ad76d8..0d4c89ec63 100644
--- a/src/runtime/utf8.cpp
+++ b/src/runtime/utf8.cpp
@@ -205,7 +205,7 @@ unsigned next_utf8(std::string const & str, size_t & i) {
     return next_utf8(str.data(), str.size(), i);
 }
 
-void utf8_decode(std::string const & str, buffer<unsigned> & out) {
+void utf8_decode(std::string const & str, std::vector<unsigned> & out) {
     size_t i = 0;
     while (i < str.size()) {
         out.push_back(next_utf8(str, i));