equal
deleted
inserted
replaced
34 case '\\' => "\\\\" |
34 case '\\' => "\\\\" |
35 case _ => c.toString |
35 case _ => c.toString |
36 } |
36 } |
37 |
37 |
38 def string(s: String): Source = |
38 def string(s: String): Source = |
39 "'" + s.map(escape_char(_)).mkString + "'" |
39 s.iterator.map(escape_char(_)).mkString("'", "", "'") |
40 |
40 |
41 def ident(s: String): Source = |
41 def ident(s: String): Source = |
42 Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\"")))) |
42 Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\"")))) |
43 |
43 |
44 def enclose(s: Source): Source = "(" + s + ")" |
44 def enclose(s: Source): Source = "(" + s + ")" |