--- 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
--- 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
--- 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) ~!