# HG changeset patch
# User wenzelm
# Date 1489480862 -3600
# Node ID 6af51a47545bbdc21a4708dad01eb6f5a63c1c94
# Parent  420f55912b3e70fb0c7c88b5e335087bdeb0210f
more abstract module Document;

diff -r 420f55912b3e -r 6af51a47545b src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Mar 14 00:13:38 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Tue Mar 14 09:41:02 2017 +0100
@@ -473,6 +473,11 @@
 
   /* model */
 
+  trait Session
+  {
+    def resources: Resources
+  }
+
   trait Model
   {
     def session: Session
diff -r 420f55912b3e -r 6af51a47545b src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Tue Mar 14 00:13:38 2017 +0100
+++ b/src/Pure/PIDE/session.scala	Tue Mar 14 09:41:02 2017 +0100
@@ -114,7 +114,7 @@
 }
 
 
-class Session(val resources: Resources)
+class Session(val resources: Resources) extends Document.Session
 {
   session =>