# 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 \ - @@{command display_drafts} (@{syntax name} +) + @@{command display_drafts} (@{syntax xname} +) \} \<^descr> @{command "display_drafts"}~\paths\ 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