# HG changeset patch
# User wenzelm
# Date 1464095817 -7200
# Node ID 035785035a1a63a2c31ac3755e27328e4ff63320
# Parent  284e1802bc5c8bceabfe7fe0b1e4b7bf9ee4e834
cartouche abbreviations work both for " as well;

diff -r 284e1802bc5c -r 035785035a1a NEWS
--- a/NEWS	Tue May 24 11:39:26 2016 +0200
+++ b/NEWS	Tue May 24 15:16:57 2016 +0200
@@ -38,6 +38,9 @@
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
+* Cartouche abbreviations work both for " and ` to accomodate typical
+situations where old ASCII notation may be updated.
+
 * IDE support for the Isabelle/Pure bootstrap process, with the
 following independent stages:
 
diff -r 284e1802bc5c -r 035785035a1a src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Tue May 24 11:39:26 2016 +0200
+++ b/src/Pure/General/completion.scala	Tue May 24 15:16:57 2016 +0200
@@ -334,7 +334,10 @@
     List("@{" -> "@{\u0007}",
       "`" -> "\\<close>",
       "`" -> "\\<open>",
-      "`" -> "\\<open>\u0007\\<close>")
+      "`" -> "\\<open>\u0007\\<close>",
+      "\"" -> "\\<close>",
+      "\"" -> "\\<open>",
+      "\"" -> "\\<open>\u0007\\<close>")
 
   private def default_frequency(name: String): Option[Int] =
     default_abbrs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2)