diff -r 59eff6e56d81 -r 0f39f59317c1 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Wed Jul 20 11:44:11 2016 +0200 +++ b/src/Pure/General/symbol.scala Wed Jul 20 16:02:00 2016 +0200 @@ -458,8 +458,9 @@ val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*) - /* comment */ + /* misc symbols */ + val newline_decoded = decode(newline) val comment_decoded = decode(comment) @@ -526,7 +527,15 @@ def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym) - /* comment */ + /* misc symbols */ + + val newline: Symbol = "\\" + def newline_decoded: Symbol = symbols.newline_decoded + + def print_newlines(str: String): String = + if (str.contains('\n')) + (for (s <- iterator(str)) yield { if (s == "\n") newline_decoded else s }).mkString + else str val comment: Symbol = "\\" def comment_decoded: Symbol = symbols.comment_decoded