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