src/Pure/System/session.scala
author wenzelm
Thu Aug 12 17:37:58 2010 +0200 (2010-08-12)
changeset 38366 fea82d1add74
parent 38365 7c6254a9c432
child 38370 8b15d0f98962
permissions -rw-r--r--
simplified/clarified Change: transition prev --edits--> result, based on futures;
Session.history: plain List instead of somewhat indirect Change.ancestors;
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   /* managed entities */
    27 
    28   trait Entity
    29   {
    30     val id: Document.ID
    31     def consume(message: XML.Tree, forward: Command => Unit): Unit
    32   }
    33 }
    34 
    35 
    36 class Session(system: Isabelle_System)
    37 {
    38   /* real time parameters */  // FIXME properties or settings (!?)
    39 
    40   // user input (e.g. text edits, cursor movement)
    41   val input_delay = 300
    42 
    43   // prover output (markup, common messages)
    44   val output_delay = 100
    45 
    46   // GUI layout updates
    47   val update_delay = 500
    48 
    49 
    50   /* pervasive event buses */
    51 
    52   val global_settings = new Event_Bus[Session.Global_Settings.type]
    53   val raw_results = new Event_Bus[Isabelle_Process.Result]
    54   val raw_output = new Event_Bus[Isabelle_Process.Result]
    55   val commands_changed = new Event_Bus[Session.Commands_Changed]
    56   val perspective = new Event_Bus[Session.Perspective.type]
    57 
    58 
    59   /* unique ids */
    60 
    61   private var id_count: Document.ID = 0
    62   def create_id(): Document.ID = synchronized {
    63     require(id_count > java.lang.Long.MIN_VALUE)
    64     id_count -= 1
    65     id_count
    66   }
    67 
    68 
    69 
    70   /** main actor **/
    71 
    72   @volatile private var syntax = new Outer_Syntax(system.symbols)
    73   def current_syntax: Outer_Syntax = syntax
    74 
    75   @volatile private var entities = Map[Document.ID, Session.Entity]()
    76   def lookup_entity(id: Document.ID): Option[Session.Entity] = entities.get(id)
    77   def lookup_command(id: Document.ID): Option[Command] =
    78     lookup_entity(id) match {
    79       case Some(cmd: Command) => Some(cmd)
    80       case _ => None
    81     }
    82 
    83   private case class Started(timeout: Int, args: List[String])
    84   private case object Stop
    85 
    86   private lazy val session_actor = actor {
    87 
    88     var prover: Isabelle_Process with Isar_Document = null
    89 
    90     def register(entity: Session.Entity) { entities += (entity.id -> entity) }
    91 
    92     var documents = Map[Document.Version_ID, Document]()
    93     def register_document(doc: Document) { documents += (doc.id -> doc) }
    94     register_document(Document.init)
    95 
    96 
    97     /* document changes */
    98 
    99     def handle_change(change: Document.Change)
   100     //{{{
   101     {
   102       require(change.is_finished)
   103 
   104       val old_id = change.prev.join.id
   105       val (node_edits, doc) = change.result.join
   106 
   107       val id_edits =
   108         node_edits map {
   109           case (name, None) => (name, None)
   110           case (name, Some(cmd_edits)) =>
   111             val chs =
   112               cmd_edits map {
   113                 case (c1, c2) =>
   114                   val id1 = c1.map(_.id)
   115                   val id2 =
   116                     c2 match {
   117                       case None => None
   118                       case Some(command) =>
   119                         if (!lookup_command(command.id).isDefined) {
   120                           register(command)
   121                           prover.define_command(command.id, system.symbols.encode(command.source))
   122                         }
   123                         Some(command.id)
   124                     }
   125                   (id1, id2)
   126               }
   127             (name -> Some(chs))
   128         }
   129       register_document(doc)
   130       prover.edit_document(old_id, doc.id, id_edits)
   131     }
   132     //}}}
   133 
   134 
   135     /* prover results */
   136 
   137     def bad_result(result: Isabelle_Process.Result)
   138     {
   139       System.err.println("Ignoring prover result: " + result.message.toString)
   140     }
   141 
   142     def handle_result(result: Isabelle_Process.Result)
   143     //{{{
   144     {
   145       raw_results.event(result)
   146 
   147       val target_id: Option[Document.ID] = Position.get_id(result.properties)
   148       val target: Option[Session.Entity] =
   149         target_id match {
   150           case None => None
   151           case Some(id) => lookup_entity(id)
   152         }
   153       if (target.isDefined) target.get.consume(result.message, indicate_command_change)
   154       else if (result.is_status) {
   155         // global status message
   156         result.body match {
   157 
   158           // execution assignment
   159           case List(Isar_Document.Assign(edits)) if target_id.isDefined =>
   160             documents.get(target_id.get) match {
   161               case Some(doc) =>
   162                 val execs =
   163                   for {
   164                     Isar_Document.Edit(cmd_id, exec_id) <- edits
   165                     cmd <- lookup_command(cmd_id)
   166                   } yield {
   167                     val st = cmd.assign_exec(exec_id)  // FIXME session state
   168                     register(st)
   169                     (cmd, st)
   170                   }
   171                 doc.assign_execs(execs)  // FIXME session state
   172               case None => bad_result(result)
   173             }
   174 
   175           // keyword declarations
   176           case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   177           case List(Keyword.Keyword_Decl(name)) => syntax += name
   178 
   179           case _ => if (!result.is_ready) bad_result(result)
   180         }
   181       }
   182       else if (result.kind == Markup.EXIT)
   183         prover = null
   184       else if (result.is_raw)
   185         raw_output.event(result)
   186       else if (!result.is_system)   // FIXME syslog (!?)
   187         bad_result(result)
   188     }
   189     //}}}
   190 
   191 
   192     /* prover startup */
   193 
   194     def startup_error(): String =
   195     {
   196       val buf = new StringBuilder
   197       while (
   198         receiveWithin(0) {
   199           case result: Isabelle_Process.Result =>
   200             if (result.is_raw) {
   201               for (text <- XML.content(result.message))
   202                 buf.append(text)
   203             }
   204             true
   205           case TIMEOUT => false
   206         }) {}
   207       buf.toString
   208     }
   209 
   210     def prover_startup(timeout: Int): Option[String] =
   211     {
   212       receiveWithin(timeout) {
   213         case result: Isabelle_Process.Result
   214           if result.kind == Markup.INIT =>
   215           while (receive {
   216             case result: Isabelle_Process.Result =>
   217               handle_result(result); !result.is_ready
   218             }) {}
   219           None
   220 
   221         case result: Isabelle_Process.Result
   222           if result.kind == Markup.EXIT =>
   223           Some(startup_error())
   224 
   225         case TIMEOUT =>  // FIXME clarify
   226           prover.kill; Some(startup_error())
   227       }
   228     }
   229 
   230 
   231     /* main loop */
   232 
   233     val xml_cache = new XML.Cache(131071)
   234 
   235     loop {
   236       react {
   237         case Started(timeout, args) =>
   238           if (prover == null) {
   239             prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
   240             val origin = sender
   241             val opt_err = prover_startup(timeout)
   242             if (opt_err.isDefined) prover = null
   243             origin ! opt_err
   244           }
   245           else reply(None)
   246 
   247         case Stop =>  // FIXME clarify; synchronous
   248           if (prover != null) {
   249             prover.kill
   250             prover = null
   251           }
   252 
   253         case change: Document.Change if prover != null =>
   254           handle_change(change)
   255 
   256         case result: Isabelle_Process.Result =>
   257           handle_result(result.cache(xml_cache))
   258 
   259         case TIMEOUT =>  // FIXME clarify!
   260 
   261         case bad if prover != null =>
   262           System.err.println("session_actor: ignoring bad message " + bad)
   263       }
   264     }
   265   }
   266 
   267 
   268 
   269   /** buffered command changes (delay_first discipline) **/
   270 
   271   private lazy val command_change_buffer = actor
   272   //{{{
   273   {
   274     import scala.compat.Platform.currentTime
   275 
   276     var changed: Set[Command] = Set()
   277     var flush_time: Option[Long] = None
   278 
   279     def flush_timeout: Long =
   280       flush_time match {
   281         case None => 5000L
   282         case Some(time) => (time - currentTime) max 0
   283       }
   284 
   285     def flush()
   286     {
   287       if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
   288       changed = Set()
   289       flush_time = None
   290     }
   291 
   292     def invoke()
   293     {
   294       val now = currentTime
   295       flush_time match {
   296         case None => flush_time = Some(now + output_delay)
   297         case Some(time) => if (now >= time) flush()
   298       }
   299     }
   300 
   301     loop {
   302       reactWithin(flush_timeout) {
   303         case command: Command => changed += command; invoke()
   304         case TIMEOUT => flush()
   305         case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
   306       }
   307     }
   308   }
   309   //}}}
   310 
   311   def indicate_command_change(command: Command)
   312   {
   313     command_change_buffer ! command
   314   }
   315 
   316 
   317 
   318   /** editor history **/
   319 
   320   private case class Edit_Document(edits: List[Document.Node_Text_Edit])
   321 
   322   private val editor_history = new Actor
   323   {
   324     @volatile private var history = List(Document.Change.init)
   325 
   326     def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
   327     {
   328       val history_snapshot = history
   329 
   330       require(history_snapshot.exists(_.is_assigned))
   331       val latest = history_snapshot.head
   332       val stable = history_snapshot.find(_.is_assigned).get
   333 
   334       val edits =
   335         (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) =>
   336             (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
   337       lazy val reverse_edits = edits.reverse
   338 
   339       new Document.Snapshot {
   340         val document = stable.document.join
   341         val node = document.nodes(name)
   342         val is_outdated = !(pending_edits.isEmpty && latest == stable)
   343         def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
   344         def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
   345         def state(command: Command): Command.State = document.current_state(command)
   346       }
   347     }
   348 
   349     def act
   350     {
   351       loop {
   352         react {
   353           case Edit_Document(edits) =>
   354             val history_snapshot = history
   355             require(!history_snapshot.isEmpty)
   356 
   357             val prev = history_snapshot.head.document
   358             val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
   359               isabelle.Future.fork {
   360                 val old_doc = prev.join
   361                 old_doc.await_assignment
   362                 Document.text_edits(Session.this, old_doc, edits)
   363               }
   364             val new_change = new Document.Change(prev, edits, result)
   365             history ::= new_change
   366             new_change.document.map(_ => session_actor ! new_change)
   367             reply(())
   368 
   369           case bad => System.err.println("editor_model: ignoring bad message " + bad)
   370         }
   371       }
   372     }
   373   }
   374   editor_history.start
   375 
   376 
   377 
   378   /** main methods **/
   379 
   380   def started(timeout: Int, args: List[String]): Option[String] =
   381     (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
   382 
   383   def stop() { session_actor ! Stop }
   384 
   385   def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
   386     editor_history.snapshot(name, pending_edits)
   387 
   388   def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
   389 }