# HG changeset patch
# User wenzelm
# Date 1678535317 -3600
# Node ID 606ac3fae270592d6287a120d07ed2b4d0396aaf
# Parent  3b09ae9e40cba1b45fcbc0e1b153e3392f56ecba
clarified tags;

diff -r 3b09ae9e40cb -r 606ac3fae270 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Sat Mar 11 12:41:53 2023 +0100
+++ b/src/Pure/System/options.scala	Sat Mar 11 12:48:37 2023 +0100
@@ -43,11 +43,11 @@
   case object String extends Type
   case object Unknown extends Type
 
-  val TAG_CONTENT = "content"
-  val TAG_DOCUMENT = "document"
-  val TAG_BUILD = "build"
-  val TAG_UPDATE = "update"
-  val TAG_CONNECTION = "connection"
+  val TAG_CONTENT = "content"    // formal theory content
+  val TAG_DOCUMENT = "document"  // document preparation
+  val TAG_BUILD = "build"        // relavant for "isabelle build"
+  val TAG_UPDATE = "update"      // relevant for "isabelle update"
+  val TAG_CONNECTION = "connection"  // private information about connections (password etc.)
 
   case class Entry(
     public: Boolean,
@@ -92,10 +92,7 @@
 
     def has_tag(tag: String): Boolean = tags.contains(tag)
 
-    def session_content: Boolean =
-      has_tag(TAG_CONTENT) ||
-      has_tag(TAG_DOCUMENT) ||
-      has_tag(TAG_UPDATE)
+    def session_content: Boolean = has_tag(TAG_CONTENT) || has_tag(TAG_DOCUMENT)
   }