--- 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
--- 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
--- 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
}