--- 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}+)
\<close>}
\<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on