src/Pure/System/session.scala
author wenzelm
Sat Aug 07 14:45:26 2010 +0200 (2010-08-07)
changeset 38222 dac5fa0ac971
parent 38221 e0f00f0945b4
child 38226 9d8848d70b0a
permissions -rw-r--r--
replaced individual Document_Model history by all-inclusive one in Session;
Document_Model: provide thy_name externally, i.e. by central Isabelle plugin;
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 
    14 
    15 object Session
    16 {
    17   /* events */
    18 
    19   case object Global_Settings
    20   case object Perspective
    21 
    22 
    23   /* managed entities */
    24 
    25   type Entity_ID = String
    26 
    27   trait Entity
    28   {
    29     val id: Entity_ID
    30     def consume(message: XML.Tree, forward: Command => Unit): Unit
    31   }
    32 }
    33 
    34 
    35 class Session(system: Isabelle_System)
    36 {
    37   /* real time parameters */  // FIXME properties or settings (!?)
    38 
    39   // user input (e.g. text edits, cursor movement)
    40   val input_delay = 300
    41 
    42   // prover output (markup, common messages)
    43   val output_delay = 100
    44 
    45   // GUI layout updates
    46   val update_delay = 500
    47 
    48 
    49   /* pervasive event buses */
    50 
    51   val global_settings = new Event_Bus[Session.Global_Settings.type]
    52   val raw_results = new Event_Bus[Isabelle_Process.Result]
    53   val raw_output = new Event_Bus[Isabelle_Process.Result]
    54   val commands_changed = new Event_Bus[Command_Set]
    55   val perspective = new Event_Bus[Session.Perspective.type]
    56 
    57 
    58   /* unique ids */
    59 
    60   private var id_count: BigInt = 0
    61   def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
    62 
    63 
    64 
    65   /** main actor **/
    66 
    67   @volatile private var syntax = new Outer_Syntax(system.symbols)
    68   def current_syntax: Outer_Syntax = syntax
    69 
    70   @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
    71   def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
    72   def lookup_command(id: Session.Entity_ID): Option[Command] =
    73     lookup_entity(id) match {
    74       case Some(cmd: Command) => Some(cmd)
    75       case _ => None
    76     }
    77 
    78   private case class Started(timeout: Int, args: List[String])
    79   private case object Stop
    80 
    81   private lazy val session_actor = actor {
    82 
    83     var prover: Isabelle_Process with Isar_Document = null
    84 
    85     def register(entity: Session.Entity) { entities += (entity.id -> entity) }
    86 
    87     var documents = Map[Document.Version_ID, Document]()
    88     def register_document(doc: Document) { documents += (doc.id -> doc) }
    89     register_document(Document.init)
    90 
    91 
    92     /* document changes */
    93 
    94     def handle_change(change: Change)
    95     //{{{
    96     {
    97       require(change.parent.isDefined)
    98 
    99       val (node_edits, doc) = change.result.join
   100       val id_edits =
   101         node_edits map {
   102           case (name, None) => (name, None)
   103           case (name, Some(cmd_edits)) =>
   104             val chs =
   105               cmd_edits map {
   106                 case (c1, c2) =>
   107                   val id1 = c1.map(_.id)
   108                   val id2 =
   109                     c2 match {
   110                       case None => None
   111                       case Some(command) =>
   112                         if (!lookup_command(command.id).isDefined) {
   113                           register(command)
   114                           prover.define_command(command.id, system.symbols.encode(command.source))
   115                         }
   116                         Some(command.id)
   117                     }
   118                   (id1, id2)
   119               }
   120             (name -> Some(chs))
   121         }
   122       register_document(doc)
   123       prover.edit_document(change.parent.get.id, doc.id, id_edits)
   124     }
   125     //}}}
   126 
   127 
   128     /* prover results */
   129 
   130     def bad_result(result: Isabelle_Process.Result)
   131     {
   132       System.err.println("Ignoring prover result: " + result.message.toString)
   133     }
   134 
   135     def handle_result(result: Isabelle_Process.Result)
   136     //{{{
   137     {
   138       raw_results.event(result)
   139 
   140       val target_id: Option[Session.Entity_ID] = Position.get_id(result.message.attributes)
   141       val target: Option[Session.Entity] =
   142         target_id match {
   143           case None => None
   144           case Some(id) => lookup_entity(id)
   145         }
   146       if (target.isDefined) target.get.consume(result.message, indicate_command_change)
   147       else if (result.is_status) {
   148         // global status message
   149         result.body match {
   150 
   151           // document state assignment
   152           case List(Isar_Document.Assign(edits)) if target_id.isDefined =>
   153             documents.get(target_id.get) match {
   154               case Some(doc) =>
   155                 val states =
   156                   for {
   157                     Isar_Document.Edit(cmd_id, state_id) <- edits
   158                     cmd <- lookup_command(cmd_id)
   159                   } yield {
   160                     val st = cmd.assign_state(state_id)
   161                     register(st)
   162                     (cmd, st)
   163                   }
   164                 doc.assign_states(states)
   165               case None => bad_result(result)
   166             }
   167 
   168           // keyword declarations
   169           case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   170           case List(Keyword.Keyword_Decl(name)) => syntax += name
   171 
   172           case _ => if (!result.is_ready) bad_result(result)
   173         }
   174       }
   175       else if (result.kind == Markup.EXIT)
   176         prover = null
   177       else if (result.is_raw)
   178         raw_output.event(result)
   179       else if (!result.is_system)   // FIXME syslog (!?)
   180         bad_result(result)
   181     }
   182     //}}}
   183 
   184 
   185     /* prover startup */
   186 
   187     def startup_error(): String =
   188     {
   189       val buf = new StringBuilder
   190       while (
   191         receiveWithin(0) {
   192           case result: Isabelle_Process.Result =>
   193             if (result.is_raw) {
   194               for (text <- XML.content(result.message))
   195                 buf.append(text)
   196             }
   197             true
   198           case TIMEOUT => false
   199         }) {}
   200       buf.toString
   201     }
   202 
   203     def prover_startup(timeout: Int): Option[String] =
   204     {
   205       receiveWithin(timeout) {
   206         case result: Isabelle_Process.Result
   207           if result.kind == Markup.INIT =>
   208           while (receive {
   209             case result: Isabelle_Process.Result =>
   210               handle_result(result); !result.is_ready
   211             }) {}
   212           None
   213 
   214         case result: Isabelle_Process.Result
   215           if result.kind == Markup.EXIT =>
   216           Some(startup_error())
   217 
   218         case TIMEOUT =>  // FIXME clarify
   219           prover.kill; Some(startup_error())
   220       }
   221     }
   222 
   223 
   224     /* main loop */
   225 
   226     val xml_cache = new XML.Cache(131071)
   227 
   228     loop {
   229       react {
   230         case Started(timeout, args) =>
   231           if (prover == null) {
   232             prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
   233             val origin = sender
   234             val opt_err = prover_startup(timeout)
   235             if (opt_err.isDefined) prover = null
   236             origin ! opt_err
   237           }
   238           else reply(None)
   239 
   240         case Stop =>  // FIXME clarify; synchronous
   241           if (prover != null) {
   242             prover.kill
   243             prover = null
   244           }
   245 
   246         case change: Change if prover != null =>
   247           handle_change(change)
   248 
   249         case result: Isabelle_Process.Result =>
   250           handle_result(result.cache(xml_cache))
   251 
   252         case TIMEOUT =>  // FIXME clarify!
   253 
   254         case bad if prover != null =>
   255           System.err.println("session_actor: ignoring bad message " + bad)
   256       }
   257     }
   258   }
   259 
   260 
   261 
   262   /** buffered command changes -- delay_first discipline **/
   263 
   264   private lazy val command_change_buffer = actor
   265   //{{{
   266   {
   267     import scala.compat.Platform.currentTime
   268 
   269     var changed: Set[Command] = Set()
   270     var flush_time: Option[Long] = None
   271 
   272     def flush_timeout: Long =
   273       flush_time match {
   274         case None => 5000L
   275         case Some(time) => (time - currentTime) max 0
   276       }
   277 
   278     def flush()
   279     {
   280       if (!changed.isEmpty) commands_changed.event(Command_Set(changed))
   281       changed = Set()
   282       flush_time = None
   283     }
   284 
   285     def invoke()
   286     {
   287       val now = currentTime
   288       flush_time match {
   289         case None => flush_time = Some(now + output_delay)
   290         case Some(time) => if (now >= time) flush()
   291       }
   292     }
   293 
   294     loop {
   295       reactWithin(flush_timeout) {
   296         case command: Command => changed += command; invoke()
   297         case TIMEOUT => flush()
   298         case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
   299       }
   300     }
   301   }
   302   //}}}
   303 
   304   def indicate_command_change(command: Command)
   305   {
   306     command_change_buffer ! command
   307   }
   308 
   309 
   310   /* main methods */
   311 
   312   def started(timeout: Int, args: List[String]): Option[String] =
   313     (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
   314 
   315   def stop() { session_actor ! Stop }
   316 
   317   def input(change: Change) { session_actor ! change }
   318 
   319 
   320 
   321   /** editor model **/  // FIXME subclass Editor_Session (!?)
   322 
   323   @volatile private var history = Change.init // owned by Swing thread (!??)
   324   def current_change(): Change = history
   325 
   326   def edit_document(edits: List[Document.Node_Text_Edit])
   327   {
   328     Swing_Thread.now {
   329       val old_change = current_change()
   330       val new_id = create_id()
   331       val result: Future[(List[Document.Edit[Command]], Document)] =
   332         Future.fork {
   333           val old_doc = old_change.join_document
   334           old_doc.await_assignment
   335           Document.text_edits(this, old_doc, new_id, edits)
   336         }
   337       val new_change = new Change(new_id, Some(old_change), edits, result)
   338       history = new_change
   339       new_change.result.map(_ => input(new_change))
   340     }
   341   }
   342 }