--- a/src/Pure/General/file.scala Mon Feb 04 14:03:31 2019 +0100
+++ b/src/Pure/General/file.scala Mon Feb 04 15:45:40 2019 +0100
@@ -343,6 +343,12 @@
/* permissions */
+ def is_executable(path: Path): Boolean =
+ {
+ if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok
+ else path.file.canExecute
+ }
+
def executable(path: Path)
{
if (Platform.is_windows) Isabelle_System.bash("chmod a+x " + bash_path(path)).check
--- a/src/Pure/PIDE/markup.ML Mon Feb 04 14:03:31 2019 +0100
+++ b/src/Pure/PIDE/markup.ML Mon Feb 04 15:45:40 2019 +0100
@@ -209,15 +209,20 @@
val task_statistics: Properties.entry
val command_timing: Properties.entry
val theory_timing: Properties.entry
- val exportN: string
- type export_args =
- {id: string option, serial: serial, theory_name: string, name: string, compress: bool}
- val export: export_args -> Properties.T
val loading_theory: string -> Properties.T
val dest_loading_theory: Properties.T -> string option
val build_session_finished: Properties.T
val print_operationsN: string
val print_operations: Properties.T
+ val exportN: string
+ type export_args =
+ {id: string option,
+ serial: serial,
+ theory_name: string,
+ name: string,
+ executable: bool,
+ compress: bool}
+ val export: export_args -> Properties.T
val debugger_state: string -> Properties.T
val debugger_output: string -> Properties.T
val simp_trace_panelN: string
@@ -663,13 +668,6 @@
val theory_timing = (functionN, "theory_timing");
-val exportN = "export";
-type export_args =
- {id: string option, serial: serial, theory_name: string, name: string, compress: bool}
-fun export ({id, serial, theory_name, name, compress}: export_args) =
- [(functionN, exportN), (idN, the_default "" id), (serialN, Value.print_int serial),
- ("theory_name", theory_name), (nameN, name), ("compress", Value.print_bool compress)];
-
fun loading_theory name = [("function", "loading_theory"), ("name", name)];
fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
@@ -681,6 +679,28 @@
val print_operations = [(functionN, print_operationsN)];
+(* export *)
+
+val exportN = "export";
+
+type export_args =
+ {id: string option,
+ serial: serial,
+ theory_name: string,
+ name: string,
+ executable: bool,
+ compress: bool};
+
+fun export ({id, serial, theory_name, name, executable, compress}: export_args) =
+ [(functionN, exportN),
+ (idN, the_default "" id),
+ (serialN, Value.print_int serial),
+ ("theory_name", theory_name),
+ (nameN, name),
+ ("executable", Value.print_bool executable),
+ ("compress", Value.print_bool compress)];
+
+
(* debugger *)
fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)];
--- a/src/Pure/PIDE/markup.scala Mon Feb 04 14:03:31 2019 +0100
+++ b/src/Pure/PIDE/markup.scala Mon Feb 04 15:45:40 2019 +0100
@@ -584,13 +584,29 @@
}
}
+ val BUILD_SESSION_FINISHED = "build_session_finished"
+ val Build_Session_Finished: Properties.T = List((FUNCTION, BUILD_SESSION_FINISHED))
+
+ val PRINT_OPERATIONS = "print_operations"
+
+
+
+ /* export */
+
val EXPORT = "export"
+
object Export
{
sealed case class Args(
- id: Option[String], serial: Long, theory_name: String, name: String, compress: Boolean)
+ id: Option[String],
+ serial: Long,
+ theory_name: String,
+ name: String,
+ executable: Boolean,
+ compress: Boolean)
val THEORY_NAME = "theory_name"
+ val EXECUTABLE = "executable"
val COMPRESS = "compress"
def dest_inline(props: Properties.T): Option[(Args, Path)] =
@@ -600,9 +616,11 @@
(SERIAL, Value.Long(serial)),
(THEORY_NAME, theory_name),
(NAME, name),
+ (EXECUTABLE, Value.Boolean(executable)),
(COMPRESS, Value.Boolean(compress)),
(FILE, file)) if isabelle.Path.is_valid(file) =>
- Some((Args(None, serial, theory_name, name, compress), isabelle.Path.explode(file)))
+ val args = Args(None, serial, theory_name, name, executable, compress)
+ Some((args, isabelle.Path.explode(file)))
case _ => None
}
@@ -614,17 +632,13 @@
(SERIAL, Value.Long(serial)),
(THEORY_NAME, theory_name),
(NAME, name),
+ (EXECUTABLE, Value.Boolean(executable)),
(COMPRESS, Value.Boolean(compress))) =>
- Some(Args(proper_string(id), serial, theory_name, name, compress))
+ Some(Args(proper_string(id), serial, theory_name, name, executable, compress))
case _ => None
}
}
- val BUILD_SESSION_FINISHED = "build_session_finished"
- val Build_Session_Finished: Properties.T = List((FUNCTION, BUILD_SESSION_FINISHED))
-
- val PRINT_OPERATIONS = "print_operations"
-
/* debugger output */
--- a/src/Pure/Thy/export.ML Mon Feb 04 14:03:31 2019 +0100
+++ b/src/Pure/Thy/export.ML Mon Feb 04 15:45:40 2019 +0100
@@ -6,8 +6,10 @@
signature EXPORT =
sig
+ type params = {theory: theory, path: Path.T, executable: bool, compress: bool}
+ val export_params: params -> string list -> unit
val export: theory -> Path.T -> string list -> unit
- val export_raw: theory -> Path.T -> string list -> unit
+ val export_executable: theory -> Path.T -> string list -> unit
val markup: theory -> string -> Markup.T
val message: theory -> string -> string
end;
@@ -25,16 +27,22 @@
else error ("Bad export name: " ^ quote name);
in name end;
-fun gen_export compress thy path body =
+type params = {theory: theory, path: Path.T, executable: bool, compress: bool};
+
+fun export_params ({theory, path, executable, compress}: params) blob =
(Output.try_protocol_message o Markup.export)
{id = Position.get_id (Position.thread_data ()),
serial = serial (),
- theory_name = Context.theory_long_name thy,
+ theory_name = Context.theory_long_name theory,
name = check_name path,
- compress = compress} body;
+ executable = executable,
+ compress = compress} blob;
-val export = gen_export true;
-val export_raw = gen_export false;
+fun export theory path blob =
+ export_params {theory = theory, path = path, executable = false, compress = true} blob;
+
+fun export_executable theory path blob =
+ export_params {theory = theory, path = path, executable = true, compress = true} blob;
(* information message *)
--- a/src/Pure/Thy/export.scala Mon Feb 04 14:03:31 2019 +0100
+++ b/src/Pure/Thy/export.scala Mon Feb 04 15:45:40 2019 +0100
@@ -26,11 +26,13 @@
val session_name = SQL.Column.string("session_name").make_primary_key
val theory_name = SQL.Column.string("theory_name").make_primary_key
val name = SQL.Column.string("name").make_primary_key
+ val executable = SQL.Column.bool("executable")
val compressed = SQL.Column.bool("compressed")
val body = SQL.Column.bytes("body")
val table =
- SQL.Table("isabelle_exports", List(session_name, theory_name, name, compressed, body))
+ SQL.Table("isabelle_exports",
+ List(session_name, theory_name, name, executable, compressed, body))
def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source =
"WHERE " + Data.session_name.equal(session_name) +
@@ -77,6 +79,7 @@
session_name: String,
theory_name: String,
name: String,
+ executable: Boolean,
body: Future[(Boolean, Bytes)])
{
override def toString: String = name
@@ -105,8 +108,9 @@
stmt.string(1) = session_name
stmt.string(2) = theory_name
stmt.string(3) = name
- stmt.bool(4) = compressed
- stmt.bytes(5) = bytes
+ stmt.bool(4) = executable
+ stmt.bool(5) = compressed
+ stmt.bytes(6) = bytes
stmt.execute()
})
}
@@ -140,7 +144,7 @@
def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes,
cache: XZ.Cache = XZ.cache()): Entry =
{
- Entry(session_name, args.theory_name, args.name,
+ Entry(session_name, args.theory_name, args.name, args.executable,
if (args.compress) Future.fork(body.maybe_compress(cache = cache))
else Future.value((false, body)))
}
@@ -149,15 +153,16 @@
: Option[Entry] =
{
val select =
- Data.table.select(List(Data.compressed, Data.body),
+ Data.table.select(List(Data.executable, Data.compressed, Data.body),
Data.where_equal(session_name, theory_name, name))
db.using_statement(select)(stmt =>
{
val res = stmt.execute_query()
if (res.next()) {
+ val executable = res.bool(Data.executable)
val compressed = res.bool(Data.compressed)
val body = res.bytes(Data.body)
- Some(Entry(session_name, theory_name, name, Future.value(compressed, body)))
+ Some(Entry(session_name, theory_name, name, executable, Future.value(compressed, body)))
}
else None
})
@@ -167,8 +172,9 @@
{
val path = dir + Path.basic(theory_name) + Path.explode(name)
if (path.is_file) {
+ val executable = File.is_executable(path)
val uncompressed = Bytes.read(path)
- Some(Entry(session_name, theory_name, name, Future.value((false, uncompressed))))
+ Some(Entry(session_name, theory_name, name, executable, Future.value((false, uncompressed))))
}
else None
}
@@ -295,6 +301,7 @@
progress.echo(export_prefix + "export " + path)
Isabelle_System.mkdirs(path.dir)
Bytes.write(path, entry.uncompressed(cache = store.xz_cache))
+ if (entry.executable) File.executable(path)
}
}
}