# HG changeset patch # User wenzelm # Date 1525726104 -7200 # Node ID 3687109009c4ebe6d711c7cb6539abb7e69724c7 # Parent b2d84b1114face1091e8c84f595a07d64da5bc22# Parent a514e29db9806aa874b80e4e1ebbba9e0b29f913 merged diff -r b2d84b1114fa -r 3687109009c4 src/Doc/System/Server.thy --- 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>\type\ \export =\ \\ + \quad~~\{name: string, base64: bool, body: string}\ \\ + \<^bold>\type\ \node_results =\ \\ + \quad~~\{status: node_status, messages: [message], exports: [export]}\ \\ \<^bold>\type\ \use_theories_results =\ \\ \quad\{ok: bool,\ \\ \quad~~\errors: [message],\ \\ - \quad~~\nodes: [node \ {status: node_status, messages: [message]}]}\ \\ + \quad~~\nodes: [node \ node_results]}\ \\ \end{tabular} \<^medskip> @@ -916,6 +920,14 @@ invocations of \<^verbatim>\use_theories\ are idempotent: it could make sense to do that with different values for \pretty_margin\ or \unicode_symbols\ to get different formatting for \errors\ or \messages\. + + The \exports\ can be arbitrary binary resources produced by a theory. An + \export\ \name\ roughly follows file-system standards: ``\<^verbatim>\/\'' separated + list of base names (excluding special names like ``\<^verbatim>\.\'' or ``\<^verbatim>\..\''). The + \base64\ field specifies the format of the \body\ 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>\java.util.Base64.getDecoder.decode(String)\. \ diff -r b2d84b1114fa -r 3687109009c4 src/Pure/General/bytes.scala --- 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 diff -r b2d84b1114fa -r 3687109009c4 src/Pure/PIDE/command.scala --- 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 } - } + } } diff -r b2d84b1114fa -r 3687109009c4 src/Pure/PIDE/document.scala --- 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) diff -r b2d84b1114fa -r 3687109009c4 src/Pure/PIDE/markup.ML --- 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)]; diff -r b2d84b1114fa -r 3687109009c4 src/Pure/PIDE/markup.scala --- 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 } } diff -r b2d84b1114fa -r 3687109009c4 src/Pure/PIDE/session.scala --- 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) diff -r b2d84b1114fa -r 3687109009c4 src/Pure/Thy/export.ML --- 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; diff -r b2d84b1114fa -r 3687109009c4 src/Pure/Thy/export.scala --- 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] = { diff -r b2d84b1114fa -r 3687109009c4 src/Pure/Thy/thy_resources.scala --- 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]( diff -r b2d84b1114fa -r 3687109009c4 src/Pure/Tools/server_commands.scala --- 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) }