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