--- a/src/Doc/JEdit/JEdit.thy Mon Jul 21 13:50:26 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy Mon Jul 21 14:24:10 2014 +0200
@@ -1225,6 +1225,12 @@
situations, to tell that some language keywords should be excluded from
further completion attempts. For example, @{verbatim ":"} within accepted
Isar syntax looses its meaning as abbreviation for symbol @{text "\<in>"}.
+
+ \medskip The completion context is \emph{ignored} for built-in templates and
+ symbols in their explicit form ``@{verbatim "\<foobar>"}''; see also
+ \secref{sec:completion-varieties}. This allows to complete within broken
+ input that escapes its normal semantic context, e.g.\ antiquotations or
+ string literals in ML, which do not allow arbitrary backslash sequences.
*}
--- a/src/Pure/General/completion.scala Mon Jul 21 13:50:26 2014 +0200
+++ b/src/Pure/General/completion.scala Mon Jul 21 14:24:10 2014 +0200
@@ -11,6 +11,7 @@
import scala.collection.immutable.SortedMap
import scala.util.parsing.combinator.RegexParsers
+import scala.util.matching.Regex
import scala.math.Ordering
@@ -219,6 +220,9 @@
{
override val whiteSpace = "".r
+ private val symbol_regex: Regex = """\\<\^?[A-Za-z0-9_']+>""".r
+ def is_symbol(s: CharSequence): Boolean = symbol_regex.pattern.matcher(s).matches
+
private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
@@ -347,7 +351,10 @@
case (a, _) :: _ =>
val ok =
if (a == Completion.antiquote) language_context.antiquotes
- else language_context.symbols || Completion.default_abbrs.exists(_._1 == a)
+ else
+ language_context.symbols ||
+ Completion.default_abbrs.exists(_._1 == a) ||
+ Completion.Word_Parsers.is_symbol(a)
if (ok) Some((a, abbrevs))
else None
}