--- a/etc/symbols Mon Apr 29 00:36:43 2019 +0100
+++ b/etc/symbols Mon Apr 29 00:36:54 2019 +0100
@@ -394,6 +394,7 @@
\<^class> argument: cartouche
\<^class_syntax> argument: cartouche
\<^command_keyword> argument: cartouche
+\<^const> argument: cartouche
\<^const_abbrev> argument: cartouche
\<^const_name> argument: cartouche
\<^const_syntax> argument: cartouche
--- a/src/Pure/Admin/build_release.scala Mon Apr 29 00:36:43 2019 +0100
+++ b/src/Pure/Admin/build_release.scala Mon Apr 29 00:36:54 2019 +0100
@@ -38,8 +38,8 @@
def bundle_info(platform: Platform.Family.Value): Bundle_Info =
platform match {
- case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
- case Platform.Family.macos => Bundle_Info(platform, "Mac OS X", dist_name + "_macos.tar.gz")
+ case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.xz")
+ case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.xz")
case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
}
}
@@ -522,11 +522,11 @@
isabelle_target + Path.explode(isabelle_name))
Isabelle_System.rm_tree(linux_app)
- val archive_name = isabelle_name + "_linux.tar.gz"
+ val archive_name = isabelle_name + "_linux.tar.xz"
progress.echo("Packaging " + archive_name + " ...")
execute_tar(tmp_dir,
- "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
- Bash.string(isabelle_name))
+ "-cf- " + Bash.string(isabelle_name) +
+ " | xz > " + File.bash_path(release.dist_dir + Path.explode(archive_name)))
case Platform.Family.macos =>
@@ -582,11 +582,11 @@
// application archive
- val archive_name = isabelle_name + "_macos.tar.gz"
+ val archive_name = isabelle_name + "_macos.tar.xz"
progress.echo("Packaging " + archive_name + " ...")
execute_tar(tmp_dir,
- "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
- File.bash_path(isabelle_app))
+ "-cf- " + File.bash_path(isabelle_app) +
+ " | xz > " + File.bash_path(release.dist_dir + Path.explode(archive_name)))
case Platform.Family.windows =>
--- a/src/Pure/Isar/parse.ML Mon Apr 29 00:36:43 2019 +0100
+++ b/src/Pure/Isar/parse.ML Mon Apr 29 00:36:54 2019 +0100
@@ -67,6 +67,7 @@
val name_position: (string * Position.T) parser
val binding: binding parser
val embedded: string parser
+ val embedded_input: Input.source parser
val embedded_position: (string * Position.T) parser
val text: string parser
val path: string parser
@@ -278,7 +279,8 @@
(cartouche || string || short_ident || long_ident || sym_ident ||
term_var || type_ident || type_var || number);
-val embedded_position = input embedded >> Input.source_content;
+val embedded_input = input embedded;
+val embedded_position = embedded_input >> Input.source_content;
val text = group (fn () => "text") (embedded || verbatim);
--- a/src/Pure/Pure.thy Mon Apr 29 00:36:43 2019 +0100
+++ b/src/Pure/Pure.thy Mon Apr 29 00:36:54 2019 +0100
@@ -125,7 +125,7 @@
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>generate_file\<close>
"generate source file, with antiquotations"
- (Parse.path_binding -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
+ (Parse.path_binding -- (\<^keyword>\<open>=\<close> |-- Parse.embedded_input)
>> Generated_Files.generate_file_cmd);
--- a/src/Pure/Thy/document_marker.ML Mon Apr 29 00:36:43 2019 +0100
+++ b/src/Pure/Thy/document_marker.ML Mon Apr 29 00:36:54 2019 +0100
@@ -103,7 +103,7 @@
setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #>
setup0 (Binding.make ("date", \<^here>)) Parse.embedded (meta_data Markup.meta_date) #>
setup0 (Binding.make ("license", \<^here>)) Parse.embedded (meta_data Markup.meta_license) #>
- setup0 (Binding.make ("description", \<^here>)) (Parse.input Parse.embedded)
+ setup0 (Binding.make ("description", \<^here>)) Parse.embedded_input
(fn source => fn ctxt =>
let
val (arg, pos) = Input.source_content source;
--- a/src/Tools/jEdit/src/isabelle_vfs.scala Mon Apr 29 00:36:43 2019 +0100
+++ b/src/Tools/jEdit/src/isabelle_vfs.scala Mon Apr 29 00:36:54 2019 +0100
@@ -73,7 +73,7 @@
override def _getFile(vfs_session: AnyRef, url: String, component: Component): VFSFile =
{
val parent = getParentOfPath(url)
- if (parent == prefix) null
+ if (parent == prefix) new VFSFile(prefix, prefix, prefix, VFSFile.DIRECTORY, 0L, false)
else {
val files = _listFiles(vfs_session, parent, component)
if (files == null) null