src/Pure/Thy/sessions.scala
changeset 66970 13857f49d215
parent 66969 39077839947e
child 66974 b14c24b31f45
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 31 22:17:38 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed Nov 01 12:28:20 2017 +0100
     1.3 @@ -691,7 +691,7 @@
     1.4  
     1.5        val theories =
     1.6          $$$(THEORIES) ~!
     1.7 -          ((options | success(Nil)) ~ rep(theory_entry)) ^^
     1.8 +          ((options | success(Nil)) ~ rep1(theory_entry)) ^^
     1.9            { case _ ~ (x ~ y) => (x, y) }
    1.10  
    1.11        val document_files =
    1.12 @@ -708,8 +708,8 @@
    1.13              (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
    1.14                (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
    1.15                (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
    1.16 -              (($$$(SESSIONS) ~! rep(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
    1.17 -              rep1(theories) ~
    1.18 +              (($$$(SESSIONS) ~! rep1(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
    1.19 +              rep(theories) ~
    1.20                (rep(document_files) ^^ (x => x.flatten))))) ^^
    1.21          { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
    1.22              Session_Entry(pos, a, b, c, d, e, f, g, h, i) }