# HG changeset patch # User wenzelm # Date 1525705861 -7200 # Node ID 0699a0bacc5023c3378015dc4affcfb4e06360ad # Parent 5f3cffe163119a3342f065493567a6446ef23e5f store exports within PIDE command state; Markup.Export.unapply: proper NAME; diff -r 5f3cffe16311 -r 0699a0bacc50 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sun May 06 23:59:14 2018 +0100 +++ b/src/Pure/PIDE/command.scala Mon May 07 17:11:01 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 5f3cffe16311 -r 0699a0bacc50 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sun May 06 23:59:14 2018 +0100 +++ b/src/Pure/PIDE/document.scala Mon May 07 17:11:01 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 5f3cffe16311 -r 0699a0bacc50 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sun May 06 23:59:14 2018 +0100 +++ b/src/Pure/PIDE/markup.ML Mon May 07 17:11:01 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 5f3cffe16311 -r 0699a0bacc50 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sun May 06 23:59:14 2018 +0100 +++ b/src/Pure/PIDE/markup.scala Mon May 07 17:11:01 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 5f3cffe16311 -r 0699a0bacc50 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Sun May 06 23:59:14 2018 +0100 +++ b/src/Pure/PIDE/session.scala Mon May 07 17:11:01 2018 +0200 @@ -191,6 +191,7 @@ private case object Stop private case class Cancel_Exec(exec_id: Document_ID.Exec) private case class Protocol_Command(name: String, args: List[String]) + private case class Add_Export(args: Markup.Export.Args, bytes: Bytes, output: Prover.Output) private case class Update_Options(options: Options) private case object Consolidate_Execution private case object Prune_History @@ -400,25 +401,26 @@ /* prover output */ + def bad_output(output: Prover.Output) + { + if (verbose) + Output.warning("Ignoring bad prover output: " + output.message.toString) + } + + def change_command(f: Document.State => (Command.State, Document.State), output: Prover.Output) + { + try { + val st = global_state.change_result(f) + change_buffer.invoke(false, List(st.command)) + } + catch { case _: Document.State.Fail => bad_output(output) } + } + def handle_output(output: Prover.Output) //{{{ { - def bad_output() - { - if (verbose) - Output.warning("Ignoring bad prover output: " + output.message.toString) - } - - def accumulate(state_id: Document_ID.Generic, message: XML.Elem) - { - try { - val st = global_state.change_result(_.accumulate(state_id, message, xml_cache)) - change_buffer.invoke(false, List(st.command)) - } - catch { - case _: Document.State.Fail => bad_output() - } - } + def accumulate(state_id: Document_ID.Generic, message: XML.Elem): Unit = + change_command(_.accumulate(state_id, message, xml_cache), output) output match { case msg: Prover.Protocol_Output => @@ -435,8 +437,12 @@ case Protocol.Theory_Timing(_, _) => // FIXME - case Markup.Export(_) => - // FIXME + case Markup.Export(args) + if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined => + if (args.compress) { + Future.fork { manager.send(Add_Export(args, msg.bytes.compress(), output)) } + } + else manager.send(Add_Export(args, msg.bytes, output)) case Markup.Assign_Update => msg.text match { @@ -446,8 +452,8 @@ change_buffer.invoke(true, cmds) manager.send(Session.Change_Flush) } - catch { case _: Document.State.Fail => bad_output() } - case _ => bad_output() + catch { case _: Document.State.Fail => bad_output(output) } + case _ => bad_output(output) } delay_prune.invoke() @@ -458,8 +464,8 @@ global_state.change(_.removed_versions(removed)) manager.send(Session.Change_Flush) } - catch { case _: Document.State.Fail => bad_output() } - case _ => bad_output() + catch { case _: Document.State.Fail => bad_output(output) } + case _ => bad_output(output) } case Markup.ML_Statistics(props) => @@ -468,7 +474,7 @@ case Markup.Task_Statistics(props) => // FIXME - case _ => bad_output() + case _ => bad_output(output) } } case _ => @@ -556,6 +562,11 @@ case Protocol_Command(name, args) if prover.defined => prover.get.protocol_command(name, args:_*) + case Add_Export(args, bytes, output) => + val id = Value.Long.parse(args.id.get) + val entry = (args.serial, Export.make_entry("", args, bytes)) + change_command(_.add_export(id, entry), output) + case change: Session.Change if prover.defined => val state = global_state.value if (!state.removing_versions && state.is_assigned(change.previous)) diff -r 5f3cffe16311 -r 0699a0bacc50 src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Sun May 06 23:59:14 2018 +0100 +++ b/src/Pure/Thy/export.ML Mon May 07 17:11:01 2018 +0200 @@ -16,6 +16,7 @@ fun gen_export compress thy name output = (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]; diff -r 5f3cffe16311 -r 0699a0bacc50 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Sun May 06 23:59:14 2018 +0100 +++ b/src/Pure/Thy/export.scala Mon May 07 17:11:01 2018 +0200 @@ -58,6 +58,12 @@ } } + def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry = + { + val bytes = if (args.compress) body.compress() else body + Entry(session_name, args.theory_name, args.name, args.compress, bytes) + } + def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry = { val select = @@ -104,9 +110,9 @@ { consumer.send( if (args.compress) - Future.fork(Entry(session_name, args.theory_name, args.name, true, body.compress())) + Future.fork(make_entry(session_name, args, body)) else - Future.value(Entry(session_name, args.theory_name, args.name, false, body))) + Future.value(make_entry(session_name, args, body))) } def shutdown(close: Boolean = false): List[String] =