always complete explicit symbols;
authorwenzelm
Mon Jul 21 14:24:10 2014 +0200 (2014-07-21)
changeset 57589e0e4ac981cf1
parent 57588 ff31aad27661
child 57590 06cb5375e189
always complete explicit symbols;
src/Doc/JEdit/JEdit.thy
src/Pure/General/completion.scala
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Mon Jul 21 13:50:26 2014 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Mon Jul 21 14:24:10 2014 +0200
     1.3 @@ -1225,6 +1225,12 @@
     1.4    situations, to tell that some language keywords should be excluded from
     1.5    further completion attempts. For example, @{verbatim ":"} within accepted
     1.6    Isar syntax looses its meaning as abbreviation for symbol @{text "\<in>"}.
     1.7 +
     1.8 +  \medskip The completion context is \emph{ignored} for built-in templates and
     1.9 +  symbols in their explicit form ``@{verbatim "\<foobar>"}''; see also
    1.10 +  \secref{sec:completion-varieties}. This allows to complete within broken
    1.11 +  input that escapes its normal semantic context, e.g.\ antiquotations or
    1.12 +  string literals in ML, which do not allow arbitrary backslash sequences.
    1.13  *}
    1.14  
    1.15  
     2.1 --- a/src/Pure/General/completion.scala	Mon Jul 21 13:50:26 2014 +0200
     2.2 +++ b/src/Pure/General/completion.scala	Mon Jul 21 14:24:10 2014 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4  
     2.5  import scala.collection.immutable.SortedMap
     2.6  import scala.util.parsing.combinator.RegexParsers
     2.7 +import scala.util.matching.Regex
     2.8  import scala.math.Ordering
     2.9  
    2.10  
    2.11 @@ -219,6 +220,9 @@
    2.12    {
    2.13      override val whiteSpace = "".r
    2.14  
    2.15 +    private val symbol_regex: Regex = """\\<\^?[A-Za-z0-9_']+>""".r
    2.16 +    def is_symbol(s: CharSequence): Boolean = symbol_regex.pattern.matcher(s).matches
    2.17 +
    2.18      private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
    2.19      private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
    2.20      private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
    2.21 @@ -347,7 +351,10 @@
    2.22              case (a, _) :: _ =>
    2.23                val ok =
    2.24                  if (a == Completion.antiquote) language_context.antiquotes
    2.25 -                else language_context.symbols || Completion.default_abbrs.exists(_._1 == a)
    2.26 +                else
    2.27 +                  language_context.symbols ||
    2.28 +                  Completion.default_abbrs.exists(_._1 == a) ||
    2.29 +                  Completion.Word_Parsers.is_symbol(a)
    2.30                if (ok) Some((a, abbrevs))
    2.31                else None
    2.32            }