src/Pure/Thy/sessions.scala

             Position.here(old_entry.pos) + Position.here(entry.pos))
       }
   }
 
   private object Parsers extends Options.Parsers {
+    private val description: Parser[String] =
+      ($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")
+
     private val chapter_def: Parser[Chapter_Def] =
-      command(CHAPTER_DEFINITION) ~!
-        (position(chapter_name) ~ $$$(DESCRIPTION) ~ text) ^^
-        { case _ ~ ((a, pos) ~ _ ~ b) => Chapter_Def(pos, a, b) }
+      command(CHAPTER_DEFINITION) ~! (position(chapter_name) ~ description) ^^
+        { case _ ~ ((a, pos) ~ b) => Chapter_Def(pos, a, b) }
 
     private val chapter_entry: Parser[Chapter_Entry] =
       command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter_Entry(a) }
 
     private val session_entry: Parser[Session_Entry] = {

       command(SESSION) ~!
         (position(session_name) ~
           (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
           (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
           ($$$("=") ~!
-            (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
-              (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
+            (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~ description ~
               (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
               (($$$(SESSIONS) ~! rep1(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
               (($$$(DIRECTORIES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
               rep(theories) ~
               (opt(document_theories) ^^ (x => x.getOrElse(Nil))) ~