# HG changeset patch
# User wenzelm
# Date 1471000564 -7200
# Node ID 5a7c919a4ada696ad4b1201e2bbfccb57b997696
# Parent  eb4f59275c05d62cf9bbc422538805483a0f700c
more uniform path syntax (like url);

diff -r eb4f59275c05 -r 5a7c919a4ada src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Aug 12 11:54:36 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Aug 12 13:16:04 2016 +0200
@@ -195,7 +195,7 @@
       @@{antiquotation emph} options @{syntax text} |
       @@{antiquotation bold} options @{syntax text} |
       @@{antiquotation verbatim} options @{syntax text} |
-      @@{antiquotation path} options @{syntax name} |
+      @@{antiquotation path} options @{syntax embedded} |
       @@{antiquotation "file"} options @{syntax name} |
       @@{antiquotation dir} options @{syntax name} |
       @@{antiquotation url} options @{syntax embedded} |
diff -r eb4f59275c05 -r 5a7c919a4ada src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Fri Aug 12 11:54:36 2016 +0200
+++ b/src/Pure/Isar/parse.ML	Fri Aug 12 13:16:04 2016 +0200
@@ -270,7 +270,7 @@
 
 val text = group (fn () => "text") (embedded || verbatim);
 
-val path = group (fn () => "file name/path specification") name;
+val path = group (fn () => "file name/path specification") embedded;
 
 val theory_name = group (fn () => "theory name") name;