--- a/src/Pure/General/completion.scala Tue Apr 22 23:01:59 2014 +0200
+++ b/src/Pure/General/completion.scala Tue Apr 22 23:31:45 2014 +0200
@@ -266,10 +266,10 @@
/* abbreviations */
- private val caret_indicator = '\007'
+ private val caret_indicator = '\u0007'
private val antiquote = "@{"
private val default_abbrs =
- List("@{" -> "@{\007}", "`" -> "\\<open>\007\\<close>", "`" -> "\\<open>", "`" -> "\\<close>")
+ List("@{" -> "@{\u0007}", "`" -> "\\<open>\u0007\\<close>", "`" -> "\\<open>", "`" -> "\\<close>")
}
final class Completion private(
--- a/src/Pure/PIDE/yxml.scala Tue Apr 22 23:01:59 2014 +0200
+++ b/src/Pure/PIDE/yxml.scala Tue Apr 22 23:31:45 2014 +0200
@@ -16,8 +16,8 @@
{
/* chunk markers */
- val X = '\5'
- val Y = '\6'
+ val X = '\u0005'
+ val Y = '\u0006'
val is_X = (c: Char) => c == X
val is_Y = (c: Char) => c == Y
--- a/src/Pure/System/isabelle_system.scala Tue Apr 22 23:01:59 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala Tue Apr 22 23:31:45 2014 +0200
@@ -107,7 +107,7 @@
if (rc != 0) error(output)
val entries =
- (for (entry <- File.read(dump) split "\0" if entry != "") yield {
+ (for (entry <- File.read(dump) split "\u0000" if entry != "") yield {
val i = entry.indexOf('=')
if (i <= 0) (entry -> "")
else (entry.substring(0, i) -> entry.substring(i + 1))
--- a/src/Pure/Tools/main.scala Tue Apr 22 23:01:59 2014 +0200
+++ b/src/Pure/Tools/main.scala Tue Apr 22 23:31:45 2014 +0200
@@ -195,7 +195,7 @@
val path = (new JFile(isabelle_home, link)).toPath
val writer = Files.newBufferedWriter(path, UTF8.charset)
- try { writer.write("!<symlink>" + content + "\0") }
+ try { writer.write("!<symlink>" + content + "\u0000") }
finally { writer.close }
Files.setAttribute(path, "dos:system", true)