src/Pure/System/session.scala
author wenzelm
Sun Aug 15 14:18:52 2010 +0200 (2010-08-15)
changeset 38417 b8922ae21111
parent 38416 56e76cd46b4f
child 38419 f9dc924e54f8
permissions -rw-r--r--
renamed class Document to Document.Version etc.;
renamed Change.prev to Change.previous, and Change.document to Change.current;
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_results = 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 create_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 lazy val session_actor = actor {
    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_results.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     val xml_cache = new XML.Cache(131071)
   203 
   204     loop {
   205       react {
   206         case Started(timeout, args) =>
   207           if (prover == null) {
   208             prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
   209             val origin = sender
   210             val opt_err = prover_startup(timeout)
   211             if (opt_err.isDefined) prover = null
   212             origin ! opt_err
   213           }
   214           else reply(None)
   215 
   216         case Stop =>  // FIXME clarify; synchronous
   217           if (prover != null) {
   218             prover.kill
   219             prover = null
   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.cache(xml_cache))
   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 lazy 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   private val editor_history = new Actor
   292   {
   293     @volatile private var history = List(Document.Change.init)
   294 
   295     def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
   296     {
   297       val state_snapshot = current_state()
   298       val history_snapshot = history
   299 
   300       val found_stable = history_snapshot.find(change =>
   301         change.is_finished && state_snapshot.is_assigned(change.current.join))
   302       require(found_stable.isDefined)
   303       val stable = found_stable.get
   304       val latest = history_snapshot.head
   305 
   306       val edits =
   307         (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) =>
   308             (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
   309       lazy val reverse_edits = edits.reverse
   310 
   311       new Document.Snapshot {
   312         val version = stable.current.join
   313         val node = version.nodes(name)
   314         val is_outdated = !(pending_edits.isEmpty && latest == stable)
   315         def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
   316         def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
   317         def lookup_command(id: Document.Command_ID): Option[Command] =
   318           state_snapshot.lookup_command(id)
   319         def state(command: Command): Command.State =
   320           try { state_snapshot.command_state(version, command) }
   321           catch { case _: Document.State.Fail => command.empty_state }
   322       }
   323     }
   324 
   325     def act
   326     {
   327       loop {
   328         react {
   329           case Edit_Version(edits) =>
   330             val history_snapshot = history
   331             require(!history_snapshot.isEmpty)
   332 
   333             val prev = history_snapshot.head.current
   334             val result =
   335               isabelle.Future.fork {
   336                 val previous = prev.join
   337                 val former_assignment = current_state().the_assignment(previous).join  // FIXME async!?
   338                 Thy_Syntax.text_edits(Session.this, previous, edits)
   339               }
   340             val new_change = new Document.Change(prev, edits, result)
   341             history ::= new_change
   342             new_change.current.map(_ => session_actor ! new_change)
   343             reply(())
   344 
   345           case bad => System.err.println("editor_model: ignoring bad message " + bad)
   346         }
   347       }
   348     }
   349   }
   350   editor_history.start
   351 
   352 
   353 
   354   /** main methods **/
   355 
   356   def started(timeout: Int, args: List[String]): Option[String] =
   357     (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
   358 
   359   def stop() { session_actor ! Stop }
   360 
   361   def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
   362     editor_history.snapshot(name, pending_edits)
   363 
   364   def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }
   365 }