src/Pure/General/symbol.scala
changeset 63528 0f39f59317c1
parent 62528 c8c532b22947
child 63936 b87784e19a77
--- 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 = "\\<newline>"
+  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 = "\\<comment>"
   def comment_decoded: Symbol = symbols.comment_decoded