# HG changeset patch
# User wenzelm
# Date 1398202305 -7200
# Node ID ef623f6f036bc41761ba4d7a96ac6a88a3eab7a1
# Parent  5d629da46f04ce444649219d0a142785d92e5fa1
avoid octal escape literals -- deprecated in scala-2.11.0;

diff -r 5d629da46f04 -r ef623f6f036b src/Pure/General/completion.scala
--- 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(
diff -r 5d629da46f04 -r ef623f6f036b src/Pure/PIDE/yxml.scala
--- 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
diff -r 5d629da46f04 -r ef623f6f036b src/Pure/System/isabelle_system.scala
--- 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))
diff -r 5d629da46f04 -r ef623f6f036b src/Pure/Tools/main.scala
--- 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)