--- a/src/Doc/System/Server.thy Sun May 06 18:20:25 2018 +0000
+++ b/src/Doc/System/Server.thy Mon May 07 22:48:24 2018 +0200
@@ -897,10 +897,14 @@
\end{tabular}
\begin{tabular}{ll}
+ \<^bold>\<open>type\<close> \<open>export =\<close> \\
+ \quad~~\<open>{name: string, base64: bool, body: string}\<close> \\
+ \<^bold>\<open>type\<close> \<open>node_results =\<close> \\
+ \quad~~\<open>{status: node_status, messages: [message], exports: [export]}\<close> \\
\<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
\quad\<open>{ok: bool,\<close> \\
\quad~~\<open>errors: [message],\<close> \\
- \quad~~\<open>nodes: [node \<oplus> {status: node_status, messages: [message]}]}\<close> \\
+ \quad~~\<open>nodes: [node \<oplus> node_results]}\<close> \\
\end{tabular}
\<^medskip>
@@ -916,6 +920,14 @@
invocations of \<^verbatim>\<open>use_theories\<close> are idempotent: it could make sense to do
that with different values for \<open>pretty_margin\<close> or \<open>unicode_symbols\<close> to get
different formatting for \<open>errors\<close> or \<open>messages\<close>.
+
+ The \<open>exports\<close> can be arbitrary binary resources produced by a theory. An
+ \<open>export\<close> \<open>name\<close> roughly follows file-system standards: ``\<^verbatim>\<open>/\<close>'' separated
+ list of base names (excluding special names like ``\<^verbatim>\<open>.\<close>'' or ``\<^verbatim>\<open>..\<close>''). The
+ \<open>base64\<close> field specifies the format of the \<open>body\<close> string: it is true for a
+ byte vector that cannot be represented as plain text in UTF-8 encoding,
+ which means the string needs to be decoded as in
+ \<^verbatim>\<open>java.util.Base64.getDecoder.decode(String)\<close>.
\<close>
--- a/src/Pure/General/bytes.scala Sun May 06 18:20:25 2018 +0000
+++ b/src/Pure/General/bytes.scala Mon May 07 22:48:24 2018 +0200
@@ -160,6 +160,12 @@
Base64.getEncoder.encodeToString(b)
}
+ def maybe_base64: (Boolean, String) =
+ {
+ val s = text
+ if (this == Bytes(s)) (false, s) else (true, base64)
+ }
+
override def toString: String =
{
val str = text
--- a/src/Pure/PIDE/command.scala Sun May 06 18:20:25 2018 +0000
+++ b/src/Pure/PIDE/command.scala Mon May 07 22:48:24 2018 +0200
@@ -28,7 +28,7 @@
object Results
{
type Entry = (Long, XML.Tree)
- val empty = new Results(SortedMap.empty)
+ val empty: Results = new Results(SortedMap.empty)
def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
@@ -68,7 +68,39 @@
}
- /* markup */
+ /* exports */
+
+ object Exports
+ {
+ type Entry = (Long, Export.Entry)
+ val empty: Exports = new Exports(SortedMap.empty)
+ def merge(args: TraversableOnce[Exports]): Exports = (empty /: args)(_ ++ _)
+ }
+
+ final class Exports private(private val rep: SortedMap[Long, Export.Entry])
+ {
+ def iterator: Iterator[Exports.Entry] = rep.iterator
+
+ def + (entry: Exports.Entry): Exports =
+ if (rep.isDefinedAt(entry._1)) this
+ else new Exports(rep + entry)
+
+ def ++ (other: Exports): Exports =
+ if (this eq other) this
+ else if (rep.isEmpty) other
+ else (this /: other.iterator)(_ + _)
+
+ override def hashCode: Int = rep.hashCode
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Exports => rep == other.rep
+ case _ => false
+ }
+ override def toString: String = iterator.mkString("Exports(", ", ", ")")
+ }
+
+
+ /* markups */
object Markup_Index
{
@@ -175,6 +207,9 @@
def merge_results(states: List[State]): Results =
Results.merge(states.map(_.results))
+ def merge_exports(states: List[State]): Exports =
+ Exports.merge(states.map(_.exports))
+
def merge_markups(states: List[State]): Markups =
Markups.merge(states.map(_.markups))
@@ -183,7 +218,8 @@
Markup_Tree.merge(states.map(_.markup(index)), range, elements)
def merge(command: Command, states: List[State]): State =
- State(command, states.flatMap(_.status), merge_results(states), merge_markups(states))
+ State(command, states.flatMap(_.status), merge_results(states),
+ merge_exports(states), merge_markups(states))
/* XML data representation */
@@ -213,7 +249,7 @@
val blobs_info: Blobs_Info =
(blobs_names.map(name => Exn.Res((node_name(name), None)): Blob), blobs_index)
val command = Command(id, node_name(node), blobs_info, span)
- State(command, status, results, markups)
+ State(command, status, results, Exports.empty, markups)
}
}
@@ -221,6 +257,7 @@
command: Command,
status: List[Markup] = Nil,
results: Results = Results.empty,
+ exports: Exports = Exports.empty,
markups: Markups = Markups.empty)
{
lazy val consolidated: Boolean =
@@ -245,7 +282,7 @@
{
val markups1 = markups.redirect(other_command.id)
if (markups1.is_empty) None
- else Some(new State(other_command, Nil, Results.empty, markups1))
+ else Some(new State(other_command, markups = markups1))
}
private def add_status(st: Markup): State =
@@ -254,6 +291,9 @@
private def add_result(entry: Results.Entry): State =
copy(results = results + entry)
+ def add_export(entry: Exports.Entry): State =
+ copy(exports = exports + entry)
+
private def add_markup(
status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
{
@@ -342,7 +382,7 @@
Output.warning("Ignored message without serial number: " + message)
this
}
- }
+ }
}
--- a/src/Pure/PIDE/document.scala Sun May 06 18:20:25 2018 +0000
+++ b/src/Pure/PIDE/document.scala Mon May 07 22:48:24 2018 +0200
@@ -721,6 +721,22 @@
}
}
+ def add_export(id: Document_ID.Generic, entry: Command.Exports.Entry): (Command.State, State) =
+ {
+ execs.get(id) match {
+ case Some(st) =>
+ val new_st = st.add_export(entry)
+ (new_st, copy(execs = execs + (id -> new_st)))
+ case None =>
+ commands.get(id) match {
+ case Some(st) =>
+ val new_st = st.add_export(entry)
+ (new_st, copy(commands = commands + (id -> new_st)))
+ case None => fail
+ }
+ }
+ }
+
def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
{
val version = the_version(id)
--- a/src/Pure/PIDE/markup.ML Sun May 06 18:20:25 2018 +0000
+++ b/src/Pure/PIDE/markup.ML Mon May 07 22:48:24 2018 +0200
@@ -203,7 +203,8 @@
val command_timing: Properties.entry
val theory_timing: Properties.entry
val exportN: string
- type export_args = {id: string option, theory_name: string, name: string, compress: bool}
+ 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
@@ -642,9 +643,10 @@
val theory_timing = (functionN, "theory_timing");
val exportN = "export";
-type export_args = {id: string option, theory_name: string, name: string, compress: bool}
-fun export ({id, theory_name, name, compress}: export_args) =
- [(functionN, exportN), (idN, the_default "" id),
+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)];
--- a/src/Pure/PIDE/markup.scala Sun May 06 18:20:25 2018 +0000
+++ b/src/Pure/PIDE/markup.scala Mon May 07 22:48:24 2018 +0200
@@ -571,7 +571,8 @@
val EXPORT = "export"
object Export
{
- sealed case class Args(id: Option[String], theory_name: String, name: String, compress: Boolean)
+ sealed case class Args(
+ id: Option[String], serial: Long, theory_name: String, name: String, compress: Boolean)
val THEORY_NAME = "theory_name"
val COMPRESS = "compress"
@@ -579,16 +580,26 @@
def dest_inline(props: Properties.T): Option[(Args, Bytes)] =
props match {
case
- List((THEORY_NAME, theory_name), (NAME, name), (COMPRESS, Value.Boolean(compress)),
- (EXPORT, hex)) => Some((Args(None, theory_name, name, compress), Bytes.hex(hex)))
+ List(
+ (SERIAL, Value.Long(serial)),
+ (THEORY_NAME, theory_name),
+ (NAME, name),
+ (COMPRESS, Value.Boolean(compress)),
+ (EXPORT, hex)) =>
+ Some((Args(None, serial, theory_name, name, compress), Bytes.hex(hex)))
case _ => None
}
def unapply(props: Properties.T): Option[Args] =
props match {
- case List((FUNCTION, EXPORT), (ID, id),
- (THEORY_NAME, theory_name), (PATH, name), (COMPRESS, Value.Boolean(compress))) =>
- Some(Args(proper_string(id), theory_name, name, compress))
+ case List(
+ (FUNCTION, EXPORT),
+ (ID, id),
+ (SERIAL, Value.Long(serial)),
+ (THEORY_NAME, theory_name),
+ (NAME, name),
+ (COMPRESS, Value.Boolean(compress))) =>
+ Some(Args(proper_string(id), serial, theory_name, name, compress))
case _ => None
}
}
--- a/src/Pure/PIDE/session.scala Sun May 06 18:20:25 2018 +0000
+++ b/src/Pure/PIDE/session.scala Mon May 07 22:48:24 2018 +0200
@@ -409,15 +409,13 @@
Output.warning("Ignoring bad prover output: " + output.message.toString)
}
- def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
+ def change_command(f: Document.State => (Command.State, Document.State))
{
try {
- val st = global_state.change_result(_.accumulate(state_id, message, xml_cache))
+ val st = global_state.change_result(f)
change_buffer.invoke(false, List(st.command))
}
- catch {
- case _: Document.State.Fail => bad_output()
- }
+ catch { case _: Document.State.Fail => bad_output() }
}
output match {
@@ -430,13 +428,16 @@
case Protocol.Command_Timing(state_id, timing) if prover.defined =>
val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
- accumulate(state_id, xml_cache.elem(message))
+ change_command(_.accumulate(state_id, xml_cache.elem(message), xml_cache))
case Protocol.Theory_Timing(_, _) =>
// FIXME
- case Markup.Export(_) =>
- // FIXME
+ case Markup.Export(args)
+ if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
+ val id = Value.Long.unapply(args.id.get).get
+ val entry = (args.serial, Export.make_entry("", args, msg.bytes))
+ change_command(_.add_export(id, entry))
case Markup.Assign_Update =>
msg.text match {
@@ -474,7 +475,7 @@
case _ =>
output.properties match {
case Position.Id(state_id) =>
- accumulate(state_id, output.message)
+ change_command(_.accumulate(state_id, output.message, xml_cache))
case _ if output.is_init =>
prover.get.options(session_options)
--- a/src/Pure/Thy/export.ML Sun May 06 18:20:25 2018 +0000
+++ b/src/Pure/Thy/export.ML Mon May 07 22:48:24 2018 +0200
@@ -1,26 +1,39 @@
(* Title: Pure/Thy/export.ML
Author: Makarius
-Manage theory exports.
+Manage theory exports: compressed blobs.
*)
signature EXPORT =
sig
- val export: theory -> string -> Output.output -> unit
- val export_uncompressed: theory -> string -> Output.output -> unit
+ val export: theory -> string -> string -> unit
+ val export_raw: theory -> string -> string list -> unit
end;
structure Export: EXPORT =
struct
-fun gen_export compress thy name output =
+fun check_name name =
+ let
+ fun err () = error ("Bad export name " ^ quote name);
+ fun check_elem elem =
+ if member (op =) ["", ".", ".."] elem then err ()
+ else ignore (Path.basic elem handle ERROR _ => err ());
+
+ val elems = space_explode "/" name;
+ val _ = null elems andalso err ();
+ val _ = List.app check_elem elems;
+ in name end;
+
+fun gen_export compress thy name body =
(Output.try_protocol_message o Markup.export)
{id = Position.get_id (Position.thread_data ()),
+ serial = serial (),
theory_name = Context.theory_long_name thy,
- name = name,
- compress = compress} [output];
+ name = check_name name,
+ compress = compress} body;
-val export = gen_export true;
-val export_uncompressed = gen_export false;
+fun export thy name body = gen_export (size body > 60) thy name [body];
+fun export_raw thy name body = gen_export false thy name body;
end;
--- a/src/Pure/Thy/export.scala Sun May 06 18:20:25 2018 +0000
+++ b/src/Pure/Thy/export.scala Mon May 07 22:48:24 2018 +0200
@@ -1,7 +1,7 @@
/* Title: Pure/Thy/export.scala
Author: Makarius
-Manage theory exports.
+Manage theory exports: compressed blobs.
*/
package isabelle
@@ -33,31 +33,39 @@
stmt.execute_query().iterator(res => res.string(Data.name)).toList)
}
+ def message(msg: String, theory_name: String, name: String): String =
+ msg + " " + quote(name) + " for theory " + quote(theory_name)
+
sealed case class Entry(
- session_name: String, theory_name: String, name: String, compressed: Boolean, body: Bytes)
+ session_name: String,
+ theory_name: String,
+ name: String,
+ compressed: Boolean,
+ body: Future[Bytes])
{
override def toString: String = theory_name + ":" + name
- def message(msg: String): String =
- msg + " " + quote(name) + " for theory " + quote(theory_name)
-
- lazy val compressed_body: Bytes = if (compressed) body else body.compress()
- lazy val uncompressed_body: Bytes = if (compressed) body.uncompress() else body
-
def write(db: SQL.Database)
{
+ val bytes = body.join
db.using_statement(Data.table.insert())(stmt =>
{
stmt.string(1) = session_name
stmt.string(2) = theory_name
stmt.string(3) = name
stmt.bool(4) = compressed
- stmt.bytes(5) = body
+ stmt.bytes(5) = bytes
stmt.execute()
})
}
}
+ def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry =
+ {
+ Entry(session_name, args.theory_name, args.name, args.compress,
+ if (args.compress) Future.fork(body.compress()) else Future.value(body))
+ }
+
def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry =
{
val select =
@@ -69,9 +77,9 @@
if (res.next()) {
val compressed = res.bool(Data.compressed)
val body = res.bytes(Data.body)
- Entry(session_name, theory_name, name, compressed, body)
+ Entry(session_name, theory_name, name, compressed, Future.value(body))
}
- else error(Entry(session_name, theory_name, name, false, Bytes.empty).message("Bad export"))
+ else error(message("Bad export", theory_name, name))
})
}
@@ -87,27 +95,21 @@
private val export_errors = Synchronized[List[String]](Nil)
private val consumer =
- Consumer_Thread.fork(name = "export")(consume = (future: Future[Entry]) =>
+ Consumer_Thread.fork(name = "export")(consume = (entry: Entry) =>
{
- val entry = future.join
-
+ entry.body.join
db.transaction {
if (read_names(db, entry.session_name, entry.theory_name).contains(entry.name)) {
- export_errors.change(errs => entry.message("Duplicate export") :: errs)
+ val err = message("Duplicate export", entry.theory_name, entry.name)
+ export_errors.change(errs => err :: errs)
}
else entry.write(db)
}
true
})
- def apply(session_name: String, args: Markup.Export.Args, body: Bytes)
- {
- consumer.send(
- if (args.compress)
- Future.fork(Entry(session_name, args.theory_name, args.name, true, body.compress()))
- else
- Future.value(Entry(session_name, args.theory_name, args.name, false, body)))
- }
+ def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit =
+ consumer.send(make_entry(session_name, args, body))
def shutdown(close: Boolean = false): List[String] =
{
--- a/src/Pure/Thy/thy_resources.scala Sun May 06 18:20:25 2018 +0000
+++ b/src/Pure/Thy/thy_resources.scala Mon May 07 22:48:24 2018 +0200
@@ -72,6 +72,16 @@
(_, tree) <- state.command_results(version, command).iterator
} yield (tree, pos)).toList
}
+
+ def exports(node_name: Document.Node.Name): List[Export.Entry] =
+ {
+ val node = version.nodes(node_name)
+ Command.Exports.merge(
+ for {
+ command <- node.commands.iterator
+ st <- state.command_states(version, command).iterator
+ } yield st.exports).iterator.map(_._2).toList
+ }
}
class Session private[Thy_Resources](
--- a/src/Pure/Tools/server_commands.scala Sun May 06 18:20:25 2018 +0000
+++ b/src/Pure/Tools/server_commands.scala Mon May 07 22:48:24 2018 +0200
@@ -212,7 +212,13 @@
("messages" ->
(for {
(tree, pos) <- result.messages(name) if Protocol.is_exported(tree)
- } yield output_message(tree, pos)))))
+ } yield output_message(tree, pos))) +
+ ("exports" ->
+ (for { entry <- result.exports(name) }
+ yield {
+ val (base64, body) = entry.body.join.maybe_base64
+ JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
+ }))))
(result_json, result)
}