# HG changeset patch
# User wenzelm
# Date 1671445006 -3600
# Node ID 3543ecb4c97d266d3829e60e128cef821324068f
# Parent  8ad17c4669da1ea6a271b6b8ee8b0acd74d083d6
tuned signature;

diff -r 8ad17c4669da -r 3543ecb4c97d src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Sun Dec 18 18:30:37 2022 +0100
+++ b/src/Pure/PIDE/editor.scala	Mon Dec 19 11:16:46 2022 +0100
@@ -20,16 +20,12 @@
   protected val document_editor: Synchronized[Document_Editor.State] =
     Synchronized(Document_Editor.State())
 
-  def document_editor_session: Option[Sessions.Background] =
-    document_editor.value.session_background
-  def document_editor_active: Boolean =
-    document_editor.value.is_active
-  def document_editor_setup(background: Option[Sessions.Background]): Unit =
+  def document_session: Option[Sessions.Background] = document_editor.value.session_background
+  def document_active: Boolean = document_editor.value.is_active
+  def document_setup(background: Option[Sessions.Background]): Unit =
     document_editor.change(_.copy(session_background = background))
-  def document_editor_init(id: AnyRef): Unit =
-    document_editor.change(_.register_view(id))
-  def document_editor_exit(id: AnyRef): Unit =
-    document_editor.change(_.unregister_view(id))
+  def document_init(id: AnyRef): Unit = document_editor.change(_.register_view(id))
+  def document_exit(id: AnyRef): Unit = document_editor.change(_.unregister_view(id))
 
 
   /* current situation */
diff -r 8ad17c4669da -r 3543ecb4c97d src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Sun Dec 18 18:30:37 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Mon Dec 19 11:16:46 2022 +0100
@@ -138,7 +138,7 @@
               val session_background =
                 Document_Build.session_background(
                   options, session, dirs = JEdit_Sessions.session_dirs)
-              PIDE.editor.document_editor_setup(Some(session_background))
+              PIDE.editor.document_setup(Some(session_background))
               GUI_Thread.later { show_state(); show_page(theories_page) }
             }
             catch {
@@ -277,7 +277,7 @@
     }
 
   override def init(): Unit = {
-    PIDE.editor.document_editor_init(dockable)
+    PIDE.editor.document_init(dockable)
     init_state()
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
@@ -290,6 +290,6 @@
     PIDE.session.global_options -= main
     PIDE.session.commands_changed -= main
     delay_resize.revoke()
-    PIDE.editor.document_editor_exit(dockable)
+    PIDE.editor.document_exit(dockable)
   }
 }