src/Pure/System/session.scala
author wenzelm
Sat Sep 25 16:22:27 2010 +0200 (2010-09-25 ago)
changeset 39701 7c351c1c0624
parent 39698 625a3bc4417b
child 40478 4bae781b8f7c
permissions -rw-r--r--
simplified / clarified Session.Phase;
     1 /*  Title:      Pure/System/session.scala
     2     Author:     Makarius
     3     Options:    :folding=explicit:collapseFolds=1:
     4 
     5 Isabelle session, potentially with running prover.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import scala.actors.TIMEOUT
    12 import scala.actors.Actor
    13 import scala.actors.Actor._
    14 
    15 
    16 object Session
    17 {
    18   /* events */
    19 
    20   case object Global_Settings
    21   case object Perspective
    22   case object Assignment
    23   case class Commands_Changed(set: Set[Command])
    24 
    25   sealed abstract class Phase
    26   case object Inactive extends Phase
    27   case object Startup extends Phase  // transient
    28   case object Failed extends Phase
    29   case object Ready extends Phase
    30   case object Shutdown extends Phase  // transient
    31 }
    32 
    33 
    34 class Session(system: Isabelle_System)
    35 {
    36   /* real time parameters */  // FIXME properties or settings (!?)
    37 
    38   // user input (e.g. text edits, cursor movement)
    39   val input_delay = 300
    40 
    41   // prover output (markup, common messages)
    42   val output_delay = 100
    43 
    44   // GUI layout updates
    45   val update_delay = 500
    46 
    47 
    48   /* pervasive event buses */
    49 
    50   val phase_changed = new Event_Bus[Session.Phase]
    51   val global_settings = new Event_Bus[Session.Global_Settings.type]
    52   val raw_messages = new Event_Bus[Isabelle_Process.Result]
    53   val commands_changed = new Event_Bus[Session.Commands_Changed]
    54   val perspective = new Event_Bus[Session.Perspective.type]
    55   val assignments = new Event_Bus[Session.Assignment.type]
    56 
    57 
    58   /* unique ids */
    59 
    60   private var id_count: Document.ID = 0
    61   def new_id(): Document.ID = synchronized {
    62     require(id_count > java.lang.Long.MIN_VALUE)
    63     id_count -= 1
    64     id_count
    65   }
    66 
    67 
    68 
    69   /** buffered command changes (delay_first discipline) **/
    70 
    71   private case object Stop
    72 
    73   private val (_, command_change_buffer) =
    74     Simple_Thread.actor("command_change_buffer", daemon = true)
    75   //{{{
    76   {
    77     import scala.compat.Platform.currentTime
    78 
    79     var changed: Set[Command] = Set()
    80     var flush_time: Option[Long] = None
    81 
    82     def flush_timeout: Long =
    83       flush_time match {
    84         case None => 5000L
    85         case Some(time) => (time - currentTime) max 0
    86       }
    87 
    88     def flush()
    89     {
    90       if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
    91       changed = Set()
    92       flush_time = None
    93     }
    94 
    95     def invoke()
    96     {
    97       val now = currentTime
    98       flush_time match {
    99         case None => flush_time = Some(now + output_delay)
   100         case Some(time) => if (now >= time) flush()
   101       }
   102     }
   103 
   104     var finished = false
   105     while (!finished) {
   106       receiveWithin(flush_timeout) {
   107         case command: Command => changed += command; invoke()
   108         case TIMEOUT => flush()
   109         case Stop => finished = true; reply(())
   110         case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
   111       }
   112     }
   113   }
   114   //}}}
   115 
   116 
   117 
   118   /** main protocol actor **/
   119 
   120   @volatile private var syntax = new Outer_Syntax(system.symbols)
   121   def current_syntax(): Outer_Syntax = syntax
   122 
   123   @volatile private var reverse_syslog = List[XML.Elem]()
   124   def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
   125 
   126   @volatile private var _phase: Session.Phase = Session.Inactive
   127   def phase = _phase
   128   private def phase_=(new_phase: Session.Phase)
   129   {
   130     _phase = new_phase
   131     phase_changed.event(new_phase)
   132   }
   133 
   134   private val global_state = new Volatile(Document.State.init)
   135   def current_state(): Document.State = global_state.peek()
   136 
   137   private case object Interrupt_Prover
   138   private case class Edit_Version(edits: List[Document.Node_Text_Edit])
   139   private case class Start(timeout: Int, args: List[String])
   140 
   141   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   142   {
   143     var prover: Isabelle_Process with Isar_Document = null
   144 
   145 
   146     /* document changes */
   147 
   148     def handle_change(change: Document.Change)
   149     //{{{
   150     {
   151       val previous = change.previous.get_finished
   152       val (node_edits, version) = change.result.get_finished
   153 
   154       var former_assignment = global_state.peek().the_assignment(previous).get_finished
   155       for {
   156         (name, Some(cmd_edits)) <- node_edits
   157         (prev, None) <- cmd_edits
   158         removed <- previous.nodes(name).commands.get_after(prev)
   159       } former_assignment -= removed
   160 
   161       val id_edits =
   162         node_edits map {
   163           case (name, None) => (name, None)
   164           case (name, Some(cmd_edits)) =>
   165             val ids =
   166               cmd_edits map {
   167                 case (c1, c2) =>
   168                   val id1 = c1.map(_.id)
   169                   val id2 =
   170                     c2 match {
   171                       case None => None
   172                       case Some(command) =>
   173                         if (global_state.peek().lookup_command(command.id).isEmpty) {
   174                           global_state.change(_.define_command(command))
   175                           prover.define_command(command.id, system.symbols.encode(command.source))
   176                         }
   177                         Some(command.id)
   178                     }
   179                   (id1, id2)
   180               }
   181             (name -> Some(ids))
   182         }
   183       global_state.change(_.define_version(version, former_assignment))
   184       prover.edit_version(previous.id, version.id, id_edits)
   185     }
   186     //}}}
   187 
   188 
   189     /* prover results */
   190 
   191     def bad_result(result: Isabelle_Process.Result)
   192     {
   193       System.err.println("Ignoring prover result: " + result.message.toString)
   194     }
   195 
   196     def handle_result(result: Isabelle_Process.Result)
   197     //{{{
   198     {
   199       raw_messages.event(result)
   200 
   201       result.properties match {
   202         case Position.Id(state_id) =>
   203           try {
   204             val st = global_state.change_yield(_.accumulate(state_id, result.message))
   205             command_change_buffer ! st.command
   206           }
   207           catch { case _: Document.State.Fail => bad_result(result) }
   208         case _ =>
   209           if (result.is_syslog) {
   210             reverse_syslog ::= result.message
   211             if (result.is_ready) phase = Session.Ready
   212             else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
   213             else if (result.is_exit) phase = Session.Inactive
   214           }
   215           else if (result.is_stdout) { }
   216           else if (result.is_status) {
   217             result.body match {
   218               case List(Isar_Document.Assign(id, edits)) =>
   219                 try {
   220                   val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
   221                   for (cmd <- cmds) command_change_buffer ! cmd
   222                   assignments.event(Session.Assignment)
   223                 }
   224                 catch { case _: Document.State.Fail => bad_result(result) }
   225               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   226               case List(Keyword.Keyword_Decl(name)) => syntax += name
   227               case _ => bad_result(result)
   228             }
   229           }
   230           else bad_result(result)
   231         }
   232     }
   233     //}}}
   234 
   235 
   236     /* main loop */
   237 
   238     var finished = false
   239     while (!finished) {
   240       receive {
   241         case Interrupt_Prover =>
   242           if (prover != null) prover.interrupt
   243 
   244         case Edit_Version(edits) if prover != null =>
   245           val previous = global_state.peek().history.tip.version
   246           val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
   247           val change = global_state.change_yield(_.extend_history(previous, edits, result))
   248 
   249           val this_actor = self
   250           change.version.map(_ => {
   251             assignments.await { global_state.peek().is_assigned(previous.get_finished) }
   252             this_actor ! change })
   253 
   254           reply(())
   255 
   256         case change: Document.Change if prover != null => handle_change(change)
   257 
   258         case result: Isabelle_Process.Result => handle_result(result)
   259 
   260         case Start(timeout, args) if prover == null =>
   261           if (phase == Session.Inactive || phase == Session.Failed) {
   262             phase = Session.Startup
   263             prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
   264           }
   265 
   266         case Stop =>
   267           if (phase == Session.Ready) {
   268             global_state.change(_ => Document.State.init)  // FIXME event bus!?
   269             phase = Session.Shutdown
   270             prover.terminate
   271             phase = Session.Inactive
   272           }
   273           finished = true
   274           reply(())
   275 
   276         case bad if prover != null =>
   277           System.err.println("session_actor: ignoring bad message " + bad)
   278       }
   279     }
   280   }
   281 
   282 
   283 
   284   /** main methods **/
   285 
   286   def start(timeout: Int, args: List[String]) { session_actor ! Start(timeout, args) }
   287 
   288   def stop() { command_change_buffer !? Stop; session_actor !? Stop }
   289 
   290   def interrupt() { session_actor ! Interrupt_Prover }
   291 
   292   def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
   293 
   294   def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
   295     global_state.peek().snapshot(name, pending_edits)
   296 }