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