[ base ] Add getTermCols and getTermLines to base library and fix pri… (

#3009)

CHANGELOG.md

@@ -169,6 +169,9 @@
 
 * Adds `leftmost` and `rightmost` to `Control.Order`, a generalisation of `min` and `max`.
 
+* Adds `getTermCols` and `getTermLines` to the base library. They return the size of the
+  terminal if either stdin or stdout is a tty.
+
 #### System
 
 * Changes `getNProcessors` to return the number of online processors rather than

libs/base/System/Term.idr

@@ -0,0 +1,27 @@
+module System.Term
+
+%default total
+
+libterm : String -> String
+libterm s = "C:" ++ s ++ ", libidris2_support, idris_term.h"
+
+%foreign libterm "idris2_setupTerm"
+prim__setupTerm : PrimIO ()
+
+%foreign libterm "idris2_getTermCols"
+prim__getTermCols : PrimIO Int
+
+%foreign libterm "idris2_getTermLines"
+prim__getTermLines : PrimIO Int
+
+export
+setupTerm : IO ()
+setupTerm = primIO prim__setupTerm
+
+export
+getTermCols : IO Int
+getTermCols = primIO prim__getTermCols
+
+export
+getTermLines : IO Int
+getTermLines = primIO prim__getTermLines

libs/base/base.ipkg

@@ -127,4 +127,5 @@ modules = Control.App,
           System.File.Virtual,
           System.Info,
           System.REPL,
-          System.Signal
+          System.Signal,
+          System.Term

src/Libraries/Utils/Term.idr

@@ -2,6 +2,8 @@ module Libraries.Utils.Term
 
 %default total
 
+-- TODO: remove this file and use System.Term after version following 0.6.0 is released
+
 libterm : String -> String
 libterm s = "C:" ++ s ++ ", libidris2_support, idris_term.h"
 

support/c/idris_term.c

@@ -36,13 +36,23 @@ void idris2_setupTerm() {
 
 int idris2_getTermCols() {
   struct winsize ts;
-  ioctl(0, TIOCGWINSZ, &ts);
+  int err = ioctl(0, TIOCGWINSZ, &ts);
+  if (err) {
+    err = ioctl(1, TIOCGWINSZ, &ts);
+  }
+  if (err)
+    return 0;
   return (int)ts.ws_col;
 }
 
 int idris2_getTermLines() {
   struct winsize ts;
-  ioctl(0, TIOCGWINSZ, &ts);
+  int err = ioctl(0, TIOCGWINSZ, &ts);
+  if (err) {
+    err = ioctl(1, TIOCGWINSZ, &ts);
+  }
+  if (err)
+    return 0;
   return (int)ts.ws_row;
 }
 

tests/Main.idr

@@ -204,7 +204,7 @@ idrisTestsAllSchemes : Requirement -> TestPool
 idrisTestsAllSchemes cg = MkTestPool
       ("Test across all scheme backends: " ++ show cg ++ " instance")
       [] (Just cg)
-      [ "scheme001"
+      [ "scheme001", "scheme002"
       , "channels001", "channels002", "channels003", "channels004", "channels005"
       , "channels006"
       ]

tests/allschemes/scheme002/TermSize.idr

@@ -0,0 +1,7 @@
+import System.Term
+
+main : IO ()
+main = do
+  width <- getTermCols
+  height <- getTermLines
+  printLn "Success \{show $ width > 0} \{show $ height > 0}"

tests/allschemes/scheme002/expected

@@ -0,0 +1 @@
+"Success False False"

tests/allschemes/scheme002/run

@@ -0,0 +1,13 @@
+rm -rf build
+
+# observe that errors are correctly reported as zero.
+$1 --exec main TermSize.idr </dev/null
+
+# The following should report True True, but the ci scripts don't
+# provide a terminal
+# $1 --exec main TermSize.idr
+
+# The following should also report True True if the output is a terminal,
+# but the testing framework redirects output.
+
+# idris2 --exec main tests/allschemes/scheme002/TermSize.idr </dev/null