# HG changeset patch
# User wenzelm
# Date 1508932073 -7200
# Node ID aca50a1572c59168fb8699728be0d3d21f4a79e5
# Parent  f4259adc928a690a202800a1db4d840a450fd401
more documentation;

diff -r f4259adc928a -r aca50a1572c5 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Oct 25 11:40:58 2017 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Wed Oct 25 13:47:53 2017 +0200
@@ -188,6 +188,9 @@
     ;
     @{syntax_def par_name}: '(' @{syntax name} ')'
   \<close>}
+
+  A @{syntax_def system_name} is like @{syntax name}, but it excludes
+  white-space characters and needs to conform to file-name notation.
 \<close>
 
 
diff -r f4259adc928a -r aca50a1572c5 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Wed Oct 25 11:40:58 2017 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Wed Oct 25 13:47:53 2017 +0200
@@ -58,7 +58,8 @@
   such a global @{command (global) "end"}.
 
   @{rail \<open>
-    @@{command theory} @{syntax name} @'imports' (@{syntax name} +) \<newline>
+    @@{command theory} @{syntax system_name}
+      @'imports' (@{syntax system_name} +) \<newline>
       keywords? abbrevs? @'begin'
     ;
     keywords: @'keywords' (keyword_decls + @'and')
diff -r f4259adc928a -r aca50a1572c5 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Wed Oct 25 11:40:58 2017 +0200
+++ b/src/Doc/System/Sessions.thy	Wed Oct 25 13:47:53 2017 +0200
@@ -52,11 +52,12 @@
     @{syntax_def session_chapter}: @'chapter' @{syntax name}
     ;
 
-    @{syntax_def session_entry}: @'session' spec '=' (@{syntax name} '+')? body
+    @{syntax_def session_entry}: @'session' spec '='
+      (@{syntax system_name} '+')? body
     ;
     body: description? options? (theories+) \<newline> (document_files*)
     ;
-    spec: @{syntax name} groups? dir?
+    spec: @{syntax system_name} groups? dir?
     ;
     groups: '(' (@{syntax name} +) ')'
     ;
@@ -70,11 +71,11 @@
     ;
     value: @{syntax name} | @{syntax real}
     ;
-    sessions: @'sessions' (@{syntax name}+)
+    sessions: @'sessions' (@{syntax system_name}+)
     ;
     theories: @'theories' opts? (theory_entry*)
     ;
-    theory_entry: @{syntax name} ('(' @'global' ')')?
+    theory_entry: @{syntax system_name} ('(' @'global' ')')?
     ;
     document_files: @'document_files' ('(' dir ')')? (@{syntax name}+)
   \<close>}