# HG changeset patch
# User wenzelm
# Date 1549291540 -3600
# Node ID c175499a7537581e4549fc72c57c9dc18bf76518
# Parent  60b5a47316956c831eb69f2370e2708522f1484c
added executable flag for exports;
clarified signature;

diff -r 60b5a4731695 -r c175499a7537 src/Pure/General/file.scala
--- 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
diff -r 60b5a4731695 -r c175499a7537 src/Pure/PIDE/markup.ML
--- 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)];
diff -r 60b5a4731695 -r c175499a7537 src/Pure/PIDE/markup.scala
--- 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 */
 
diff -r 60b5a4731695 -r c175499a7537 src/Pure/Thy/export.ML
--- 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 *)
diff -r 60b5a4731695 -r c175499a7537 src/Pure/Thy/export.scala
--- 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)
           }
         }
       }