src/Pure/library.scala
changeset 73602 ec52a1a6ed31
parent 73594 f5c147654661
child 73604 31d4274f32de
equal deleted inserted replaced
73601:79b120d1c1a3 73602:ec52a1a6ed31
   146   def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s
   146   def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s
   147 
   147 
   148   def isolate_substring(s: String): String = new String(s.toCharArray)
   148   def isolate_substring(s: String): String = new String(s.toCharArray)
   149 
   149 
   150   def strip_ansi_color(s: String): String =
   150   def strip_ansi_color(s: String): String =
   151     s.replaceAll("""\u001b\[\d+m""", "")
   151     s.replaceAll("\u001b\\[\\d+m", "")
   152 
   152 
   153 
   153 
   154   /* quote */
   154   /* quote */
   155 
   155 
   156   def single_quote(s: String): String = "'" + s + "'"
   156   def single_quote(s: String): String = "'" + s + "'"