src/Pure/PIDE/session.scala
author wenzelm
Sun May 19 18:10:45 2019 +0200 (5 months ago)
changeset 70284 3e17c3a5fd39
parent 69640 af09cc4792dc
child 70625 1ae987cc052f
permissions -rw-r--r--
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
     1 /*  Title:      Pure/PIDE/session.scala
     2     Author:     Makarius
     3     Options:    :folding=explicit:
     4 
     5 PIDE editor session, potentially with running prover process.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import scala.collection.immutable.Queue
    12 import scala.annotation.tailrec
    13 
    14 
    15 object Session
    16 {
    17   /* outlets */
    18 
    19   object Consumer
    20   {
    21     def apply[A](name: String)(consume: A => Unit): Consumer[A] =
    22       new Consumer[A](name, consume)
    23   }
    24   final class Consumer[-A] private(val name: String, val consume: A => Unit)
    25 
    26   class Outlet[A](dispatcher: Consumer_Thread[() => Unit])
    27   {
    28     private val consumers = Synchronized[List[Consumer[A]]](Nil)
    29 
    30     def += (c: Consumer[A]) { consumers.change(Library.update(c)) }
    31     def -= (c: Consumer[A]) { consumers.change(Library.remove(c)) }
    32 
    33     def post(a: A)
    34     {
    35       for (c <- consumers.value.iterator) {
    36         dispatcher.send(() =>
    37           try { c.consume(a) }
    38           catch {
    39             case exn: Throwable =>
    40               Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
    41           })
    42       }
    43     }
    44   }
    45 
    46 
    47   /* change */
    48 
    49   sealed case class Change(
    50     previous: Document.Version,
    51     syntax_changed: List[Document.Node.Name],
    52     deps_changed: Boolean,
    53     doc_edits: List[Document.Edit_Command],
    54     consolidate: List[Document.Node.Name],
    55     version: Document.Version)
    56 
    57   case object Change_Flush
    58 
    59 
    60   /* events */
    61 
    62   //{{{
    63   case class Statistics(props: Properties.T)
    64   case class Global_Options(options: Options)
    65   case object Caret_Focus
    66   case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
    67   case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
    68   case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
    69   case class Commands_Changed(
    70     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
    71 
    72   sealed abstract class Phase
    73   {
    74     def print: String =
    75       this match {
    76         case Terminated(result) => if (result.ok) "finished" else "failed"
    77         case _ => Word.lowercase(this.toString)
    78       }
    79   }
    80   case object Inactive extends Phase  // stable
    81   case object Startup extends Phase  // transient
    82   case object Ready extends Phase  // metastable
    83   case object Shutdown extends Phase  // transient
    84   case class Terminated(result: Process_Result) extends Phase  // stable
    85   //}}}
    86 
    87 
    88   /* syslog */
    89 
    90   private[Session] class Syslog(limit: Int)
    91   {
    92     private var queue = Queue.empty[XML.Elem]
    93     private var length = 0
    94 
    95     def += (msg: XML.Elem): Unit = synchronized {
    96       queue = queue.enqueue(msg)
    97       length += 1
    98       if (length > limit) queue = queue.dequeue._2
    99     }
   100 
   101     def content: String = synchronized {
   102       cat_lines(queue.iterator.map(XML.content)) +
   103       (if (length > limit) "\n(A total of " + length + " messages...)" else "")
   104     }
   105   }
   106 
   107 
   108   /* protocol handlers */
   109 
   110   abstract class Protocol_Handler
   111   {
   112     def init(session: Session): Unit = {}
   113     def exit(): Unit = {}
   114     val functions: List[(String, Prover.Protocol_Output => Boolean)]
   115   }
   116 }
   117 
   118 
   119 class Session(_session_options: => Options, val resources: Resources) extends Document.Session
   120 {
   121   session =>
   122 
   123   val xml_cache: XML.Cache = XML.make_cache()
   124   val xz_cache: XZ.Cache = XZ.make_cache()
   125 
   126 
   127   /* global flags */
   128 
   129   @volatile var timing: Boolean = false
   130   @volatile var verbose: Boolean = false
   131 
   132 
   133   /* dynamic session options */
   134 
   135   def session_options: Options = _session_options
   136 
   137   def output_delay: Time = session_options.seconds("editor_output_delay")
   138   def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay")
   139   def prune_delay: Time = session_options.seconds("editor_prune_delay")
   140   def prune_size: Int = session_options.int("editor_prune_size")
   141   def syslog_limit: Int = session_options.int("editor_syslog_limit")
   142   def reparse_limit: Int = session_options.int("editor_reparse_limit")
   143 
   144 
   145   /* dispatcher */
   146 
   147   private val dispatcher =
   148     Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true }
   149 
   150   def assert_dispatcher[A](body: => A): A =
   151   {
   152     assert(dispatcher.check_thread)
   153     body
   154   }
   155 
   156   def require_dispatcher[A](body: => A): A =
   157   {
   158     require(dispatcher.check_thread)
   159     body
   160   }
   161 
   162   def send_dispatcher(body: => Unit): Unit =
   163   {
   164     if (dispatcher.check_thread) body
   165     else dispatcher.send(() => body)
   166   }
   167 
   168   def send_wait_dispatcher(body: => Unit): Unit =
   169   {
   170     if (dispatcher.check_thread) body
   171     else dispatcher.send_wait(() => body)
   172   }
   173 
   174 
   175   /* outlets */
   176 
   177   val statistics = new Session.Outlet[Session.Statistics](dispatcher)
   178   val global_options = new Session.Outlet[Session.Global_Options](dispatcher)
   179   val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher)
   180   val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher)
   181   val commands_changed = new Session.Outlet[Session.Commands_Changed](dispatcher)
   182   val phase_changed = new Session.Outlet[Session.Phase](dispatcher)
   183   val syslog_messages = new Session.Outlet[Prover.Output](dispatcher)
   184   val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher)
   185   val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher)
   186   val debugger_updates = new Session.Outlet[Debugger.Update.type](dispatcher)
   187 
   188   val all_messages = new Session.Outlet[Prover.Message](dispatcher)  // potential bottle-neck!
   189 
   190 
   191   /** main protocol manager **/
   192 
   193   /* internal messages */
   194 
   195   private case class Start(start_prover: Prover.Receiver => Prover)
   196   private case object Stop
   197   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   198   private case class Protocol_Command(name: String, args: List[String])
   199   private case class Update_Options(options: Options)
   200   private case object Consolidate_Execution
   201   private case object Prune_History
   202 
   203 
   204   /* phase */
   205 
   206   private def post_phase(new_phase: Session.Phase): Session.Phase =
   207   {
   208     phase_changed.post(new_phase)
   209     new_phase
   210   }
   211   private val _phase = Synchronized[Session.Phase](Session.Inactive)
   212   private def phase_=(new_phase: Session.Phase): Unit = _phase.change(_ => post_phase(new_phase))
   213 
   214   def phase = _phase.value
   215   def is_ready: Boolean = phase == Session.Ready
   216 
   217 
   218   /* global state */
   219 
   220   private val syslog = new Session.Syslog(syslog_limit)
   221   def syslog_content(): String = syslog.content
   222 
   223   private val global_state = Synchronized(Document.State.init)
   224   def current_state(): Document.State = global_state.value
   225 
   226   def recent_syntax(name: Document.Node.Name): Outer_Syntax =
   227     global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
   228     resources.session_base.overall_syntax
   229 
   230 
   231   /* pipelined change parsing */
   232 
   233   private case class Text_Edits(
   234     previous: Future[Document.Version],
   235     doc_blobs: Document.Blobs,
   236     text_edits: List[Document.Edit_Text],
   237     consolidate: List[Document.Node.Name],
   238     version_result: Promise[Document.Version])
   239 
   240   private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
   241   {
   242     case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) =>
   243       val prev = previous.get_finished
   244       val change =
   245         Timing.timeit("parse_change", timing) {
   246           resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate)
   247         }
   248       version_result.fulfill(change.version)
   249       manager.send(change)
   250       true
   251   }
   252 
   253 
   254   /* buffered changes */
   255 
   256   private object change_buffer
   257   {
   258     private var assignment: Boolean = false
   259     private var nodes: Set[Document.Node.Name] = Set.empty
   260     private var commands: Set[Command] = Set.empty
   261 
   262     def flush(): Unit = synchronized {
   263       if (assignment || nodes.nonEmpty || commands.nonEmpty)
   264         commands_changed.post(Session.Commands_Changed(assignment, nodes, commands))
   265       if (nodes.nonEmpty) consolidation.update(nodes)
   266       assignment = false
   267       nodes = Set.empty
   268       commands = Set.empty
   269     }
   270     private val delay_flush = Standard_Thread.delay_first(output_delay) { flush() }
   271 
   272     def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit =
   273       synchronized {
   274         assignment |= assign
   275         for (node <- edited_nodes) {
   276           nodes += node
   277         }
   278         for (command <- cmds) {
   279           nodes += command.node_name
   280           command.blobs_names.foreach(nodes += _)
   281           commands += command
   282         }
   283         delay_flush.invoke()
   284       }
   285 
   286     def shutdown()
   287     {
   288       delay_flush.revoke()
   289       flush()
   290     }
   291   }
   292 
   293 
   294   /* postponed changes */
   295 
   296   private object postponed_changes
   297   {
   298     private var postponed: List[Session.Change] = Nil
   299 
   300     def store(change: Session.Change): Unit = synchronized { postponed ::= change }
   301 
   302     def flush(state: Document.State): List[Session.Change] = synchronized {
   303       val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous))
   304       postponed = unassigned
   305       assigned.reverse
   306     }
   307   }
   308 
   309 
   310   /* node consolidation */
   311 
   312   private object consolidation
   313   {
   314     private val delay =
   315       Standard_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) }
   316 
   317     private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty)
   318     private val state = Synchronized(init_state)
   319 
   320     def exit()
   321     {
   322       delay.revoke()
   323       state.change(_ => None)
   324     }
   325 
   326     def update(new_nodes: Set[Document.Node.Name] = Set.empty)
   327     {
   328       val active =
   329         state.change_result(st =>
   330           (st.isDefined, st.map(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes)))
   331       if (active) delay.invoke()
   332     }
   333 
   334     def flush(): Set[Document.Node.Name] =
   335       state.change_result(st => if (st.isDefined) (st.get, init_state) else (Set.empty, None))
   336   }
   337 
   338 
   339   /* prover process */
   340 
   341   private object prover
   342   {
   343     private val variable = Synchronized[Option[Prover]](None)
   344 
   345     def defined: Boolean = variable.value.isDefined
   346     def get: Prover = variable.value.get
   347     def set(p: Prover) { variable.change(_ => Some(p)) }
   348     def reset { variable.change(_ => None) }
   349     def await_reset() { variable.guarded_access({ case None => Some((), None) case _ => None }) }
   350   }
   351 
   352 
   353   /* file formats */
   354 
   355   lazy val file_formats: File_Format.Session =
   356     resources.file_formats.start_session(session)
   357 
   358 
   359   /* protocol handlers */
   360 
   361   private val protocol_handlers = Protocol_Handlers.init(session)
   362 
   363   def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
   364     protocol_handlers.get(name)
   365 
   366   def init_protocol_handler(handler: Session.Protocol_Handler): Unit =
   367     protocol_handlers.init(handler)
   368 
   369   def init_protocol_handler(name: String): Unit =
   370     protocol_handlers.init(name)
   371 
   372 
   373   /* debugger */
   374 
   375   private val debugger_handler = new Debugger.Handler(this)
   376   init_protocol_handler(debugger_handler)
   377 
   378   def debugger: Debugger = debugger_handler.debugger
   379 
   380 
   381   /* manager thread */
   382 
   383   private val delay_prune =
   384     Standard_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
   385 
   386   private val manager: Consumer_Thread[Any] =
   387   {
   388     /* raw edits */
   389 
   390     def handle_raw_edits(
   391       doc_blobs: Document.Blobs = Document.Blobs.empty,
   392       edits: List[Document.Edit_Text] = Nil,
   393       consolidate: List[Document.Node.Name] = Nil)
   394     //{{{
   395     {
   396       require(prover.defined)
   397 
   398       prover.get.discontinue_execution()
   399 
   400       val previous = global_state.value.history.tip.version
   401       val version = Future.promise[Document.Version]
   402       global_state.change(_.continue_history(previous, edits, version))
   403 
   404       raw_edits.post(Session.Raw_Edits(doc_blobs, edits))
   405       change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version))
   406     }
   407     //}}}
   408 
   409 
   410     /* resulting changes */
   411 
   412     def handle_change(change: Session.Change)
   413     //{{{
   414     {
   415       require(prover.defined)
   416 
   417       def id_command(command: Command)
   418       {
   419         for {
   420           (name, digest) <- command.blobs_defined
   421           if !global_state.value.defined_blob(digest)
   422         } {
   423           change.version.nodes(name).get_blob match {
   424             case Some(blob) =>
   425               global_state.change(_.define_blob(digest))
   426               prover.get.define_blob(digest, blob.bytes)
   427             case None =>
   428               Output.error_message("Missing blob " + quote(name.toString))
   429           }
   430         }
   431 
   432         if (!global_state.value.defined_command(command.id)) {
   433           global_state.change(_.define_command(command))
   434           prover.get.define_command(command)
   435         }
   436       }
   437       for { (_, edit) <- change.doc_edits } {
   438         edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) })
   439       }
   440 
   441       val assignment = global_state.value.the_assignment(change.previous).check_finished
   442       global_state.change(_.define_version(change.version, assignment))
   443       prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate)
   444       resources.commit(change)
   445     }
   446     //}}}
   447 
   448 
   449     /* prover output */
   450 
   451     def handle_output(output: Prover.Output)
   452     //{{{
   453     {
   454       def bad_output()
   455       {
   456         if (verbose)
   457           Output.warning("Ignoring bad prover output: " + output.message.toString)
   458       }
   459 
   460       def change_command(f: Document.State => (Command.State, Document.State))
   461       {
   462         try {
   463           val st = global_state.change_result(f)
   464           change_buffer.invoke(false, Nil, List(st.command))
   465         }
   466         catch { case _: Document.State.Fail => bad_output() }
   467       }
   468 
   469       output match {
   470         case msg: Prover.Protocol_Output =>
   471           val handled = protocol_handlers.invoke(msg)
   472           if (!handled) {
   473             msg.properties match {
   474               case Markup.Protocol_Handler(name) if prover.defined =>
   475                 init_protocol_handler(name)
   476 
   477               case Protocol.Command_Timing(state_id, timing) if prover.defined =>
   478                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
   479                 change_command(_.accumulate(state_id, xml_cache.elem(message), xml_cache))
   480 
   481               case Protocol.Theory_Timing(_, _) =>
   482                 // FIXME
   483 
   484               case Markup.Export(args)
   485               if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
   486                 val id = Value.Long.unapply(args.id.get).get
   487                 val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
   488                 change_command(_.add_export(id, (args.serial, export)))
   489 
   490               case Markup.Assign_Update =>
   491                 msg.text match {
   492                   case Protocol.Assign_Update(id, edited, update) =>
   493                     try {
   494                       val (edited_nodes, cmds) =
   495                         global_state.change_result(_.assign(id, edited, update))
   496                       change_buffer.invoke(true, edited_nodes, cmds)
   497                       manager.send(Session.Change_Flush)
   498                     }
   499                     catch { case _: Document.State.Fail => bad_output() }
   500                   case _ => bad_output()
   501                 }
   502                 delay_prune.invoke()
   503 
   504               case Markup.Removed_Versions =>
   505                 msg.text match {
   506                   case Protocol.Removed(removed) =>
   507                     try {
   508                       global_state.change(_.removed_versions(removed))
   509                       manager.send(Session.Change_Flush)
   510                     }
   511                     catch { case _: Document.State.Fail => bad_output() }
   512                   case _ => bad_output()
   513                 }
   514 
   515               case Markup.ML_Statistics(props) =>
   516                 statistics.post(Session.Statistics(props))
   517 
   518               case Markup.Task_Statistics(props) =>
   519                 // FIXME
   520 
   521               case _ => bad_output()
   522             }
   523           }
   524         case _ =>
   525           output.properties match {
   526             case Position.Id(state_id) =>
   527               change_command(_.accumulate(state_id, output.message, xml_cache))
   528 
   529             case _ if output.is_init =>
   530               prover.get.options(file_formats.prover_options(session_options))
   531               prover.get.session_base(resources)
   532               phase = Session.Ready
   533               debugger.ready()
   534 
   535             case Markup.Process_Result(result) if output.is_exit =>
   536               file_formats.stop_session
   537               phase = Session.Terminated(result)
   538               prover.reset
   539 
   540             case _ =>
   541               raw_output_messages.post(output)
   542           }
   543         }
   544     }
   545     //}}}
   546 
   547 
   548     /* main thread */
   549 
   550     Consumer_Thread.fork[Any]("Session.manager", daemon = true)
   551     {
   552       case arg: Any =>
   553         //{{{
   554         arg match {
   555           case output: Prover.Output =>
   556             if (output.is_stdout || output.is_stderr)
   557               raw_output_messages.post(output)
   558             else handle_output(output)
   559 
   560             if (output.is_syslog) {
   561               syslog += output.message
   562               syslog_messages.post(output)
   563             }
   564 
   565             all_messages.post(output)
   566 
   567           case input: Prover.Input =>
   568             all_messages.post(input)
   569 
   570           case Start(start_prover) if !prover.defined =>
   571             prover.set(start_prover(manager.send(_)))
   572 
   573           case Stop =>
   574             consolidation.exit()
   575             delay_prune.revoke()
   576             if (prover.defined) {
   577               protocol_handlers.exit()
   578               global_state.change(_ => Document.State.init)
   579               prover.get.terminate
   580             }
   581 
   582           case Consolidate_Execution =>
   583             if (prover.defined) {
   584               val state = global_state.value
   585               state.stable_tip_version match {
   586                 case None => consolidation.update()
   587                 case Some(version) =>
   588                   val consolidate =
   589                     consolidation.flush().iterator.filter(name =>
   590                       !resources.session_base.loaded_theory(name) &&
   591                       !state.node_consolidated(version, name) &&
   592                       state.node_maybe_consolidated(version, name)).toList
   593                   if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate)
   594               }
   595             }
   596 
   597           case Prune_History =>
   598             if (prover.defined) {
   599               val old_versions = global_state.change_result(_.remove_versions(prune_size))
   600               if (old_versions.nonEmpty) prover.get.remove_versions(old_versions)
   601             }
   602 
   603           case Update_Options(options) =>
   604             if (prover.defined && is_ready) {
   605               prover.get.options(file_formats.prover_options(options))
   606               handle_raw_edits()
   607             }
   608             global_options.post(Session.Global_Options(options))
   609 
   610           case Cancel_Exec(exec_id) if prover.defined =>
   611             prover.get.cancel_exec(exec_id)
   612 
   613           case Session.Raw_Edits(doc_blobs, edits) if prover.defined =>
   614             handle_raw_edits(doc_blobs = doc_blobs, edits = edits)
   615 
   616           case Session.Dialog_Result(id, serial, result) if prover.defined =>
   617             prover.get.dialog_result(serial, result)
   618             handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
   619 
   620           case Protocol_Command(name, args) if prover.defined =>
   621             prover.get.protocol_command(name, args:_*)
   622 
   623           case change: Session.Change if prover.defined =>
   624             val state = global_state.value
   625             if (!state.removing_versions && state.is_assigned(change.previous))
   626               handle_change(change)
   627             else postponed_changes.store(change)
   628 
   629           case Session.Change_Flush if prover.defined =>
   630             val state = global_state.value
   631             if (!state.removing_versions)
   632               postponed_changes.flush(state).foreach(handle_change(_))
   633 
   634           case bad =>
   635             if (verbose) Output.warning("Ignoring bad message: " + bad.toString)
   636         }
   637         true
   638         //}}}
   639     }
   640   }
   641 
   642 
   643   /* main operations */
   644 
   645   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
   646       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
   647     global_state.value.snapshot(name, pending_edits)
   648 
   649   @tailrec final def await_stable_snapshot(): Document.Snapshot =
   650   {
   651     val snapshot = this.snapshot()
   652     if (snapshot.is_outdated) {
   653       Thread.sleep(output_delay.ms)
   654       await_stable_snapshot()
   655     }
   656     else snapshot
   657   }
   658 
   659   def start(start_prover: Prover.Receiver => Prover)
   660   {
   661     file_formats
   662     _phase.change(
   663       {
   664         case Session.Inactive =>
   665           manager.send(Start(start_prover))
   666           post_phase(Session.Startup)
   667         case phase => error("Cannot start prover in phase " + quote(phase.print))
   668       })
   669   }
   670 
   671   def send_stop()
   672   {
   673     val was_ready =
   674       _phase.guarded_access(phase =>
   675         phase match {
   676           case Session.Startup | Session.Shutdown => None
   677           case Session.Terminated(_) => Some((false, phase))
   678           case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0)))))
   679           case Session.Ready => Some((true, post_phase(Session.Shutdown)))
   680         })
   681     if (was_ready) manager.send(Stop)
   682   }
   683 
   684   def stop(): Process_Result =
   685   {
   686     send_stop()
   687     prover.await_reset()
   688 
   689     change_parser.shutdown()
   690     change_buffer.shutdown()
   691     manager.shutdown()
   692     dispatcher.shutdown()
   693 
   694     phase match {
   695       case Session.Terminated(result) => result
   696       case phase => error("Bad session phase after shutdown: " + quote(phase.print))
   697     }
   698   }
   699 
   700   def protocol_command(name: String, args: String*)
   701   { manager.send(Protocol_Command(name, args.toList)) }
   702 
   703   def cancel_exec(exec_id: Document_ID.Exec)
   704   { manager.send(Cancel_Exec(exec_id)) }
   705 
   706   def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   707   { if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits)) }
   708 
   709   def update_options(options: Options)
   710   { manager.send_wait(Update_Options(options)) }
   711 
   712   def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
   713   { manager.send(Session.Dialog_Result(id, serial, result)) }
   714 }