# HG changeset patch # User wenzelm # Date 1535222896 -7200 # Node ID 5467858e9419482a8453c7e1e70497f93becae4c # Parent e28978310a2addaa6e3adee0163ac86241ea14c8 more uniform cartouche syntax; diff -r e28978310a2a -r 5467858e9419 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Sat Aug 25 20:22:00 2018 +0200 +++ b/src/Doc/System/Sessions.thy Sat Aug 25 20:48:16 2018 +0200 @@ -58,7 +58,7 @@ ; groups: '(' (@{syntax name} +) ')' ; - dir: @'in' @{syntax name} + dir: @'in' @{syntax embedded} ; description: @'description' @{syntax text} ; @@ -74,9 +74,9 @@ ; theory_entry: @{syntax system_name} ('(' @'global' ')')? ; - document_files: @'document_files' ('(' dir ')')? (@{syntax name}+) + document_files: @'document_files' ('(' dir ')')? (@{syntax embedded}+) ; - export_files: @'export_files' ('(' dir ')')? (@{syntax name}+) + export_files: @'export_files' ('(' dir ')')? (@{syntax embedded}+) \} \<^descr> \isakeyword{session}~\A = B + body\ defines a new session \A\ based on diff -r e28978310a2a -r 5467858e9419 src/Pure/Thy/sessions.ML --- a/src/Pure/Thy/sessions.ML Sat Aug 25 20:22:00 2018 +0200 +++ b/src/Pure/Thy/sessions.ML Sat Aug 25 20:48:16 2018 +0200 @@ -37,7 +37,7 @@ val export_files = Parse.$$$ "export_files" |-- - Parse.!!! (Scan.optional in_path ("export", Position.none) -- Scan.repeat1 Parse.name); + Parse.!!! (Scan.optional in_path ("export", Position.none) -- Scan.repeat1 Parse.embedded); in diff -r e28978310a2a -r 5467858e9419 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sat Aug 25 20:22:00 2018 +0200 +++ b/src/Pure/Thy/sessions.scala Sat Aug 25 20:48:16 2018 +0200 @@ -815,7 +815,7 @@ ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) } val export_files = - $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ rep1(name)) ^^ + $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ rep1(embedded)) ^^ { case _ ~ (x ~ y) => (x, y) } command(SESSION) ~!