src/Pure/System/session.scala
author wenzelm
Fri Aug 13 18:21:19 2010 +0200 (2010-08-13)
changeset 38370 8b15d0f98962
parent 38366 fea82d1add74
child 38373 e8197eea3cd0
permissions -rw-r--r--
explicit Document.State value, instead of individual state variables in Session, Command, Document;
Session.snapshot: pure value based on Document.State;
Document.edit_texts: no treatment of state assignment here;
     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 old_doc = change.prev.join
    85       val (node_edits, doc) = change.result.join
    86 
    87       var former_assignment = current_state().the_assignment(old_doc).join
    88       for {
    89         (name, Some(cmd_edits)) <- node_edits
    90         (prev, None) <- cmd_edits
    91         removed <- old_doc.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_document(doc, former_assignment))
   117       prover.edit_document(old_doc.id, doc.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(target_id) =>
   136           try {
   137             val (st, state) = global_state.accumulate(target_id, result.message)
   138             global_state = state
   139             indicate_command_change(st.command)  // FIXME forward Command.State (!?)
   140           }
   141           catch {
   142             case _: Document.Failed_State =>
   143               if (result.is_status) {
   144                 result.body match {
   145                   case List(Isar_Document.Assign(edits)) =>
   146                     try { change_state(_.assign(target_id, edits)) }
   147                     catch { case _: Document.Failed_State => bad_result(result) }
   148                   case _ => bad_result(result)
   149                 }
   150               }
   151               else bad_result(result)
   152           }
   153         case None =>
   154           if (result.is_status) {
   155             result.body match {
   156               // keyword declarations   // FIXME always global!?
   157               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   158               case List(Keyword.Keyword_Decl(name)) => syntax += name
   159               case _ => if (!result.is_ready) bad_result(result)
   160             }
   161           }
   162           else if (result.kind == Markup.EXIT) prover = null
   163           else if (result.is_raw) raw_output.event(result)
   164           else if (!result.is_system) bad_result(result)  // FIXME syslog for system messages (!?)
   165         }
   166     }
   167     //}}}
   168 
   169 
   170     /* prover startup */
   171 
   172     def startup_error(): String =
   173     {
   174       val buf = new StringBuilder
   175       while (
   176         receiveWithin(0) {
   177           case result: Isabelle_Process.Result =>
   178             if (result.is_raw) {
   179               for (text <- XML.content(result.message))
   180                 buf.append(text)
   181             }
   182             true
   183           case TIMEOUT => false
   184         }) {}
   185       buf.toString
   186     }
   187 
   188     def prover_startup(timeout: Int): Option[String] =
   189     {
   190       receiveWithin(timeout) {
   191         case result: Isabelle_Process.Result
   192           if result.kind == Markup.INIT =>
   193           while (receive {
   194             case result: Isabelle_Process.Result =>
   195               handle_result(result); !result.is_ready
   196             }) {}
   197           None
   198 
   199         case result: Isabelle_Process.Result
   200           if result.kind == Markup.EXIT =>
   201           Some(startup_error())
   202 
   203         case TIMEOUT =>  // FIXME clarify
   204           prover.kill; Some(startup_error())
   205       }
   206     }
   207 
   208 
   209     /* main loop */
   210 
   211     val xml_cache = new XML.Cache(131071)
   212 
   213     loop {
   214       react {
   215         case Started(timeout, args) =>
   216           if (prover == null) {
   217             prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
   218             val origin = sender
   219             val opt_err = prover_startup(timeout)
   220             if (opt_err.isDefined) prover = null
   221             origin ! opt_err
   222           }
   223           else reply(None)
   224 
   225         case Stop =>  // FIXME clarify; synchronous
   226           if (prover != null) {
   227             prover.kill
   228             prover = null
   229           }
   230 
   231         case change: Document.Change if prover != null =>
   232           handle_change(change)
   233 
   234         case result: Isabelle_Process.Result =>
   235           handle_result(result.cache(xml_cache))
   236 
   237         case TIMEOUT =>  // FIXME clarify!
   238 
   239         case bad if prover != null =>
   240           System.err.println("session_actor: ignoring bad message " + bad)
   241       }
   242     }
   243   }
   244 
   245 
   246 
   247   /** buffered command changes (delay_first discipline) **/
   248 
   249   private lazy val command_change_buffer = actor
   250   //{{{
   251   {
   252     import scala.compat.Platform.currentTime
   253 
   254     var changed: Set[Command] = Set()
   255     var flush_time: Option[Long] = None
   256 
   257     def flush_timeout: Long =
   258       flush_time match {
   259         case None => 5000L
   260         case Some(time) => (time - currentTime) max 0
   261       }
   262 
   263     def flush()
   264     {
   265       if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
   266       changed = Set()
   267       flush_time = None
   268     }
   269 
   270     def invoke()
   271     {
   272       val now = currentTime
   273       flush_time match {
   274         case None => flush_time = Some(now + output_delay)
   275         case Some(time) => if (now >= time) flush()
   276       }
   277     }
   278 
   279     loop {
   280       reactWithin(flush_timeout) {
   281         case command: Command => changed += command; invoke()
   282         case TIMEOUT => flush()
   283         case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
   284       }
   285     }
   286   }
   287   //}}}
   288 
   289   def indicate_command_change(command: Command)
   290   {
   291     command_change_buffer ! command
   292   }
   293 
   294 
   295 
   296   /** editor history **/
   297 
   298   private case class Edit_Document(edits: List[Document.Node_Text_Edit])
   299 
   300   private val editor_history = new Actor
   301   {
   302     @volatile private var history = List(Document.Change.init)
   303 
   304     def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
   305     {
   306       val state_snapshot = current_state()
   307       val history_snapshot = history
   308 
   309       val found_stable = history_snapshot.find(change =>
   310         change.is_finished && state_snapshot.is_assigned(change.document.join))
   311       require(found_stable.isDefined)
   312       val stable = found_stable.get
   313       val latest = history_snapshot.head
   314 
   315       val edits =
   316         (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) =>
   317             (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
   318       lazy val reverse_edits = edits.reverse
   319 
   320       new Document.Snapshot {
   321         val document = stable.document.join
   322         val node = document.nodes(name)
   323         val is_outdated = !(pending_edits.isEmpty && latest == stable)
   324         def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
   325         def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
   326         def lookup_command(id: Document.Command_ID): Option[Command] =
   327           state_snapshot.lookup_command(id)
   328         def state(command: Command): Command.State =
   329           state_snapshot.command_state(document, command)
   330       }
   331     }
   332 
   333     def act
   334     {
   335       loop {
   336         react {
   337           case Edit_Document(edits) =>
   338             val history_snapshot = history
   339             require(!history_snapshot.isEmpty)
   340 
   341             val prev = history_snapshot.head.document
   342             val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
   343               isabelle.Future.fork {
   344                 val old_doc = prev.join
   345                 val former_assignment = current_state().the_assignment(old_doc).join  // FIXME async!?
   346                 Document.text_edits(Session.this, old_doc, edits)
   347               }
   348             val new_change = new Document.Change(prev, edits, result)
   349             history ::= new_change
   350             new_change.document.map(_ => session_actor ! new_change)
   351             reply(())
   352 
   353           case bad => System.err.println("editor_model: ignoring bad message " + bad)
   354         }
   355       }
   356     }
   357   }
   358   editor_history.start
   359 
   360 
   361 
   362   /** main methods **/
   363 
   364   def started(timeout: Int, args: List[String]): Option[String] =
   365     (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
   366 
   367   def stop() { session_actor ! Stop }
   368 
   369   def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
   370     editor_history.snapshot(name, pending_edits)
   371 
   372   def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
   373 }