# HG changeset patch
# User wenzelm
# Date 1397581894 -7200
# Node ID 1a59587f46ec1e2e85591ab2aff693dfb90ec1d5
# Parent  d01d183e84eabfb7b43aadeee5c8282f94591d94
clarified abbreviations for cartouche delimiters, to work in any context;

diff -r d01d183e84ea -r 1a59587f46ec NEWS
--- a/NEWS	Tue Apr 15 16:44:06 2014 +0200
+++ b/NEWS	Tue Apr 15 19:11:34 2014 +0200
@@ -22,8 +22,7 @@
 
 * Lexical syntax (inner and outer) supports text cartouches with
 arbitrary nesting, and without escapes of quotes etc.  The Prover IDE
-supports input methods via ` (backquote), or << and >> (double angle
-brackets).
+supports input via ` (backquote).
 
 * The outer syntax categories "text" (for formal comments and document
 markup commands) and "altstring" (for literal fact references) allow
diff -r d01d183e84ea -r 1a59587f46ec etc/symbols
--- a/etc/symbols	Tue Apr 15 16:44:06 2014 +0200
+++ b/etc/symbols	Tue Apr 15 19:11:34 2014 +0200
@@ -348,8 +348,8 @@
 \<hungarumlaut>         code: 0x0002dd
 \<some>                 code: 0x0003f5
 \<newline>              code: 0x0023ce
-\<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
-\<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
+\<open>                 code: 0x002039  group: punctuation  font: IsabelleText
+\<close>                code: 0x00203a  group: punctuation  font: IsabelleText
 \<here>                 code: 0x002302  font: IsabelleText
 \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
 \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
diff -r d01d183e84ea -r 1a59587f46ec src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Tue Apr 15 16:44:06 2014 +0200
+++ b/src/Pure/General/completion.scala	Tue Apr 15 19:11:34 2014 +0200
@@ -267,7 +267,7 @@
   private val caret_indicator = '\007'
   private val antiquote = "@{"
   private val default_abbrs =
-    Map("@{" -> "@{\007}", "`" -> "\\<open>\007\\<close>")
+    List("@{" -> "@{\007}", "`" -> "\\<open>\007\\<close>", "`" -> "\\<open>", "`" -> "\\<close>")
 }
 
 final class Completion private(
@@ -309,7 +309,7 @@
         yield (y, x)).toList
 
     val abbrs =
-      for ((a, b) <- symbol_abbrs ::: Completion.default_abbrs.toList)
+      for ((a, b) <- symbol_abbrs ::: Completion.default_abbrs)
         yield (a.reverse, (a, b))
 
     new Completion(
@@ -347,7 +347,7 @@
             case (a, _) :: _ =>
               val ok =
                 if (a == Completion.antiquote) language_context.antiquotes
-                else language_context.symbols || Completion.default_abbrs.isDefinedAt(a)
+                else language_context.symbols || Completion.default_abbrs.exists(_._1 == a)
               if (ok) Some(((a, abbrevs), caret))
               else None
           }