src/Pure/General/symbol.scala
changeset 47121 fb5764df8a9c
parent 46997 395b7277ed76
child 47993 135fd6f2dadd
equal deleted inserted replaced
47120:500a5d97511a 47121:fb5764df8a9c
   345       "\\<Psi>", "\\<Omega>",
   345       "\\<Psi>", "\\<Omega>",
   346 
   346 
   347       "\\<^isub>", "\\<^isup>")
   347       "\\<^isub>", "\\<^isup>")
   348 
   348 
   349     val blanks =
   349     val blanks =
   350       recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
   350       recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<spacespace>", "\\<^newline>")
   351 
   351 
   352     val sym_chars =
   352     val sym_chars =
   353       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
   353       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
   354 
   354 
   355     val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*)
   355     val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*)