store exports within PIDE command state;
authorwenzelm
Mon May 07 17:11:01 2018 +0200 (13 months ago)
changeset 681010699a0bacc50
parent 68097 5f3cffe16311
child 68102 813b5d0904c6
store exports within PIDE command state;
Markup.Export.unapply: proper NAME;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/export.ML
src/Pure/Thy/export.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sun May 06 23:59:14 2018 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Mon May 07 17:11:01 2018 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4    object Results
     1.5    {
     1.6      type Entry = (Long, XML.Tree)
     1.7 -    val empty = new Results(SortedMap.empty)
     1.8 +    val empty: Results = new Results(SortedMap.empty)
     1.9      def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
    1.10      def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
    1.11  
    1.12 @@ -68,7 +68,39 @@
    1.13    }
    1.14  
    1.15  
    1.16 -  /* markup */
    1.17 +  /* exports */
    1.18 +
    1.19 +  object Exports
    1.20 +  {
    1.21 +    type Entry = (Long, Export.Entry)
    1.22 +    val empty: Exports = new Exports(SortedMap.empty)
    1.23 +    def merge(args: TraversableOnce[Exports]): Exports = (empty /: args)(_ ++ _)
    1.24 +  }
    1.25 +
    1.26 +  final class Exports private(private val rep: SortedMap[Long, Export.Entry])
    1.27 +  {
    1.28 +    def iterator: Iterator[Exports.Entry] = rep.iterator
    1.29 +
    1.30 +    def + (entry: Exports.Entry): Exports =
    1.31 +      if (rep.isDefinedAt(entry._1)) this
    1.32 +      else new Exports(rep + entry)
    1.33 +
    1.34 +    def ++ (other: Exports): Exports =
    1.35 +      if (this eq other) this
    1.36 +      else if (rep.isEmpty) other
    1.37 +      else (this /: other.iterator)(_ + _)
    1.38 +
    1.39 +    override def hashCode: Int = rep.hashCode
    1.40 +    override def equals(that: Any): Boolean =
    1.41 +      that match {
    1.42 +        case other: Exports => rep == other.rep
    1.43 +        case _ => false
    1.44 +      }
    1.45 +    override def toString: String = iterator.mkString("Exports(", ", ", ")")
    1.46 +  }
    1.47 +
    1.48 +
    1.49 +  /* markups */
    1.50  
    1.51    object Markup_Index
    1.52    {
    1.53 @@ -175,6 +207,9 @@
    1.54      def merge_results(states: List[State]): Results =
    1.55        Results.merge(states.map(_.results))
    1.56  
    1.57 +    def merge_exports(states: List[State]): Exports =
    1.58 +      Exports.merge(states.map(_.exports))
    1.59 +
    1.60      def merge_markups(states: List[State]): Markups =
    1.61        Markups.merge(states.map(_.markups))
    1.62  
    1.63 @@ -183,7 +218,8 @@
    1.64        Markup_Tree.merge(states.map(_.markup(index)), range, elements)
    1.65  
    1.66      def merge(command: Command, states: List[State]): State =
    1.67 -      State(command, states.flatMap(_.status), merge_results(states), merge_markups(states))
    1.68 +      State(command, states.flatMap(_.status), merge_results(states),
    1.69 +        merge_exports(states), merge_markups(states))
    1.70  
    1.71  
    1.72      /* XML data representation */
    1.73 @@ -213,7 +249,7 @@
    1.74        val blobs_info: Blobs_Info =
    1.75          (blobs_names.map(name => Exn.Res((node_name(name), None)): Blob), blobs_index)
    1.76        val command = Command(id, node_name(node), blobs_info, span)
    1.77 -      State(command, status, results, markups)
    1.78 +      State(command, status, results, Exports.empty, markups)
    1.79      }
    1.80    }
    1.81  
    1.82 @@ -221,6 +257,7 @@
    1.83      command: Command,
    1.84      status: List[Markup] = Nil,
    1.85      results: Results = Results.empty,
    1.86 +    exports: Exports = Exports.empty,
    1.87      markups: Markups = Markups.empty)
    1.88    {
    1.89      lazy val consolidated: Boolean =
    1.90 @@ -245,7 +282,7 @@
    1.91      {
    1.92        val markups1 = markups.redirect(other_command.id)
    1.93        if (markups1.is_empty) None
    1.94 -      else Some(new State(other_command, Nil, Results.empty, markups1))
    1.95 +      else Some(new State(other_command, markups = markups1))
    1.96      }
    1.97  
    1.98      private def add_status(st: Markup): State =
    1.99 @@ -254,6 +291,9 @@
   1.100      private def add_result(entry: Results.Entry): State =
   1.101        copy(results = results + entry)
   1.102  
   1.103 +    def add_export(entry: Exports.Entry): State =
   1.104 +      copy(exports = exports + entry)
   1.105 +
   1.106      private def add_markup(
   1.107        status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State =
   1.108      {
   1.109 @@ -342,7 +382,7 @@
   1.110                Output.warning("Ignored message without serial number: " + message)
   1.111                this
   1.112            }
   1.113 -    }
   1.114 +      }
   1.115    }
   1.116  
   1.117  
     2.1 --- a/src/Pure/PIDE/document.scala	Sun May 06 23:59:14 2018 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Mon May 07 17:11:01 2018 +0200
     2.3 @@ -721,6 +721,22 @@
     2.4        }
     2.5      }
     2.6  
     2.7 +    def add_export(id: Document_ID.Generic, entry: Command.Exports.Entry): (Command.State, State) =
     2.8 +    {
     2.9 +      execs.get(id) match {
    2.10 +        case Some(st) =>
    2.11 +          val new_st = st.add_export(entry)
    2.12 +          (new_st, copy(execs = execs + (id -> new_st)))
    2.13 +        case None =>
    2.14 +          commands.get(id) match {
    2.15 +            case Some(st) =>
    2.16 +              val new_st = st.add_export(entry)
    2.17 +              (new_st, copy(commands = commands + (id -> new_st)))
    2.18 +            case None => fail
    2.19 +          }
    2.20 +      }
    2.21 +    }
    2.22 +
    2.23      def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
    2.24      {
    2.25        val version = the_version(id)
     3.1 --- a/src/Pure/PIDE/markup.ML	Sun May 06 23:59:14 2018 +0100
     3.2 +++ b/src/Pure/PIDE/markup.ML	Mon May 07 17:11:01 2018 +0200
     3.3 @@ -203,7 +203,8 @@
     3.4    val command_timing: Properties.entry
     3.5    val theory_timing: Properties.entry
     3.6    val exportN: string
     3.7 -  type export_args = {id: string option, theory_name: string, name: string, compress: bool}
     3.8 +  type export_args =
     3.9 +    {id: string option, serial: serial, theory_name: string, name: string, compress: bool}
    3.10    val export: export_args -> Properties.T
    3.11    val loading_theory: string -> Properties.T
    3.12    val dest_loading_theory: Properties.T -> string option
    3.13 @@ -642,9 +643,10 @@
    3.14  val theory_timing = (functionN, "theory_timing");
    3.15  
    3.16  val exportN = "export";
    3.17 -type export_args = {id: string option, theory_name: string, name: string, compress: bool}
    3.18 -fun export ({id, theory_name, name, compress}: export_args) =
    3.19 -  [(functionN, exportN), (idN, the_default "" id),
    3.20 +type export_args =
    3.21 +  {id: string option, serial: serial, theory_name: string, name: string, compress: bool}
    3.22 +fun export ({id, serial, theory_name, name, compress}: export_args) =
    3.23 +  [(functionN, exportN), (idN, the_default "" id), (serialN, Value.print_int serial),
    3.24      ("theory_name", theory_name), (nameN, name), ("compress", Value.print_bool compress)];
    3.25  
    3.26  fun loading_theory name = [("function", "loading_theory"), ("name", name)];
     4.1 --- a/src/Pure/PIDE/markup.scala	Sun May 06 23:59:14 2018 +0100
     4.2 +++ b/src/Pure/PIDE/markup.scala	Mon May 07 17:11:01 2018 +0200
     4.3 @@ -571,7 +571,8 @@
     4.4    val EXPORT = "export"
     4.5    object Export
     4.6    {
     4.7 -    sealed case class Args(id: Option[String], theory_name: String, name: String, compress: Boolean)
     4.8 +    sealed case class Args(
     4.9 +      id: Option[String], serial: Long, theory_name: String, name: String, compress: Boolean)
    4.10  
    4.11      val THEORY_NAME = "theory_name"
    4.12      val COMPRESS = "compress"
    4.13 @@ -579,16 +580,26 @@
    4.14      def dest_inline(props: Properties.T): Option[(Args, Bytes)] =
    4.15        props match {
    4.16          case
    4.17 -          List((THEORY_NAME, theory_name), (NAME, name), (COMPRESS, Value.Boolean(compress)),
    4.18 -            (EXPORT, hex)) => Some((Args(None, theory_name, name, compress), Bytes.hex(hex)))
    4.19 +          List(
    4.20 +            (SERIAL, Value.Long(serial)),
    4.21 +            (THEORY_NAME, theory_name),
    4.22 +            (NAME, name),
    4.23 +            (COMPRESS, Value.Boolean(compress)),
    4.24 +            (EXPORT, hex)) =>
    4.25 +          Some((Args(None, serial, theory_name, name, compress), Bytes.hex(hex)))
    4.26          case _ => None
    4.27        }
    4.28  
    4.29      def unapply(props: Properties.T): Option[Args] =
    4.30        props match {
    4.31 -        case List((FUNCTION, EXPORT), (ID, id),
    4.32 -          (THEORY_NAME, theory_name), (PATH, name), (COMPRESS, Value.Boolean(compress))) =>
    4.33 -            Some(Args(proper_string(id), theory_name, name, compress))
    4.34 +        case List(
    4.35 +            (FUNCTION, EXPORT),
    4.36 +            (ID, id),
    4.37 +            (SERIAL, Value.Long(serial)),
    4.38 +            (THEORY_NAME, theory_name),
    4.39 +            (NAME, name),
    4.40 +            (COMPRESS, Value.Boolean(compress))) =>
    4.41 +          Some(Args(proper_string(id), serial, theory_name, name, compress))
    4.42          case _ => None
    4.43        }
    4.44    }
     5.1 --- a/src/Pure/PIDE/session.scala	Sun May 06 23:59:14 2018 +0100
     5.2 +++ b/src/Pure/PIDE/session.scala	Mon May 07 17:11:01 2018 +0200
     5.3 @@ -191,6 +191,7 @@
     5.4    private case object Stop
     5.5    private case class Cancel_Exec(exec_id: Document_ID.Exec)
     5.6    private case class Protocol_Command(name: String, args: List[String])
     5.7 +  private case class Add_Export(args: Markup.Export.Args, bytes: Bytes, output: Prover.Output)
     5.8    private case class Update_Options(options: Options)
     5.9    private case object Consolidate_Execution
    5.10    private case object Prune_History
    5.11 @@ -400,25 +401,26 @@
    5.12  
    5.13      /* prover output */
    5.14  
    5.15 +    def bad_output(output: Prover.Output)
    5.16 +    {
    5.17 +      if (verbose)
    5.18 +        Output.warning("Ignoring bad prover output: " + output.message.toString)
    5.19 +    }
    5.20 +
    5.21 +    def change_command(f: Document.State => (Command.State, Document.State), output: Prover.Output)
    5.22 +    {
    5.23 +      try {
    5.24 +        val st = global_state.change_result(f)
    5.25 +        change_buffer.invoke(false, List(st.command))
    5.26 +      }
    5.27 +      catch { case _: Document.State.Fail => bad_output(output) }
    5.28 +    }
    5.29 +
    5.30      def handle_output(output: Prover.Output)
    5.31      //{{{
    5.32      {
    5.33 -      def bad_output()
    5.34 -      {
    5.35 -        if (verbose)
    5.36 -          Output.warning("Ignoring bad prover output: " + output.message.toString)
    5.37 -      }
    5.38 -
    5.39 -      def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
    5.40 -      {
    5.41 -        try {
    5.42 -          val st = global_state.change_result(_.accumulate(state_id, message, xml_cache))
    5.43 -          change_buffer.invoke(false, List(st.command))
    5.44 -        }
    5.45 -        catch {
    5.46 -          case _: Document.State.Fail => bad_output()
    5.47 -        }
    5.48 -      }
    5.49 +      def accumulate(state_id: Document_ID.Generic, message: XML.Elem): Unit =
    5.50 +        change_command(_.accumulate(state_id, message, xml_cache), output)
    5.51  
    5.52        output match {
    5.53          case msg: Prover.Protocol_Output =>
    5.54 @@ -435,8 +437,12 @@
    5.55                case Protocol.Theory_Timing(_, _) =>
    5.56                  // FIXME
    5.57  
    5.58 -              case Markup.Export(_) =>
    5.59 -                // FIXME
    5.60 +              case Markup.Export(args)
    5.61 +              if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
    5.62 +                if (args.compress) {
    5.63 +                  Future.fork { manager.send(Add_Export(args, msg.bytes.compress(), output)) }
    5.64 +                }
    5.65 +                else manager.send(Add_Export(args, msg.bytes, output))
    5.66  
    5.67                case Markup.Assign_Update =>
    5.68                  msg.text match {
    5.69 @@ -446,8 +452,8 @@
    5.70                        change_buffer.invoke(true, cmds)
    5.71                        manager.send(Session.Change_Flush)
    5.72                      }
    5.73 -                    catch { case _: Document.State.Fail => bad_output() }
    5.74 -                  case _ => bad_output()
    5.75 +                    catch { case _: Document.State.Fail => bad_output(output) }
    5.76 +                  case _ => bad_output(output)
    5.77                  }
    5.78                  delay_prune.invoke()
    5.79  
    5.80 @@ -458,8 +464,8 @@
    5.81                        global_state.change(_.removed_versions(removed))
    5.82                        manager.send(Session.Change_Flush)
    5.83                      }
    5.84 -                    catch { case _: Document.State.Fail => bad_output() }
    5.85 -                  case _ => bad_output()
    5.86 +                    catch { case _: Document.State.Fail => bad_output(output) }
    5.87 +                  case _ => bad_output(output)
    5.88                  }
    5.89  
    5.90                case Markup.ML_Statistics(props) =>
    5.91 @@ -468,7 +474,7 @@
    5.92                case Markup.Task_Statistics(props) =>
    5.93                  // FIXME
    5.94  
    5.95 -              case _ => bad_output()
    5.96 +              case _ => bad_output(output)
    5.97              }
    5.98            }
    5.99          case _ =>
   5.100 @@ -556,6 +562,11 @@
   5.101            case Protocol_Command(name, args) if prover.defined =>
   5.102              prover.get.protocol_command(name, args:_*)
   5.103  
   5.104 +          case Add_Export(args, bytes, output) =>
   5.105 +            val id = Value.Long.parse(args.id.get)
   5.106 +            val entry = (args.serial, Export.make_entry("", args, bytes))
   5.107 +            change_command(_.add_export(id, entry), output)
   5.108 +
   5.109            case change: Session.Change if prover.defined =>
   5.110              val state = global_state.value
   5.111              if (!state.removing_versions && state.is_assigned(change.previous))
     6.1 --- a/src/Pure/Thy/export.ML	Sun May 06 23:59:14 2018 +0100
     6.2 +++ b/src/Pure/Thy/export.ML	Mon May 07 17:11:01 2018 +0200
     6.3 @@ -16,6 +16,7 @@
     6.4  fun gen_export compress thy name output =
     6.5    (Output.try_protocol_message o Markup.export)
     6.6     {id = Position.get_id (Position.thread_data ()),
     6.7 +    serial = serial (),
     6.8      theory_name = Context.theory_long_name thy,
     6.9      name = name,
    6.10      compress = compress} [output];
     7.1 --- a/src/Pure/Thy/export.scala	Sun May 06 23:59:14 2018 +0100
     7.2 +++ b/src/Pure/Thy/export.scala	Mon May 07 17:11:01 2018 +0200
     7.3 @@ -58,6 +58,12 @@
     7.4      }
     7.5    }
     7.6  
     7.7 +  def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry =
     7.8 +  {
     7.9 +    val bytes = if (args.compress) body.compress() else body
    7.10 +    Entry(session_name, args.theory_name, args.name, args.compress, bytes)
    7.11 +  }
    7.12 +
    7.13    def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry =
    7.14    {
    7.15      val select =
    7.16 @@ -104,9 +110,9 @@
    7.17      {
    7.18        consumer.send(
    7.19          if (args.compress)
    7.20 -          Future.fork(Entry(session_name, args.theory_name, args.name, true, body.compress()))
    7.21 +          Future.fork(make_entry(session_name, args, body))
    7.22          else
    7.23 -          Future.value(Entry(session_name, args.theory_name, args.name, false, body)))
    7.24 +          Future.value(make_entry(session_name, args, body)))
    7.25      }
    7.26  
    7.27      def shutdown(close: Boolean = false): List[String] =