src/Pure/PIDE/document_editor.scala
changeset 76730 1b8dd8c0492f
parent 76716 a7602257a825
child 76732 0ba6f360d38a
--- a/src/Pure/PIDE/document_editor.scala	Wed Dec 21 13:52:44 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Wed Dec 21 14:00:00 2022 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Pure/PIDE/document_editor.scala
     Author:     Makarius
 
-Central resources for interactive document preparation.
+Central resources and configuration for interactive document preparation.
 */
 
 package isabelle
@@ -42,7 +42,7 @@
   }
 
 
-  /* global state */
+  /* configuration state */
 
   sealed case class State(
     session_background: Option[Sessions.Background] = None,