# HG changeset patch
# User wenzelm
# Date 1446456027 -3600
# Node ID f6bd97a587b7260805ad204623af0a1f18764eda
# Parent  346aa2c5447f8cbdba1014de5e31cdd052d5b68a
clarified completion of Isabelle symbols within document source;

diff -r 346aa2c5447f -r f6bd97a587b7 NEWS
--- a/NEWS	Mon Nov 02 09:43:20 2015 +0100
+++ b/NEWS	Mon Nov 02 10:20:27 2015 +0100
@@ -79,6 +79,9 @@
 standard Isabelle fonts provide glyphs to render important control
 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
 
+* 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 346aa2c5447f -r f6bd97a587b7 etc/options
--- a/etc/options	Mon Nov 02 09:43:20 2015 +0100
+++ b/etc/options	Mon Nov 02 10:20:27 2015 +0100
@@ -164,3 +164,5 @@
 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 346aa2c5447f -r f6bd97a587b7 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Nov 02 09:43:20 2015 +0100
+++ b/src/Pure/PIDE/markup.ML	Mon Nov 02 10:20:27 2015 +0100
@@ -36,7 +36,7 @@
   val language_prop: bool -> T
   val language_ML: bool -> T
   val language_SML: bool -> T
-  val language_document: bool -> T
+  val language_document: {symbols: bool, delimited: bool} -> T
   val language_antiquotation: T
   val language_text: bool -> T
   val language_rail: T
@@ -310,7 +310,8 @@
 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};
-val language_document = language' {name = "document", symbols = false, antiquotes = true};
+fun language_document {symbols, delimited} =
+  language' {name = "document", symbols = symbols, antiquotes = true} delimited;
 val language_antiquotation =
   language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
 val language_text = language' {name = "text", symbols = true, antiquotes = false};
diff -r 346aa2c5447f -r f6bd97a587b7 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Nov 02 09:43:20 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Nov 02 10:20:27 2015 +0100
@@ -196,7 +196,10 @@
 fun output_text state {markdown} source =
   let
     val pos = Input.pos_of source;
-    val _ = Position.report pos (Markup.language_document (Input.is_delimited source));
+    val _ =
+      Position.report pos
+        (Markup.language_document
+          {symbols = Options.default_bool "document_symbols", delimited = Input.is_delimited source});
     val syms = Input.source_explode source;
 
     val output_antiquote = eval_antiquote state #> Symbol.explode #> Latex.output_ctrl_symbols;