src/Pure/System/session.scala
author wenzelm
Sat Aug 14 22:45:23 2010 +0200 (2010-08-14)
changeset 38414 49f1f657adc2
parent 38413 224efb14f258
child 38415 f3220ef79d51
permissions -rw-r--r--
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
added convenient Markup.Int/Long objects (Scala);
simplified "assign" message format -- explicit version id;
misc tuning and simplification;
     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(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(doc_id, edits)) =>
   146                 try { change_state(_.assign(doc_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_Document(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.document.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 document = stable.document.join
   313         val node = document.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           state_snapshot.command_state(document, command)
   321       }
   322     }
   323 
   324     def act
   325     {
   326       loop {
   327         react {
   328           case Edit_Document(edits) =>
   329             val history_snapshot = history
   330             require(!history_snapshot.isEmpty)
   331 
   332             val prev = history_snapshot.head.document
   333             val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
   334               isabelle.Future.fork {
   335                 val old_doc = prev.join
   336                 val former_assignment = current_state().the_assignment(old_doc).join  // FIXME async!?
   337                 Thy_Syntax.text_edits(Session.this, old_doc, edits)
   338               }
   339             val new_change = new Document.Change(prev, edits, result)
   340             history ::= new_change
   341             new_change.document.map(_ => session_actor ! new_change)
   342             reply(())
   343 
   344           case bad => System.err.println("editor_model: ignoring bad message " + bad)
   345         }
   346       }
   347     }
   348   }
   349   editor_history.start
   350 
   351 
   352 
   353   /** main methods **/
   354 
   355   def started(timeout: Int, args: List[String]): Option[String] =
   356     (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
   357 
   358   def stop() { session_actor ! Stop }
   359 
   360   def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
   361     editor_history.snapshot(name, pending_edits)
   362 
   363   def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
   364 }