unused;
authorwenzelm
Wed Mar 15 19:39:34 2017 +0100 (2017-03-15 ago)
changeset 652692947837b9f04
parent 65268 75f2aa8ecb12
child 65270 ed8043342c9c
unused;
src/Pure/Thy/sessions.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed Mar 15 19:33:34 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed Mar 15 19:39:34 2017 +0100
     1.3 @@ -35,8 +35,6 @@
     1.4  
     1.5    object Base
     1.6    {
     1.7 -    val empty: Base = Base()
     1.8 -
     1.9      lazy val bootstrap: Base =
    1.10        Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax)
    1.11    }
     2.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Mar 15 19:33:34 2017 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Mar 15 19:39:34 2017 +0100
     2.3 @@ -21,11 +21,6 @@
     2.4  import org.gjt.sp.jedit.bufferio.BufferIORequest
     2.5  
     2.6  
     2.7 -object JEdit_Resources
     2.8 -{
     2.9 -  val empty: JEdit_Resources = new JEdit_Resources(Sessions.Base.empty)
    2.10 -}
    2.11 -
    2.12  class JEdit_Resources(base: Sessions.Base) extends Resources(base)
    2.13  {
    2.14    /* document node name */