# HG changeset patch
# User wenzelm
# Date 1446908728 -3600
# Node ID 1ca11ddfcc702b37f481f7e407a03349941d3fca
# Parent  2e52df0cd8eea4591eeb87295394123522a7a70a
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);

diff -r 2e52df0cd8ee -r 1ca11ddfcc70 NEWS
--- a/NEWS	Sat Nov 07 15:23:26 2015 +0100
+++ b/NEWS	Sat Nov 07 16:05:28 2015 +0100
@@ -29,6 +29,10 @@
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
+* Completion of symbols via prefix of \<name> or \<^name> or \name is
+always possible, independently of the language context. It is never
+implicit: a popup will show up unconditionally.
+
 * Improved scheduling for urgent print tasks (e.g. command state output,
 interactive queries) wrt. long-running background tasks.
 
@@ -88,9 +92,6 @@
 corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using
 standard LaTeX macros of the same names.
 
-* System option "document_symbols" determines completion of Isabelle
-symbols within document source.
-
 * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
 Consequently, \<open>...\<close> without any decoration prints literal quasi-formal
 text. Command-line tool "isabelle update_cartouches -t" helps to update
diff -r 2e52df0cd8ee -r 1ca11ddfcc70 etc/options
--- a/etc/options	Sat Nov 07 15:23:26 2015 +0100
+++ b/etc/options	Sat Nov 07 16:05:28 2015 +0100
@@ -164,5 +164,3 @@
 public option completion_limit : int = 40
   -- "limit for completion within the formal context"
 
-public option document_symbols : bool = false
-  -- "completion of Isabelle symbols within document source"
diff -r 2e52df0cd8ee -r 1ca11ddfcc70 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Sat Nov 07 15:23:26 2015 +0100
+++ b/src/Pure/General/completion.scala	Sat Nov 07 16:05:28 2015 +0100
@@ -246,8 +246,8 @@
   {
     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 val symboloid_regex: Regex = """\\([A-Za-z0-9_']+|<\^?[A-Za-z0-9_']+>)""".r
+    def is_symboloid(s: CharSequence): Boolean = symboloid_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
@@ -401,10 +401,7 @@
             case (abbr, _) :: _ =>
               val ok =
                 if (abbr == Completion.antiquote) language_context.antiquotes
-                else
-                  language_context.symbols ||
-                  Completion.default_abbrs.exists(_._1 == abbr) ||
-                  Completion.Word_Parsers.is_symbol(abbr)
+                else language_context.symbols || Completion.default_abbrs.exists(_._1 == abbr)
               if (ok) Some((abbr, abbrevs))
               else None
           }
@@ -434,7 +431,7 @@
                     complete_word <- complete_words
                     ok =
                       if (is_keyword(complete_word)) !word_context && language_context.is_outer
-                      else language_context.symbols
+                      else language_context.symbols || Completion.Word_Parsers.is_symboloid(word)
                     if ok
                     completion <- words_map.get_list(complete_word)
                   } yield (complete_word, completion)
@@ -448,6 +445,7 @@
         val immediate =
           explicit ||
             (!Completion.Word_Parsers.is_word(original) &&
+             !Completion.Word_Parsers.is_symboloid(original) &&
               Character.codePointCount(original, 0, original.length) > 1)
         val unique = completions.length == 1
 
diff -r 2e52df0cd8ee -r 1ca11ddfcc70 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Nov 07 15:23:26 2015 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Nov 07 16:05:28 2015 +0100
@@ -36,7 +36,7 @@
   val language_prop: bool -> T
   val language_ML: bool -> T
   val language_SML: bool -> T
-  val language_document: {symbols: bool, delimited: bool} -> T
+  val language_document: bool -> T
   val language_antiquotation: T
   val language_text: bool -> T
   val language_rail: T
@@ -309,8 +309,7 @@
 val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
 val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
 val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
-fun language_document {symbols, delimited} =
-  language' {name = "document", symbols = symbols, antiquotes = true} delimited;
+val language_document = language' {name = "document", symbols = false, antiquotes = true};
 val language_antiquotation =
   language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
 val language_text = language' {name = "text", symbols = true, antiquotes = false};
diff -r 2e52df0cd8ee -r 1ca11ddfcc70 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat Nov 07 15:23:26 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sat Nov 07 16:05:28 2015 +0100
@@ -196,10 +196,7 @@
 fun output_text state {markdown} source =
   let
     val pos = Input.pos_of source;
-    val _ =
-      Position.report pos
-        (Markup.language_document
-          {symbols = Options.default_bool "document_symbols", delimited = Input.is_delimited source});
+    val _ = Position.report pos (Markup.language_document (Input.is_delimited source));
     val syms = Input.source_explode source;
 
     val output_antiquotes = map (eval_antiquote state) #> implode;