chore: address review comments

src/Init/System/IO.lean

@@ -311,7 +311,8 @@ Note that EOF does not actually close a stream, so further reads may block and r
   -/
   getLine : IO String
   putStr  : String → IO Unit
-  isatty  : BaseIO Bool
+  /-- Returns true if a stream refers to a Windows console or Unix terminal. -/
+  isTty   : BaseIO Bool
   deriving Inhabited
 
 open FS
@@ -362,7 +363,7 @@ Will succeed even if no lock has been acquired.
 @[extern "lean_io_prim_handle_unlock"] opaque unlock (h : @& Handle) : IO Unit
 
 /-- Returns true if a handle refers to a Windows console or Unix terminal. -/
-@[extern "lean_io_prim_handle_isatty"] opaque isatty (h : @& Handle) : BaseIO Bool
+@[extern "lean_io_prim_handle_is_tty"] opaque isTty (h : @& Handle) : BaseIO Bool
 
 @[extern "lean_io_prim_handle_flush"] opaque flush (h : @& Handle) : IO Unit
 /-- Rewinds the read/write cursor to the beginning of the handle. -/
@@ -753,7 +754,7 @@ def ofHandle (h : Handle) : Stream where
   write   := Handle.write h
   getLine := Handle.getLine h
   putStr  := Handle.putStr h
-  isatty  := Handle.isatty h
+  isTty   := Handle.isTty h
 
 structure Buffer where
   data : ByteArray := ByteArray.empty
@@ -776,7 +777,7 @@ def ofBuffer (r : Ref Buffer) : Stream where
   putStr  := fun s => r.modify fun b =>
     let data := s.toUTF8
     { b with data := data.copySlice 0 b.data b.pos data.size false, pos := b.pos + data.size }
-  isatty  := pure false
+  isTty   := pure false
 
 end Stream
 

src/runtime/io.cpp

@@ -302,14 +302,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_mk(b_obj_arg filename, uint8
 #ifdef LEAN_WINDOWS
 
 static inline HANDLE win_handle(FILE * fp) {
-// Windows CE requires a different approach.
-// We may be able to ignore this, as we may not otherwise support WinCE?
-// https://stackoverflow.com/a/3989842
-#ifdef q4_WCE
-    return (HANDLE)_fileno(fp);
-#else
     return (HANDLE)_get_osfhandle(_fileno(fp));
-#endif
 }
 
 /* Handle.lock : (@& Handle) → (exclusive : Bool) → IO Unit */
@@ -394,14 +387,14 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_unlock(b_obj_arg h, obj_arg /
 
 #endif
 
-/* Handle.isatty : (@& Handle) → BaseIO Bool */
-extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_isatty(b_obj_arg h, obj_arg /* w */) {
+/* Handle.isTty : (@& Handle) → BaseIO Bool */
+extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_is_tty(b_obj_arg h, obj_arg /* w */) {
     FILE * fp = io_get_handle(h);
 #ifdef LEAN_WINDOWS
     /*
     On Windows, there are two approaches for detecting a console.
     1)  _isatty(_fileno(fp)) != 0
-        This checks whether the the file descriptor is is a *character device*,
+        This checks whether the file descriptor is a *character device*,
         not just a terminal (unlike Unix's isatty). Thus, it produces a false
         positive in some edge cases (such as NUL).
         https://stackoverflow.com/q/3648711
@@ -411,7 +404,8 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_isatty(b_obj_arg h, obj_arg /
         which is not implemented as a Windows-recognized console on
         old Windows versions (e.g., pre-Windows 10, pre-ConPTY).
         https://github.com/msys2/MINGW-packages/issues/14087
-    We choose to use GetConsoleMode as that seems like the more modern approach.
+    We choose to use GetConsoleMode as that seems like the more modern approach,
+    and Lean does not support pre-Windows 10.
     */
     DWORD mode;
     return io_result_mk_ok(box(GetConsoleMode(win_handle(fp), &mode) != 0));