clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
authorwenzelm
Sat Nov 07 16:05:28 2015 +0100 (2015-11-07)
changeset 616001ca11ddfcc70
parent 61599 2e52df0cd8ee
child 61601 15952a05133c
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
NEWS
etc/options
src/Pure/General/completion.scala
src/Pure/PIDE/markup.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Sat Nov 07 15:23:26 2015 +0100
     1.2 +++ b/NEWS	Sat Nov 07 16:05:28 2015 +0100
     1.3 @@ -29,6 +29,10 @@
     1.4  
     1.5  *** Prover IDE -- Isabelle/Scala/jEdit ***
     1.6  
     1.7 +* Completion of symbols via prefix of \<name> or \<^name> or \name is
     1.8 +always possible, independently of the language context. It is never
     1.9 +implicit: a popup will show up unconditionally.
    1.10 +
    1.11  * Improved scheduling for urgent print tasks (e.g. command state output,
    1.12  interactive queries) wrt. long-running background tasks.
    1.13  
    1.14 @@ -88,9 +92,6 @@
    1.15  corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using
    1.16  standard LaTeX macros of the same names.
    1.17  
    1.18 -* System option "document_symbols" determines completion of Isabelle
    1.19 -symbols within document source.
    1.20 -
    1.21  * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
    1.22  Consequently, \<open>...\<close> without any decoration prints literal quasi-formal
    1.23  text. Command-line tool "isabelle update_cartouches -t" helps to update
     2.1 --- a/etc/options	Sat Nov 07 15:23:26 2015 +0100
     2.2 +++ b/etc/options	Sat Nov 07 16:05:28 2015 +0100
     2.3 @@ -164,5 +164,3 @@
     2.4  public option completion_limit : int = 40
     2.5    -- "limit for completion within the formal context"
     2.6  
     2.7 -public option document_symbols : bool = false
     2.8 -  -- "completion of Isabelle symbols within document source"
     3.1 --- a/src/Pure/General/completion.scala	Sat Nov 07 15:23:26 2015 +0100
     3.2 +++ b/src/Pure/General/completion.scala	Sat Nov 07 16:05:28 2015 +0100
     3.3 @@ -246,8 +246,8 @@
     3.4    {
     3.5      override val whiteSpace = "".r
     3.6  
     3.7 -    private val symbol_regex: Regex = """\\<\^?[A-Za-z0-9_']+>""".r
     3.8 -    def is_symbol(s: CharSequence): Boolean = symbol_regex.pattern.matcher(s).matches
     3.9 +    private val symboloid_regex: Regex = """\\([A-Za-z0-9_']+|<\^?[A-Za-z0-9_']+>)""".r
    3.10 +    def is_symboloid(s: CharSequence): Boolean = symboloid_regex.pattern.matcher(s).matches
    3.11  
    3.12      private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
    3.13      private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
    3.14 @@ -401,10 +401,7 @@
    3.15              case (abbr, _) :: _ =>
    3.16                val ok =
    3.17                  if (abbr == Completion.antiquote) language_context.antiquotes
    3.18 -                else
    3.19 -                  language_context.symbols ||
    3.20 -                  Completion.default_abbrs.exists(_._1 == abbr) ||
    3.21 -                  Completion.Word_Parsers.is_symbol(abbr)
    3.22 +                else language_context.symbols || Completion.default_abbrs.exists(_._1 == abbr)
    3.23                if (ok) Some((abbr, abbrevs))
    3.24                else None
    3.25            }
    3.26 @@ -434,7 +431,7 @@
    3.27                      complete_word <- complete_words
    3.28                      ok =
    3.29                        if (is_keyword(complete_word)) !word_context && language_context.is_outer
    3.30 -                      else language_context.symbols
    3.31 +                      else language_context.symbols || Completion.Word_Parsers.is_symboloid(word)
    3.32                      if ok
    3.33                      completion <- words_map.get_list(complete_word)
    3.34                    } yield (complete_word, completion)
    3.35 @@ -448,6 +445,7 @@
    3.36          val immediate =
    3.37            explicit ||
    3.38              (!Completion.Word_Parsers.is_word(original) &&
    3.39 +             !Completion.Word_Parsers.is_symboloid(original) &&
    3.40                Character.codePointCount(original, 0, original.length) > 1)
    3.41          val unique = completions.length == 1
    3.42  
     4.1 --- a/src/Pure/PIDE/markup.ML	Sat Nov 07 15:23:26 2015 +0100
     4.2 +++ b/src/Pure/PIDE/markup.ML	Sat Nov 07 16:05:28 2015 +0100
     4.3 @@ -36,7 +36,7 @@
     4.4    val language_prop: bool -> T
     4.5    val language_ML: bool -> T
     4.6    val language_SML: bool -> T
     4.7 -  val language_document: {symbols: bool, delimited: bool} -> T
     4.8 +  val language_document: bool -> T
     4.9    val language_antiquotation: T
    4.10    val language_text: bool -> T
    4.11    val language_rail: T
    4.12 @@ -309,8 +309,7 @@
    4.13  val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
    4.14  val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
    4.15  val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
    4.16 -fun language_document {symbols, delimited} =
    4.17 -  language' {name = "document", symbols = symbols, antiquotes = true} delimited;
    4.18 +val language_document = language' {name = "document", symbols = false, antiquotes = true};
    4.19  val language_antiquotation =
    4.20    language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
    4.21  val language_text = language' {name = "text", symbols = true, antiquotes = false};
     5.1 --- a/src/Pure/Thy/thy_output.ML	Sat Nov 07 15:23:26 2015 +0100
     5.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Nov 07 16:05:28 2015 +0100
     5.3 @@ -196,10 +196,7 @@
     5.4  fun output_text state {markdown} source =
     5.5    let
     5.6      val pos = Input.pos_of source;
     5.7 -    val _ =
     5.8 -      Position.report pos
     5.9 -        (Markup.language_document
    5.10 -          {symbols = Options.default_bool "document_symbols", delimited = Input.is_delimited source});
    5.11 +    val _ = Position.report pos (Markup.language_document (Input.is_delimited source));
    5.12      val syms = Input.source_explode source;
    5.13  
    5.14      val output_antiquotes = map (eval_antiquote state) #> implode;