--- a/src/Pure/Thy/sessions.scala Wed Mar 15 19:33:34 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Wed Mar 15 19:39:34 2017 +0100
@@ -35,8 +35,6 @@
object Base
{
- val empty: Base = Base()
-
lazy val bootstrap: Base =
Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax)
}
--- a/src/Tools/jEdit/src/jedit_resources.scala Wed Mar 15 19:33:34 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Wed Mar 15 19:39:34 2017 +0100
@@ -21,11 +21,6 @@
import org.gjt.sp.jedit.bufferio.BufferIORequest
-object JEdit_Resources
-{
- val empty: JEdit_Resources = new JEdit_Resources(Sessions.Base.empty)
-}
-
class JEdit_Resources(base: Sessions.Base) extends Resources(base)
{
/* document node name */