tuned comments;
authorwenzelm
Wed, 21 Dec 2022 14:00:00 +0100
changeset 76730 1b8dd8c0492f
parent 76729 b045b40a65cc
child 76731 872fc664cd99
tuned comments;
src/Pure/PIDE/document_editor.scala
--- 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,