src/Pure/System/session.scala
author wenzelm
Tue Aug 21 12:15:25 2012 +0200 (2012-08-21)
changeset 48870 4accee106f0f
parent 48794 8d2a026e576b
child 48884 963b50ec6d73
permissions -rw-r--r--
clarified initialization of Thy_Load, Thy_Info, Session;
     1 /*  Title:      Pure/System/session.scala
     2     Author:     Makarius
     3     Options:    :folding=explicit:collapseFolds=1:
     4 
     5 Main Isabelle/Scala session, potentially with running prover process.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import java.lang.System
    12 import java.util.{Timer, TimerTask}
    13 
    14 import scala.collection.mutable
    15 import scala.collection.immutable.Queue
    16 import scala.actors.TIMEOUT
    17 import scala.actors.Actor._
    18 
    19 
    20 object Session
    21 {
    22   /* events */
    23 
    24   //{{{
    25   case object Global_Settings
    26   case object Caret_Focus
    27   case class Commands_Changed(
    28     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
    29 
    30   sealed abstract class Phase
    31   case object Inactive extends Phase
    32   case object Startup extends Phase  // transient
    33   case object Failed extends Phase
    34   case object Ready extends Phase
    35   case object Shutdown extends Phase  // transient
    36   //}}}
    37 }
    38 
    39 
    40 class Session(val thy_load: Thy_Load)
    41 {
    42   /* global flags */
    43 
    44   @volatile var timing: Boolean = false
    45   @volatile var verbose: Boolean = false
    46 
    47 
    48   /* tuning parameters */  // FIXME properties or settings (!?)
    49 
    50   val message_delay = Time.seconds(0.01)  // prover messages
    51   val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
    52   val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
    53   val update_delay = Time.seconds(0.5)  // GUI layout updates
    54   val load_delay = Time.seconds(0.5)  // file load operations (new buffers etc.)
    55   val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
    56   val prune_size = 0  // size of retained history
    57   val syslog_limit = 100
    58 
    59 
    60   /* pervasive event buses */
    61 
    62   val global_settings = new Event_Bus[Session.Global_Settings.type]
    63   val caret_focus = new Event_Bus[Session.Caret_Focus.type]
    64   val commands_changed = new Event_Bus[Session.Commands_Changed]
    65   val phase_changed = new Event_Bus[Session.Phase]
    66   val syslog_messages = new Event_Bus[Isabelle_Process.Output]
    67   val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
    68   val all_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
    69 
    70 
    71 
    72   /** buffered command changes (delay_first discipline) **/
    73 
    74   //{{{
    75   private case object Stop
    76 
    77   private val (_, commands_changed_buffer) =
    78     Simple_Thread.actor("commands_changed_buffer", daemon = true)
    79   {
    80     var finished = false
    81     while (!finished) {
    82       receive {
    83         case Stop => finished = true; reply(())
    84         case changed: Session.Commands_Changed => commands_changed.event(changed)
    85         case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad)
    86       }
    87     }
    88   }
    89   //}}}
    90 
    91 
    92   /** pipelined change parsing **/
    93 
    94   //{{{
    95   private case class Text_Edits(
    96     previous: Future[Document.Version],
    97     text_edits: List[Document.Edit_Text],
    98     version_result: Promise[Document.Version])
    99 
   100   private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true)
   101   {
   102     var finished = false
   103     while (!finished) {
   104       receive {
   105         case Stop => finished = true; reply(())
   106 
   107         case Text_Edits(previous, text_edits, version_result) =>
   108           val prev = previous.get_finished
   109           val (doc_edits, version) =
   110             Timing.timeit("Thy_Syntax.text_edits", timing) {
   111               Thy_Syntax.text_edits(thy_load.base_syntax, prev, text_edits)
   112             }
   113           version_result.fulfill(version)
   114           sender ! Change(doc_edits, prev, version)
   115 
   116         case bad => System.err.println("change_parser: ignoring bad message " + bad)
   117       }
   118     }
   119   }
   120   //}}}
   121 
   122 
   123 
   124   /** main protocol actor **/
   125 
   126   /* global state */
   127 
   128   private val syslog = Volatile(Queue.empty[XML.Elem])
   129   def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
   130 
   131   @volatile private var _phase: Session.Phase = Session.Inactive
   132   private def phase_=(new_phase: Session.Phase)
   133   {
   134     _phase = new_phase
   135     phase_changed.event(new_phase)
   136   }
   137   def phase = _phase
   138   def is_ready: Boolean = phase == Session.Ready
   139 
   140   private val global_state = Volatile(Document.State.init)
   141   def current_state(): Document.State = global_state()
   142 
   143   def recent_syntax(): Outer_Syntax =
   144   {
   145     val version = current_state().recent_finished.version.get_finished
   146     if (version.is_init) thy_load.base_syntax
   147     else version.syntax
   148   }
   149   def get_recent_syntax(): Option[Outer_Syntax] =
   150     if (is_ready) Some(recent_syntax)
   151     else None
   152 
   153   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
   154       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
   155     global_state().snapshot(name, pending_edits)
   156 
   157 
   158   /* theory files */
   159 
   160   def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
   161   {
   162     val header1 =
   163       if (thy_load.loaded_theories(name.theory))
   164         header.error("Attempt to update loaded theory " + quote(name.theory))
   165       else header
   166     (name, Document.Node.Deps(header1))
   167   }
   168 
   169 
   170   /* actor messages */
   171 
   172   private case class Start(args: List[String])
   173   private case object Cancel_Execution
   174   private case class Edit(edits: List[Document.Edit_Text])
   175   private case class Change(
   176     doc_edits: List[Document.Edit_Command],
   177     previous: Document.Version,
   178     version: Document.Version)
   179   private case class Messages(msgs: List[Isabelle_Process.Message])
   180 
   181   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   182   {
   183     val this_actor = self
   184 
   185     var prune_next = System.currentTimeMillis() + prune_delay.ms
   186 
   187 
   188     /* buffered prover messages */
   189 
   190     object receiver
   191     {
   192       private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
   193 
   194       def flush(): Unit = synchronized {
   195         if (!buffer.isEmpty) {
   196           val msgs = buffer.toList
   197           this_actor ! Messages(msgs)
   198           buffer = new mutable.ListBuffer[Isabelle_Process.Message]
   199         }
   200       }
   201       def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
   202         buffer += msg
   203         msg match {
   204           case output: Isabelle_Process.Output =>
   205             if (output.is_syslog)
   206               syslog >> (queue =>
   207                 {
   208                   val queue1 = queue.enqueue(output.message)
   209                   if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
   210                 })
   211             if (output.is_protocol) flush()
   212           case _ =>
   213         }
   214       }
   215 
   216       private val timer = new Timer("session_actor.receiver", true)
   217       timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
   218 
   219       def cancel() { timer.cancel() }
   220     }
   221 
   222     var prover: Option[Isabelle_Process with Protocol] = None
   223 
   224 
   225     /* delayed command changes */
   226 
   227     object delay_commands_changed
   228     {
   229       private var changed_assignment: Boolean = false
   230       private var changed_nodes: Set[Document.Node.Name] = Set.empty
   231       private var changed_commands: Set[Command] = Set.empty
   232 
   233       private var flush_time: Option[Long] = None
   234 
   235       def flush_timeout: Long =
   236         flush_time match {
   237           case None => 5000L
   238           case Some(time) => (time - System.currentTimeMillis()) max 0
   239         }
   240 
   241       def flush()
   242       {
   243         if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty)
   244           commands_changed_buffer !
   245             Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands)
   246         changed_assignment = false
   247         changed_nodes = Set.empty
   248         changed_commands = Set.empty
   249         flush_time = None
   250       }
   251 
   252       def invoke(assign: Boolean, commands: List[Command])
   253       {
   254         changed_assignment |= assign
   255         for (command <- commands) {
   256           changed_nodes += command.node_name
   257           changed_commands += command
   258         }
   259         val now = System.currentTimeMillis()
   260         flush_time match {
   261           case None => flush_time = Some(now + output_delay.ms)
   262           case Some(time) => if (now >= time) flush()
   263         }
   264       }
   265     }
   266 
   267 
   268     /* resulting changes */
   269 
   270     def handle_change(change: Change)
   271     //{{{
   272     {
   273       val previous = change.previous
   274       val version = change.version
   275       val doc_edits = change.doc_edits
   276 
   277       def id_command(command: Command)
   278       {
   279         if (!global_state().defined_command(command.id)) {
   280           global_state >> (_.define_command(command))
   281           prover.get.define_command(command)
   282         }
   283       }
   284       doc_edits foreach {
   285         case (_, edit) =>
   286           edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
   287       }
   288 
   289       val assignment = global_state().the_assignment(previous).check_finished
   290       global_state >> (_.define_version(version, assignment))
   291       prover.get.update(previous.id, version.id, doc_edits)
   292     }
   293     //}}}
   294 
   295 
   296     /* prover output */
   297 
   298     def handle_output(output: Isabelle_Process.Output)
   299     //{{{
   300     {
   301       def bad_output(output: Isabelle_Process.Output)
   302       {
   303         if (verbose)
   304           System.err.println("Ignoring prover output: " + output.message.toString)
   305       }
   306 
   307       output.properties match {
   308 
   309         case Position.Id(state_id) if !output.is_protocol =>
   310           try {
   311             val st = global_state >>> (_.accumulate(state_id, output.message))
   312             delay_commands_changed.invoke(false, List(st.command))
   313           }
   314           catch {
   315             case _: Document.State.Fail => bad_output(output)
   316           }
   317 
   318         case Isabelle_Markup.Assign_Execs if output.is_protocol =>
   319           XML.content(output.body).mkString match {
   320             case Protocol.Assign(id, assign) =>
   321               try {
   322                 val cmds = global_state >>> (_.assign(id, assign))
   323                 delay_commands_changed.invoke(true, cmds)
   324               }
   325               catch { case _: Document.State.Fail => bad_output(output) }
   326             case _ => bad_output(output)
   327           }
   328           // FIXME separate timeout event/message!?
   329           if (prover.isDefined && System.currentTimeMillis() > prune_next) {
   330             val old_versions = global_state >>> (_.prune_history(prune_size))
   331             if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
   332             prune_next = System.currentTimeMillis() + prune_delay.ms
   333           }
   334 
   335         case Isabelle_Markup.Removed_Versions if output.is_protocol =>
   336           XML.content(output.body).mkString match {
   337             case Protocol.Removed(removed) =>
   338               try {
   339                 global_state >> (_.removed_versions(removed))
   340               }
   341               catch { case _: Document.State.Fail => bad_output(output) }
   342             case _ => bad_output(output)
   343           }
   344 
   345         case Isabelle_Markup.Invoke_Scala(name, id) if output.is_protocol =>
   346           Future.fork {
   347             val arg = XML.content(output.body).mkString
   348             val (tag, res) = Invoke_Scala.method(name, arg)
   349             prover.get.invoke_scala(id, tag, res)
   350           }
   351 
   352         case Isabelle_Markup.Cancel_Scala(id) if output.is_protocol =>
   353           System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
   354 
   355         case _ if output.is_init =>
   356             phase = Session.Ready
   357 
   358         case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
   359           if (rc == 0) phase = Session.Inactive
   360           else phase = Session.Failed
   361 
   362         case _ if output.is_stdout =>
   363 
   364         case _ => bad_output(output)
   365       }
   366     }
   367     //}}}
   368 
   369 
   370     /* main loop */
   371 
   372     //{{{
   373     var finished = false
   374     while (!finished) {
   375       receiveWithin(delay_commands_changed.flush_timeout) {
   376         case TIMEOUT => delay_commands_changed.flush()
   377 
   378         case Start(args) if prover.isEmpty =>
   379           if (phase == Session.Inactive || phase == Session.Failed) {
   380             phase = Session.Startup
   381             prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
   382           }
   383 
   384         case Stop =>
   385           if (phase == Session.Ready) {
   386             global_state >> (_ => Document.State.init)  // FIXME event bus!?
   387             phase = Session.Shutdown
   388             prover.get.terminate
   389             prover = None
   390             phase = Session.Inactive
   391           }
   392           finished = true
   393           receiver.cancel()
   394           reply(())
   395 
   396         case Cancel_Execution if prover.isDefined =>
   397           prover.get.cancel_execution()
   398 
   399         case Edit(edits) if prover.isDefined =>
   400           prover.get.discontinue_execution()
   401 
   402           val previous = global_state().history.tip.version
   403           val version = Future.promise[Document.Version]
   404           val change = global_state >>> (_.continue_history(previous, edits, version))
   405           change_parser ! Text_Edits(previous, edits, version)
   406 
   407           reply(())
   408 
   409         case Messages(msgs) =>
   410           msgs foreach {
   411             case input: Isabelle_Process.Input =>
   412               all_messages.event(input)
   413 
   414             case output: Isabelle_Process.Output =>
   415               handle_output(output)
   416               if (output.is_syslog) syslog_messages.event(output)
   417               if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
   418               all_messages.event(output)
   419           }
   420 
   421         case change: Change
   422         if prover.isDefined && global_state().is_assigned(change.previous) =>
   423           handle_change(change)
   424 
   425         case bad if !bad.isInstanceOf[Change] =>
   426           System.err.println("session_actor: ignoring bad message " + bad)
   427       }
   428     }
   429     //}}}
   430   }
   431 
   432 
   433   /* actions */
   434 
   435   def start(args: List[String])
   436   { session_actor ! Start(args) }
   437 
   438   def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
   439 
   440   def cancel_execution() { session_actor ! Cancel_Execution }
   441 
   442   def edit(edits: List[Document.Edit_Text])
   443   { session_actor !? Edit(edits) }
   444 
   445   def init_node(name: Document.Node.Name,
   446     header: Document.Node.Header, perspective: Text.Perspective, text: String)
   447   {
   448     edit(List(header_edit(name, header),
   449       name -> Document.Node.Clear(),
   450       name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
   451       name -> Document.Node.Perspective(perspective)))
   452   }
   453 
   454   def edit_node(name: Document.Node.Name,
   455     header: Document.Node.Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
   456   {
   457     edit(List(header_edit(name, header),
   458       name -> Document.Node.Edits(text_edits),
   459       name -> Document.Node.Perspective(perspective)))
   460   }
   461 }