# HG changeset patch
# User wenzelm
# Date 1405945450 -7200
# Node ID e0e4ac981cf1170278cd739b9125509c8ca30c33
# Parent  ff31aad27661f4c8a15b5be9e555c5d6e158b0fa
always complete explicit symbols;

diff -r ff31aad27661 -r e0e4ac981cf1 src/Doc/JEdit/JEdit.thy
--- 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.
 *}
 
 
diff -r ff31aad27661 -r e0e4ac981cf1 src/Pure/General/completion.scala
--- 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
           }