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