# HG changeset patch
# User wenzelm
# Date 1751028255 -7200
# Node ID 7dd048f6ead621f93140533d8a37507663aa62db
# Parent  beba766806edbc9e2ed25351ae21e98923c17a01
tuned signature: more generic operations;

diff -r beba766806ed -r 7dd048f6ead6 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Jun 27 14:41:18 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Jun 27 14:44:15 2025 +0200
@@ -818,7 +818,9 @@
   /* model */
 
   trait Session {
+    def session_options: Options
     def resources: Resources
+    def store: Store
   }
 
   trait Model {