Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more uniform path syntax (like url);
authorwenzelm
Fri, 12 Aug 2016 13:16:04 +0200
changeset 63672 5a7c919a4ada
parent 63671 eb4f59275c05
child 63673 2314e99c18a7
more uniform path syntax (like url);
src/Doc/Isar_Ref/Document_Preparation.thy file | annotate | diff | comparison | revisions
src/Pure/Isar/parse.ML file | annotate | diff | comparison | revisions 
--- 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} |
--- 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;
isabelle