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"