src/Pure/Thy/sessions.scala
changeset 66914 fb3f13a9c756
parent 66873 9953ae603a23
child 66957 82d13ba817b2
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 24 21:20:55 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed Oct 25 11:35:48 2017 +0200
     1.3 @@ -582,8 +582,6 @@
     1.4  
     1.5      private val session_entry: Parser[Session_Entry] =
     1.6      {
     1.7 -      val session_name = atom("session name", _.is_name)
     1.8 -
     1.9        val option =
    1.10          option_name ~ opt($$$("=") ~! option_value ^^
    1.11            { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }