clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty;
authorwenzelm
Wed Nov 01 12:28:20 2017 +0100 (18 months ago)
changeset 6697013857f49d215
parent 66969 39077839947e
child 66971 43b2aac6053c
clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty;
src/Doc/ROOT
src/Doc/System/Sessions.thy
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Doc/ROOT	Tue Oct 31 22:17:38 2017 +0100
     1.2 +++ b/src/Doc/ROOT	Wed Nov 01 12:28:20 2017 +0100
     1.3 @@ -127,7 +127,6 @@
     1.4  
     1.5  session Intro (doc) in "Intro" = Pure +
     1.6    options [document_variants = "intro"]
     1.7 -  theories
     1.8    document_files (in "..")
     1.9      "prepare_document"
    1.10      "pdfsetup.sty"
    1.11 @@ -272,7 +271,6 @@
    1.12  
    1.13  session Logics (doc) in "Logics" = Pure +
    1.14    options [document_variants = "logics"]
    1.15 -  theories
    1.16    document_files (in "..")
    1.17      "prepare_document"
    1.18      "pdfsetup.sty"
    1.19 @@ -328,7 +326,6 @@
    1.20  
    1.21  session Nitpick (doc) in "Nitpick" = Pure +
    1.22    options [document_variants = "nitpick"]
    1.23 -  theories
    1.24    document_files (in "..")
    1.25      "prepare_document"
    1.26      "pdfsetup.sty"
    1.27 @@ -364,7 +361,6 @@
    1.28  
    1.29  session Sledgehammer (doc) in "Sledgehammer" = Pure +
    1.30    options [document_variants = "sledgehammer"]
    1.31 -  theories
    1.32    document_files (in "..")
    1.33      "prepare_document"
    1.34      "pdfsetup.sty"
     2.1 --- a/src/Doc/System/Sessions.thy	Tue Oct 31 22:17:38 2017 +0100
     2.2 +++ b/src/Doc/System/Sessions.thy	Wed Nov 01 12:28:20 2017 +0100
     2.3 @@ -55,7 +55,7 @@
     2.4      @{syntax_def session_entry}: @'session' spec '='
     2.5        (@{syntax system_name} '+')? body
     2.6      ;
     2.7 -    body: description? options? (theories+) \<newline> (document_files*)
     2.8 +    body: description? options? (sessions?) (theories*) \<newline> (document_files*)
     2.9      ;
    2.10      spec: @{syntax system_name} groups? dir?
    2.11      ;
    2.12 @@ -73,7 +73,7 @@
    2.13      ;
    2.14      sessions: @'sessions' (@{syntax system_name}+)
    2.15      ;
    2.16 -    theories: @'theories' opts? (theory_entry*)
    2.17 +    theories: @'theories' opts? (theory_entry+)
    2.18      ;
    2.19      theory_entry: @{syntax system_name} ('(' @'global' ')')?
    2.20      ;
     3.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 31 22:17:38 2017 +0100
     3.2 +++ b/src/Pure/Thy/sessions.scala	Wed Nov 01 12:28:20 2017 +0100
     3.3 @@ -691,7 +691,7 @@
     3.4  
     3.5        val theories =
     3.6          $$$(THEORIES) ~!
     3.7 -          ((options | success(Nil)) ~ rep(theory_entry)) ^^
     3.8 +          ((options | success(Nil)) ~ rep1(theory_entry)) ^^
     3.9            { case _ ~ (x ~ y) => (x, y) }
    3.10  
    3.11        val document_files =
    3.12 @@ -708,8 +708,8 @@
    3.13              (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
    3.14                (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
    3.15                (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
    3.16 -              (($$$(SESSIONS) ~! rep(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
    3.17 -              rep1(theories) ~
    3.18 +              (($$$(SESSIONS) ~! rep1(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
    3.19 +              rep(theories) ~
    3.20                (rep(document_files) ^^ (x => x.flatten))))) ^^
    3.21          { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
    3.22              Session_Entry(pos, a, b, c, d, e, f, g, h, i) }