# HG changeset patch
# User wenzelm
# Date 1460539873 -7200
# Node ID 5bf08c9aa036c16395637e04b0cdcfff24a4fc8c
# Parent  d0c1b2dbca5b76baacaa2492b2ad792e09bbbc8e
clarified syntax;

diff -r d0c1b2dbca5b -r 5bf08c9aa036 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Wed Apr 13 11:26:52 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Wed Apr 13 11:31:13 2016 +0200
@@ -195,8 +195,8 @@
       @@{antiquotation emph} options @{syntax text} |
       @@{antiquotation bold} options @{syntax text} |
       @@{antiquotation verbatim} options @{syntax text} |
-      @@{antiquotation "file"} options @{syntax name} |
-      @@{antiquotation file_unchecked} options @{syntax name} |
+      @@{antiquotation "file"} options @{syntax xname} |
+      @@{antiquotation file_unchecked} options @{syntax xname} |
       @@{antiquotation url} options @{syntax name} |
       @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
     ;
@@ -613,7 +613,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command display_drafts} (@{syntax name} +)
+    @@{command display_drafts} (@{syntax xname} +)
   \<close>}
 
   \<^descr> @{command "display_drafts"}~\<open>paths\<close> performs simple output of a given list
diff -r d0c1b2dbca5b -r 5bf08c9aa036 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Wed Apr 13 11:26:52 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Wed Apr 13 11:31:13 2016 +0200
@@ -1054,7 +1054,7 @@
       @@{command SML_file_no_debug} |
       @@{command ML_file} |
       @@{command ML_file_debug} |
-      @@{command ML_file_no_debug}) @{syntax name} ';'?
+      @@{command ML_file_no_debug}) @{syntax xname} ';'?
     ;
     (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
       @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
diff -r d0c1b2dbca5b -r 5bf08c9aa036 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Wed Apr 13 11:26:52 2016 +0200
+++ b/src/Pure/Isar/parse.ML	Wed Apr 13 11:31:13 2016 +0200
@@ -271,7 +271,7 @@
 val text = group (fn () => "text")
   (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
 
-val path = group (fn () => "file name/path specification") name;
+val path = group (fn () => "file name/path specification") xname;
 
 val theory_name = group (fn () => "theory name") name;
 val theory_xname = group (fn () => "theory name reference") xname;
diff -r d0c1b2dbca5b -r 5bf08c9aa036 src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Wed Apr 13 11:26:52 2016 +0200
+++ b/src/Pure/Isar/parse.scala	Wed Apr 13 11:31:13 2016 +0200
@@ -74,7 +74,7 @@
     def document_source: Parser[String] = atom("document source", _.is_text)
 
     def path: Parser[String] =
-      atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
+      atom("file name/path specification", tok => tok.is_xname && Path.is_wellformed(tok.content))
 
     def theory_name: Parser[String] =
       atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
diff -r d0c1b2dbca5b -r 5bf08c9aa036 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Apr 13 11:26:52 2016 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Apr 13 11:31:13 2016 +0200
@@ -322,7 +322,7 @@
   private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
     if (tokens.exists({ case (t, _) => t.is_command })) {
       tokens.dropWhile({ case (t, _) => !t.is_command }).
-        collectFirst({ case (t, i) if t.is_name => (t.content, i) })
+        collectFirst({ case (t, i) if t.is_xname => (t.content, i) })
     }
     else None