# HG changeset patch
# User wenzelm
# Date 1661595529 -7200
# Node ID c36e5c6f306966e146732887f9a2990792d87208
# Parent  90ff9ed0cd7563ddad6aeebea0aac785076f79bf
clarified syntax: more uniform;

diff -r 90ff9ed0cd75 -r c36e5c6f3069 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sat Aug 27 12:04:49 2022 +0200
+++ b/src/Doc/System/Sessions.thy	Sat Aug 27 12:18:49 2022 +0200
@@ -50,7 +50,7 @@
   file of that name.
 
   \<^rail>\<open>
-    @{syntax_def chapter_def}: @'chapter_definition' @{syntax name} description
+    @{syntax_def chapter_def}: @'chapter_definition' @{syntax name} description?
     ;
 
     @{syntax_def chapter_entry}: @'chapter' @{syntax name}
diff -r 90ff9ed0cd75 -r c36e5c6f3069 src/Pure/Thy/sessions.ML
--- a/src/Pure/Thy/sessions.ML	Sat Aug 27 12:04:49 2022 +0200
+++ b/src/Pure/Thy/sessions.ML	Sat Aug 27 12:18:49 2022 +0200
@@ -20,6 +20,9 @@
 
 local
 
+val description =
+  Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.embedded)) Input.empty;
+
 val theory_entry = Parse.input Parse.theory_name --| Parse.opt_keyword "global";
 
 val theories =
@@ -51,24 +54,22 @@
 in
 
 val chapter_definition_parser =
-  Parse.chapter_name --
-    (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.embedded)) >> (fn (_, descr) =>
-      Toplevel.keep (fn state =>
-        let
-          val ctxt = Toplevel.context_of state;
-          val _ =
-            Context_Position.report ctxt
-              (Position.range_position (Symbol_Pos.range (Input.source_explode descr)))
-              Markup.comment;
-        in () end));
+  Parse.chapter_name -- description >> (fn (_, descr) =>
+    Toplevel.keep (fn state =>
+      let
+        val ctxt = Toplevel.context_of state;
+        val _ =
+          Context_Position.report ctxt
+            (Position.range_position (Symbol_Pos.range (Input.source_explode descr)))
+            Markup.comment;
+      in () end));
 
 val session_parser =
   Parse.session_name --
   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] --
   Scan.optional (Parse.$$$ "in" |-- Parse.!!! Parse.path_input) (Input.string ".") --
   (Parse.$$$ "=" |--
-    Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
-      Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.embedded)) Input.empty --
+    Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) -- description --
       Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
       Scan.optional (Parse.$$$ "sessions" |--
         Parse.!!! (Scan.repeat1 Parse.session_name)) [] --
diff -r 90ff9ed0cd75 -r c36e5c6f3069 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Aug 27 12:04:49 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 27 12:18:49 2022 +0200
@@ -932,10 +932,12 @@
   }
 
   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) }
@@ -978,8 +980,7 @@
           (($$$("(") ~! (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)) ~