src/Pure/System/session.scala
author wenzelm
Wed Sep 22 16:17:20 2010 +0200 (2010-09-22)
changeset 39593 1a34187f0b97
parent 39589 5b81b8df1dde
child 39625 fb0c851e4f9d
permissions -rw-r--r--
basic setup for Session_Dockable controls;
     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_messages = 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   val assignments = new Event_Bus[Session.Assignment.type]
    48 
    49 
    50   /* unique ids */
    51 
    52   private var id_count: Document.ID = 0
    53   def new_id(): Document.ID = synchronized {
    54     require(id_count > java.lang.Long.MIN_VALUE)
    55     id_count -= 1
    56     id_count
    57   }
    58 
    59 
    60 
    61   /** buffered command changes (delay_first discipline) **/
    62 
    63   private case object Stop
    64 
    65   private val (_, command_change_buffer) =
    66     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 object Interrupt_Prover
   119   private case class Edit_Version(edits: List[Document.Node_Text_Edit])
   120   private case class Started(timeout: Int, args: List[String])
   121 
   122   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   123   {
   124     var prover: Isabelle_Process with Isar_Document = null
   125 
   126 
   127     /* document changes */
   128 
   129     def handle_change(change: Document.Change)
   130     //{{{
   131     {
   132       val previous = change.previous.get_finished
   133       val (node_edits, current) = change.result.get_finished
   134 
   135       var former_assignment = global_state.peek().the_assignment(previous).get_finished
   136       for {
   137         (name, Some(cmd_edits)) <- node_edits
   138         (prev, None) <- cmd_edits
   139         removed <- previous.nodes(name).commands.get_after(prev)
   140       } former_assignment -= removed
   141 
   142       val id_edits =
   143         node_edits map {
   144           case (name, None) => (name, None)
   145           case (name, Some(cmd_edits)) =>
   146             val ids =
   147               cmd_edits map {
   148                 case (c1, c2) =>
   149                   val id1 = c1.map(_.id)
   150                   val id2 =
   151                     c2 match {
   152                       case None => None
   153                       case Some(command) =>
   154                         if (global_state.peek().lookup_command(command.id).isEmpty) {
   155                           global_state.change(_.define_command(command))
   156                           prover.define_command(command.id, system.symbols.encode(command.source))
   157                         }
   158                         Some(command.id)
   159                     }
   160                   (id1, id2)
   161               }
   162             (name -> Some(ids))
   163         }
   164       global_state.change(_.define_version(current, former_assignment))
   165       prover.edit_version(previous.id, current.id, id_edits)
   166     }
   167     //}}}
   168 
   169 
   170     /* prover results */
   171 
   172     def bad_result(result: Isabelle_Process.Result)
   173     {
   174       System.err.println("Ignoring prover result: " + result.message.toString)
   175     }
   176 
   177     def handle_result(result: Isabelle_Process.Result)
   178     //{{{
   179     {
   180       raw_messages.event(result)
   181 
   182       result.properties match {
   183         case Position.Id(state_id) =>
   184           try {
   185             val st = global_state.change_yield(_.accumulate(state_id, result.message))
   186             command_change_buffer ! st.command
   187           }
   188           catch { case _: Document.State.Fail => bad_result(result) }
   189         case _ =>
   190           if (result.is_status) {
   191             result.body match {
   192               case List(Isar_Document.Assign(id, edits)) =>
   193                 try {
   194                   val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
   195                   for (cmd <- cmds) command_change_buffer ! cmd
   196                   assignments.event(Session.Assignment)
   197                 }
   198                 catch { case _: Document.State.Fail => bad_result(result) }
   199               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   200               case List(Keyword.Keyword_Decl(name)) => syntax += name
   201               case _ => if (!result.is_ready) bad_result(result)
   202             }
   203           }
   204           else if (result.is_exit) prover = null  // FIXME ??
   205           else if (!(result.is_init || result.is_exit || result.is_system || result.is_stdout))
   206             bad_result(result)
   207         }
   208     }
   209     //}}}
   210 
   211 
   212     /* prover startup */
   213 
   214     def startup_error(): String =
   215     {
   216       val buf = new StringBuilder
   217       while (
   218         receiveWithin(0) {
   219           case result: Isabelle_Process.Result =>
   220             if (result.is_system) {
   221               for (text <- XML.content(result.message))
   222                 buf.append(text)
   223             }
   224             true
   225           case TIMEOUT => false
   226         }) {}
   227       buf.toString
   228     }
   229 
   230     def prover_startup(timeout: Int): Option[String] =
   231     {
   232       receiveWithin(timeout) {
   233         case result: Isabelle_Process.Result if result.is_init =>
   234           handle_result(result)
   235           while (receive {
   236             case result: Isabelle_Process.Result =>
   237               handle_result(result); !result.is_ready
   238             }) {}
   239           None
   240 
   241         case result: Isabelle_Process.Result if result.is_exit =>
   242           handle_result(result)
   243           Some(startup_error())
   244 
   245         case TIMEOUT =>  // FIXME clarify
   246           prover.terminate; Some(startup_error())
   247       }
   248     }
   249 
   250 
   251     /* main loop */  // FIXME proper shutdown
   252 
   253     var finished = false
   254     while (!finished) {
   255       receive {
   256         case Interrupt_Prover =>
   257           if (prover != null) prover.interrupt
   258 
   259         case Edit_Version(edits) =>
   260           val previous = global_state.peek().history.tip.current
   261           val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
   262           val change = global_state.change_yield(_.extend_history(previous, edits, result))
   263 
   264           val this_actor = self
   265           change.current.map(_ => {
   266             assignments.await { global_state.peek().is_assigned(previous.get_finished) }
   267             this_actor ! change })
   268 
   269           reply(())
   270 
   271         case change: Document.Change if prover != null =>
   272           handle_change(change)
   273 
   274         case result: Isabelle_Process.Result =>
   275           handle_result(result)
   276 
   277         case Started(timeout, args) =>
   278           if (prover == null) {
   279             prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
   280             val origin = sender
   281             val opt_err = prover_startup(timeout + 500)
   282             if (opt_err.isDefined) prover = null
   283             origin ! opt_err
   284           }
   285           else reply(None)
   286 
   287         case Stop => // FIXME synchronous!?
   288           if (prover != null) {
   289             global_state.change(_ => Document.State.init)
   290             prover.terminate
   291             prover = null
   292           }
   293 
   294         case TIMEOUT =>  // FIXME clarify
   295 
   296         case bad if prover != null =>
   297           System.err.println("session_actor: ignoring bad message " + bad)
   298       }
   299     }
   300   }
   301 
   302 
   303 
   304   /** main methods **/
   305 
   306   def started(timeout: Int, args: List[String]): Option[String] =
   307     (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
   308 
   309   def stop() { command_change_buffer ! Stop; session_actor ! Stop }
   310 
   311   def interrupt() { session_actor ! Interrupt_Prover }
   312 
   313   def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
   314 
   315   def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
   316     global_state.peek().snapshot(name, pending_edits)
   317 }