clarified completion of Isabelle symbols within document source;
authorwenzelm
Mon Nov 02 10:20:27 2015 +0100 (2015-11-02)
changeset 61537f6bd97a587b7
parent 61536 346aa2c5447f
child 61538 bf4969660913
clarified completion of Isabelle symbols within document source;
NEWS
etc/options
src/Pure/PIDE/markup.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Mon Nov 02 09:43:20 2015 +0100
     1.2 +++ b/NEWS	Mon Nov 02 10:20:27 2015 +0100
     1.3 @@ -79,6 +79,9 @@
     1.4  standard Isabelle fonts provide glyphs to render important control
     1.5  symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
     1.6  
     1.7 +* System option "document_symbols" determines completion of Isabelle
     1.8 +symbols within document source.
     1.9 +
    1.10  * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
    1.11  Consequently, \<open>...\<close> without any decoration prints literal quasi-formal
    1.12  text. Command-line tool "isabelle update_cartouches -t" helps to update
     2.1 --- a/etc/options	Mon Nov 02 09:43:20 2015 +0100
     2.2 +++ b/etc/options	Mon Nov 02 10:20:27 2015 +0100
     2.3 @@ -164,3 +164,5 @@
     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/PIDE/markup.ML	Mon Nov 02 09:43:20 2015 +0100
     3.2 +++ b/src/Pure/PIDE/markup.ML	Mon Nov 02 10:20:27 2015 +0100
     3.3 @@ -36,7 +36,7 @@
     3.4    val language_prop: bool -> T
     3.5    val language_ML: bool -> T
     3.6    val language_SML: bool -> T
     3.7 -  val language_document: bool -> T
     3.8 +  val language_document: {symbols: bool, delimited: bool} -> T
     3.9    val language_antiquotation: T
    3.10    val language_text: bool -> T
    3.11    val language_rail: T
    3.12 @@ -310,7 +310,8 @@
    3.13  val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
    3.14  val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
    3.15  val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
    3.16 -val language_document = language' {name = "document", symbols = false, antiquotes = true};
    3.17 +fun language_document {symbols, delimited} =
    3.18 +  language' {name = "document", symbols = symbols, antiquotes = true} delimited;
    3.19  val language_antiquotation =
    3.20    language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
    3.21  val language_text = language' {name = "text", symbols = true, antiquotes = false};
     4.1 --- a/src/Pure/Thy/thy_output.ML	Mon Nov 02 09:43:20 2015 +0100
     4.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Nov 02 10:20:27 2015 +0100
     4.3 @@ -196,7 +196,10 @@
     4.4  fun output_text state {markdown} source =
     4.5    let
     4.6      val pos = Input.pos_of source;
     4.7 -    val _ = Position.report pos (Markup.language_document (Input.is_delimited source));
     4.8 +    val _ =
     4.9 +      Position.report pos
    4.10 +        (Markup.language_document
    4.11 +          {symbols = Options.default_bool "document_symbols", delimited = Input.is_delimited source});
    4.12      val syms = Input.source_explode source;
    4.13  
    4.14      val output_antiquote = eval_antiquote state #> Symbol.explode #> Latex.output_ctrl_symbols;