diff -r e95ea6956df3 -r bfc120aa737a src/Pure/library.scala
--- a/src/Pure/library.scala	Fri May 22 13:53:19 2020 +0200
+++ b/src/Pure/library.scala	Fri May 22 15:53:47 2020 +0200
@@ -144,6 +144,9 @@
 
   def isolate_substring(s: String): String = new String(s.toCharArray)
 
+  def strip_ansi_color(s: String): String =
+    s.replaceAll("""\u001b\[\d+m""", "")
+
 
   /* quote */