Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cartouche abbreviations work both for " as well;
authorwenzelm
Tue, 24 May 2016 15:16:57 +0200
changeset 63135 035785035a1a
parent 63121 284e1802bc5c
child 63136 fd11a538daac
cartouche abbreviations work both for " as well;
NEWS file | annotate | diff | comparison | revisions
src/Pure/General/completion.scala file | annotate | diff | comparison | revisions 
--- 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:
 
--- 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)
isabelle