src/Pure/System/session.scala
author wenzelm
Mon Aug 23 16:53:22 2010 +0200 (2010-08-23)
changeset 38639 f642faca303e
parent 38569 9d480f6a2589
child 38722 ba31936497c2
permissions -rw-r--r--
main session actor as independent thread, to avoid starvation via regular worker pool;
tuned;
     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 class Commands_Changed(set: Set[Command])
    23 }
    24 
    25 
    26 class Session(system: Isabelle_System)
    27 {
    28   /* real time parameters */  // FIXME properties or settings (!?)
    29 
    30   // user input (e.g. text edits, cursor movement)
    31   val input_delay = 300
    32 
    33   // prover output (markup, common messages)
    34   val output_delay = 100
    35 
    36   // GUI layout updates
    37   val update_delay = 500
    38 
    39 
    40   /* pervasive event buses */
    41 
    42   val global_settings = new Event_Bus[Session.Global_Settings.type]
    43   val raw_protocol = new Event_Bus[Isabelle_Process.Result]
    44   val raw_output = new Event_Bus[Isabelle_Process.Result]
    45   val commands_changed = new Event_Bus[Session.Commands_Changed]
    46   val perspective = new Event_Bus[Session.Perspective.type]
    47 
    48 
    49   /* unique ids */
    50 
    51   private var id_count: Document.ID = 0
    52   def new_id(): Document.ID = synchronized {
    53     require(id_count > java.lang.Long.MIN_VALUE)
    54     id_count -= 1
    55     id_count
    56   }
    57 
    58 
    59 
    60   /** main actor **/
    61 
    62   @volatile private var syntax = new Outer_Syntax(system.symbols)
    63   def current_syntax(): Outer_Syntax = syntax
    64 
    65   @volatile private var global_state = Document.State.init
    66   private def change_state(f: Document.State => Document.State) { global_state = f(global_state) }
    67   def current_state(): Document.State = global_state
    68 
    69   private case class Started(timeout: Int, args: List[String])
    70   private case object Stop
    71 
    72   private val session_actor = Simple_Thread.actor("session_actor", daemon = true)
    73   {
    74     var prover: Isabelle_Process with Isar_Document = null
    75 
    76 
    77     /* document changes */
    78 
    79     def handle_change(change: Document.Change)
    80     //{{{
    81     {
    82       require(change.is_finished)
    83 
    84       val previous = change.previous.join
    85       val (node_edits, current) = change.result.join
    86 
    87       var former_assignment = current_state().the_assignment(previous).join
    88       for {
    89         (name, Some(cmd_edits)) <- node_edits
    90         (prev, None) <- cmd_edits
    91         removed <- previous.nodes(name).commands.get_after(prev)
    92       } former_assignment -= removed
    93 
    94       val id_edits =
    95         node_edits map {
    96           case (name, None) => (name, None)
    97           case (name, Some(cmd_edits)) =>
    98             val ids =
    99               cmd_edits map {
   100                 case (c1, c2) =>
   101                   val id1 = c1.map(_.id)
   102                   val id2 =
   103                     c2 match {
   104                       case None => None
   105                       case Some(command) =>
   106                         if (current_state().lookup_command(command.id).isEmpty) {
   107                           change_state(_.define_command(command))
   108                           prover.define_command(command.id, system.symbols.encode(command.source))
   109                         }
   110                         Some(command.id)
   111                     }
   112                   (id1, id2)
   113               }
   114             (name -> Some(ids))
   115         }
   116       change_state(_.define_version(current, former_assignment))
   117       prover.edit_version(previous.id, current.id, id_edits)
   118     }
   119     //}}}
   120 
   121 
   122     /* prover results */
   123 
   124     def bad_result(result: Isabelle_Process.Result)
   125     {
   126       System.err.println("Ignoring prover result: " + result.message.toString)
   127     }
   128 
   129     def handle_result(result: Isabelle_Process.Result)
   130     //{{{
   131     {
   132       raw_protocol.event(result)
   133 
   134       Position.get_id(result.properties) match {
   135         case Some(state_id) =>
   136           try {
   137             val (st, state) = global_state.accumulate(state_id, result.message)
   138             global_state = state
   139             indicate_command_change(st.command)
   140           }
   141           catch { case _: Document.State.Fail => bad_result(result) }
   142         case None =>
   143           if (result.is_status) {
   144             result.body match {
   145               case List(Isar_Document.Assign(id, edits)) =>
   146                 try { change_state(_.assign(id, edits)) }
   147                 catch { case _: Document.State.Fail => bad_result(result) }
   148               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   149               case List(Keyword.Keyword_Decl(name)) => syntax += name
   150               case _ => if (!result.is_ready) bad_result(result)
   151             }
   152           }
   153           else if (result.kind == Markup.EXIT) prover = null
   154           else if (result.is_raw) raw_output.event(result)
   155           else if (!result.is_system) bad_result(result)  // FIXME syslog for system messages (!?)
   156         }
   157     }
   158     //}}}
   159 
   160 
   161     /* prover startup */
   162 
   163     def startup_error(): String =
   164     {
   165       val buf = new StringBuilder
   166       while (
   167         receiveWithin(0) {
   168           case result: Isabelle_Process.Result =>
   169             if (result.is_raw) {
   170               for (text <- XML.content(result.message))
   171                 buf.append(text)
   172             }
   173             true
   174           case TIMEOUT => false
   175         }) {}
   176       buf.toString
   177     }
   178 
   179     def prover_startup(timeout: Int): Option[String] =
   180     {
   181       receiveWithin(timeout) {
   182         case result: Isabelle_Process.Result
   183           if result.kind == Markup.INIT =>
   184           while (receive {
   185             case result: Isabelle_Process.Result =>
   186               handle_result(result); !result.is_ready
   187             }) {}
   188           None
   189 
   190         case result: Isabelle_Process.Result
   191           if result.kind == Markup.EXIT =>
   192           Some(startup_error())
   193 
   194         case TIMEOUT =>  // FIXME clarify
   195           prover.kill; Some(startup_error())
   196       }
   197     }
   198 
   199 
   200     /* main loop */
   201 
   202     var finished = false
   203     while (!finished) {
   204       receive {
   205         case Started(timeout, args) =>
   206           if (prover == null) {
   207             prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
   208             val origin = sender
   209             val opt_err = prover_startup(timeout)
   210             if (opt_err.isDefined) prover = null
   211             origin ! opt_err
   212           }
   213           else reply(None)
   214 
   215         case Stop => // FIXME synchronous!?
   216           if (prover != null) {
   217             prover.kill
   218             prover = null
   219             finished = true
   220           }
   221 
   222         case change: Document.Change if prover != null =>
   223           handle_change(change)
   224 
   225         case result: Isabelle_Process.Result =>
   226           handle_result(result)
   227 
   228         case TIMEOUT =>  // FIXME clarify!
   229 
   230         case bad if prover != null =>
   231           System.err.println("session_actor: ignoring bad message " + bad)
   232       }
   233     }
   234   }
   235 
   236 
   237 
   238   /** buffered command changes (delay_first discipline) **/
   239 
   240   private val command_change_buffer = actor
   241   //{{{
   242   {
   243     import scala.compat.Platform.currentTime
   244 
   245     var changed: Set[Command] = Set()
   246     var flush_time: Option[Long] = None
   247 
   248     def flush_timeout: Long =
   249       flush_time match {
   250         case None => 5000L
   251         case Some(time) => (time - currentTime) max 0
   252       }
   253 
   254     def flush()
   255     {
   256       if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
   257       changed = Set()
   258       flush_time = None
   259     }
   260 
   261     def invoke()
   262     {
   263       val now = currentTime
   264       flush_time match {
   265         case None => flush_time = Some(now + output_delay)
   266         case Some(time) => if (now >= time) flush()
   267       }
   268     }
   269 
   270     loop {
   271       reactWithin(flush_timeout) {
   272         case command: Command => changed += command; invoke()
   273         case TIMEOUT => flush()
   274         case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
   275       }
   276     }
   277   }
   278   //}}}
   279 
   280   def indicate_command_change(command: Command)
   281   {
   282     command_change_buffer ! command
   283   }
   284 
   285 
   286 
   287   /** editor history **/
   288 
   289   private case class Edit_Version(edits: List[Document.Node_Text_Edit])
   290 
   291   @volatile private var history = Document.History.init
   292 
   293   def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
   294     history.snapshot(name, pending_edits, current_state())
   295 
   296   private val editor_history = actor
   297   {
   298     loop {
   299       react {
   300         case Edit_Version(edits) =>
   301           val prev = history.tip.current
   302           val result =
   303             // FIXME potential denial-of-service concerning worker pool (!?!?)
   304             isabelle.Future.fork {
   305               val previous = prev.join
   306               val former_assignment = current_state().the_assignment(previous).join  // FIXME async!?
   307               Thy_Syntax.text_edits(Session.this, previous, edits)
   308             }
   309           val change = new Document.Change(prev, edits, result)
   310           history += change
   311           change.current.map(_ => session_actor ! change)
   312           reply(())
   313 
   314         case bad => System.err.println("editor_model: ignoring bad message " + bad)
   315       }
   316     }
   317   }
   318 
   319 
   320 
   321   /** main methods **/
   322 
   323   def started(timeout: Int, args: List[String]): Option[String] =
   324     (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
   325 
   326   def stop() { session_actor ! Stop }
   327 
   328   def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }
   329 }