clarified syntax;
authorwenzelm
Wed Apr 13 11:31:13 2016 +0200 (2016-04-13 ago)
changeset 629655bf08c9aa036
parent 62964 d0c1b2dbca5b
child 62966 771b8ad5c7fc
clarified syntax;
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/Isar_Ref/Spec.thy
src/Pure/Isar/parse.ML
src/Pure/Isar/parse.scala
src/Pure/PIDE/command.scala
     1.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Wed Apr 13 11:26:52 2016 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Wed Apr 13 11:31:13 2016 +0200
     1.3 @@ -195,8 +195,8 @@
     1.4        @@{antiquotation emph} options @{syntax text} |
     1.5        @@{antiquotation bold} options @{syntax text} |
     1.6        @@{antiquotation verbatim} options @{syntax text} |
     1.7 -      @@{antiquotation "file"} options @{syntax name} |
     1.8 -      @@{antiquotation file_unchecked} options @{syntax name} |
     1.9 +      @@{antiquotation "file"} options @{syntax xname} |
    1.10 +      @@{antiquotation file_unchecked} options @{syntax xname} |
    1.11        @@{antiquotation url} options @{syntax name} |
    1.12        @@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
    1.13      ;
    1.14 @@ -613,7 +613,7 @@
    1.15    \end{matharray}
    1.16  
    1.17    @{rail \<open>
    1.18 -    @@{command display_drafts} (@{syntax name} +)
    1.19 +    @@{command display_drafts} (@{syntax xname} +)
    1.20    \<close>}
    1.21  
    1.22    \<^descr> @{command "display_drafts"}~\<open>paths\<close> performs simple output of a given list
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Wed Apr 13 11:26:52 2016 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Wed Apr 13 11:31:13 2016 +0200
     2.3 @@ -1054,7 +1054,7 @@
     2.4        @@{command SML_file_no_debug} |
     2.5        @@{command ML_file} |
     2.6        @@{command ML_file_debug} |
     2.7 -      @@{command ML_file_no_debug}) @{syntax name} ';'?
     2.8 +      @@{command ML_file_no_debug}) @{syntax xname} ';'?
     2.9      ;
    2.10      (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
    2.11        @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
     3.1 --- a/src/Pure/Isar/parse.ML	Wed Apr 13 11:26:52 2016 +0200
     3.2 +++ b/src/Pure/Isar/parse.ML	Wed Apr 13 11:31:13 2016 +0200
     3.3 @@ -271,7 +271,7 @@
     3.4  val text = group (fn () => "text")
     3.5    (short_ident || long_ident || sym_ident || string || number || verbatim || cartouche);
     3.6  
     3.7 -val path = group (fn () => "file name/path specification") name;
     3.8 +val path = group (fn () => "file name/path specification") xname;
     3.9  
    3.10  val theory_name = group (fn () => "theory name") name;
    3.11  val theory_xname = group (fn () => "theory name reference") xname;
     4.1 --- a/src/Pure/Isar/parse.scala	Wed Apr 13 11:26:52 2016 +0200
     4.2 +++ b/src/Pure/Isar/parse.scala	Wed Apr 13 11:31:13 2016 +0200
     4.3 @@ -74,7 +74,7 @@
     4.4      def document_source: Parser[String] = atom("document source", _.is_text)
     4.5  
     4.6      def path: Parser[String] =
     4.7 -      atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
     4.8 +      atom("file name/path specification", tok => tok.is_xname && Path.is_wellformed(tok.content))
     4.9  
    4.10      def theory_name: Parser[String] =
    4.11        atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
     5.1 --- a/src/Pure/PIDE/command.scala	Wed Apr 13 11:26:52 2016 +0200
     5.2 +++ b/src/Pure/PIDE/command.scala	Wed Apr 13 11:31:13 2016 +0200
     5.3 @@ -322,7 +322,7 @@
     5.4    private def find_file(tokens: List[(Token, Int)]): Option[(String, Int)] =
     5.5      if (tokens.exists({ case (t, _) => t.is_command })) {
     5.6        tokens.dropWhile({ case (t, _) => !t.is_command }).
     5.7 -        collectFirst({ case (t, i) if t.is_name => (t.content, i) })
     5.8 +        collectFirst({ case (t, i) if t.is_xname => (t.content, i) })
     5.9      }
    5.10      else None
    5.11