src/Pure/System/session.scala
author wenzelm
Mon Oct 17 11:24:22 2011 +0200 (2011-10-17 ago)
changeset 45158 db4bf4fb5492
parent 45076 dd803d319d5b
child 45248 3b7b64b194ee
permissions -rw-r--r--
always use sockets on Windows/Cygwin;
discontinued special raw_dump facility;
     1 /*  Title:      Pure/System/session.scala
     2     Author:     Makarius
     3     Options:    :folding=explicit:collapseFolds=1:
     4 
     5 Main Isabelle/Scala session, potentially with running prover process.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import java.lang.System
    12 import java.util.{Timer, TimerTask}
    13 
    14 import scala.collection.mutable
    15 import scala.actors.TIMEOUT
    16 import scala.actors.Actor._
    17 
    18 
    19 object Session
    20 {
    21   /* events */
    22 
    23   //{{{
    24   case object Global_Settings
    25   case object Caret_Focus
    26   case object Assignment
    27   case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command])
    28 
    29   sealed abstract class Phase
    30   case object Inactive extends Phase
    31   case object Startup extends Phase  // transient
    32   case object Failed extends Phase
    33   case object Ready extends Phase
    34   case object Shutdown extends Phase  // transient
    35   //}}}
    36 }
    37 
    38 
    39 class Session(thy_load: Thy_Load = new Thy_Load)
    40 {
    41   /* real time parameters */  // FIXME properties or settings (!?)
    42 
    43   val message_delay = Time.seconds(0.01)  // prover messages
    44   val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
    45   val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
    46   val update_delay = Time.seconds(0.5)  // GUI layout updates
    47   val load_delay = Time.seconds(0.5)  // file load operations (new buffers etc.)
    48   val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
    49   val prune_size = 0  // size of retained history
    50 
    51 
    52   /* pervasive event buses */
    53 
    54   val global_settings = new Event_Bus[Session.Global_Settings.type]
    55   val caret_focus = new Event_Bus[Session.Caret_Focus.type]
    56   val assignments = new Event_Bus[Session.Assignment.type]
    57   val commands_changed = new Event_Bus[Session.Commands_Changed]
    58   val phase_changed = new Event_Bus[Session.Phase]
    59   val syslog_messages = new Event_Bus[Isabelle_Process.Result]
    60   val raw_output_messages = new Event_Bus[Isabelle_Process.Result]
    61   val raw_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
    62 
    63 
    64 
    65   /** buffered command changes (delay_first discipline) **/
    66 
    67   //{{{
    68   private case object Stop
    69 
    70   private val (_, commands_changed_buffer) =
    71     Simple_Thread.actor("commands_changed_buffer", daemon = true)
    72   {
    73     var finished = false
    74     while (!finished) {
    75       receive {
    76         case Stop => finished = true; reply(())
    77         case changed: Session.Commands_Changed => commands_changed.event(changed)
    78         case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad)
    79       }
    80     }
    81   }
    82   //}}}
    83 
    84 
    85 
    86   /** main protocol actor **/
    87 
    88   /* global state */
    89 
    90   @volatile var verbose: Boolean = false
    91 
    92   @volatile private var syntax = new Outer_Syntax
    93   def current_syntax(): Outer_Syntax = syntax
    94 
    95   @volatile private var reverse_syslog = List[XML.Elem]()
    96   def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
    97 
    98   @volatile private var _phase: Session.Phase = Session.Inactive
    99   private def phase_=(new_phase: Session.Phase)
   100   {
   101     _phase = new_phase
   102     phase_changed.event(new_phase)
   103   }
   104   def phase = _phase
   105   def is_ready: Boolean = phase == Session.Ready
   106 
   107   private val global_state = new Volatile(Document.State.init)
   108   def current_state(): Document.State = global_state()
   109 
   110   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
   111       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
   112     global_state().snapshot(name, pending_edits)
   113 
   114 
   115   /* theory files */
   116 
   117   def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text =
   118   {
   119     def norm_import(s: String): String =
   120     {
   121       val thy_name = Thy_Header.base_name(s)
   122       if (thy_load.is_loaded(thy_name)) thy_name
   123       else thy_load.append(name.dir, Thy_Header.thy_path(Path.explode(s)))
   124     }
   125     def norm_use(s: String): String = thy_load.append(name.dir, Path.explode(s))
   126 
   127     val header1: Document.Node_Header =
   128       header match {
   129         case Exn.Res(Thy_Header(thy_name, _, _))
   130         if (thy_load.is_loaded(thy_name)) =>
   131           Exn.Exn(ERROR("Attempt to update loaded theory " + quote(thy_name)))
   132         case _ => Document.Node.norm_header(norm_import, norm_use, header)
   133       }
   134     (name, Document.Node.Header(header1))
   135   }
   136 
   137 
   138   /* actor messages */
   139 
   140   private case class Start(timeout: Time, args: List[String])
   141   private case object Cancel_Execution
   142   private case class Init_Node(name: Document.Node.Name,
   143     header: Document.Node_Header, perspective: Text.Perspective, text: String)
   144   private case class Edit_Node(name: Document.Node.Name,
   145     header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
   146   private case class Change_Node(
   147     name: Document.Node.Name,
   148     doc_edits: List[Document.Edit_Command],
   149     previous: Document.Version,
   150     version: Document.Version)
   151   private case class Messages(msgs: List[Isabelle_Process.Message])
   152 
   153   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   154   {
   155     val this_actor = self
   156 
   157     var prune_next = System.currentTimeMillis() + prune_delay.ms
   158 
   159 
   160     /* buffered prover messages */
   161 
   162     object receiver
   163     {
   164       private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
   165 
   166       def flush(): Unit = synchronized {
   167         if (!buffer.isEmpty) {
   168           val msgs = buffer.toList
   169           this_actor ! Messages(msgs)
   170           buffer = new mutable.ListBuffer[Isabelle_Process.Message]
   171         }
   172       }
   173       def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
   174         buffer += msg
   175         msg match {
   176           case result: Isabelle_Process.Result if result.is_raw => flush()
   177           case _ =>
   178         }
   179       }
   180 
   181       private val timer = new Timer("session_actor.receiver", true)
   182       timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
   183 
   184       def cancel() { timer.cancel() }
   185     }
   186 
   187     var prover: Option[Isabelle_Process with Isar_Document] = None
   188 
   189 
   190     /* delayed command changes */
   191 
   192     object commands_changed_delay
   193     {
   194       private var changed_nodes: Set[Document.Node.Name] = Set.empty
   195       private var changed_commands: Set[Command] = Set.empty
   196       private def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty
   197 
   198       private var flush_time: Option[Long] = None
   199 
   200       def flush_timeout: Long =
   201         flush_time match {
   202           case None => 5000L
   203           case Some(time) => (time - System.currentTimeMillis()) max 0
   204         }
   205 
   206       def flush()
   207       {
   208         if (changed)
   209           commands_changed_buffer ! Session.Commands_Changed(changed_nodes, changed_commands)
   210         changed_nodes = Set.empty
   211         changed_commands = Set.empty
   212         flush_time = None
   213       }
   214 
   215       def invoke(command: Command)
   216       {
   217         changed_nodes += command.node_name
   218         changed_commands += command
   219         val now = System.currentTimeMillis()
   220         flush_time match {
   221           case None => flush_time = Some(now + output_delay.ms)
   222           case Some(time) => if (now >= time) flush()
   223         }
   224       }
   225     }
   226 
   227 
   228     /* perspective */
   229 
   230     def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective)
   231     {
   232       val previous = global_state().tip_version
   233       val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
   234 
   235       val text_edits: List[Document.Edit_Text] =
   236         List((name, Document.Node.Perspective(text_perspective)))
   237       val change =
   238         global_state.change_yield(
   239           _.continue_history(Future.value(previous), text_edits, Future.value(version)))
   240 
   241       val assignment = global_state().the_assignment(previous).check_finished
   242       global_state.change(_.define_version(version, assignment))
   243       global_state.change_yield(_.assign(version.id, Document.no_assign))
   244 
   245       prover.get.update_perspective(previous.id, version.id, name, perspective)
   246     }
   247 
   248 
   249     /* incoming edits */
   250 
   251     def handle_edits(name: Document.Node.Name,
   252         header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
   253     //{{{
   254     {
   255       val syntax = current_syntax()
   256       val previous = global_state().history.tip.version
   257 
   258       prover.get.cancel_execution()
   259 
   260       val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
   261       val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
   262       val change =
   263         global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2)))
   264 
   265       result.map {
   266         case (doc_edits, _) =>
   267           assignments.await { global_state().is_assigned(previous.get_finished) }
   268           this_actor ! Change_Node(name, doc_edits, previous.join, change.version.join)
   269       }
   270     }
   271     //}}}
   272 
   273 
   274     /* exec state assignment */
   275 
   276     def handle_assign(id: Document.Version_ID, assign: Document.Assign)
   277     //{{{
   278     {
   279       val cmds = global_state.change_yield(_.assign(id, assign))
   280       for (cmd <- cmds) commands_changed_delay.invoke(cmd)
   281       assignments.event(Session.Assignment)
   282     }
   283     //}}}
   284 
   285 
   286     /* removed versions */
   287 
   288     def handle_removed(removed: List[Document.Version_ID])
   289     //{{{
   290     {
   291       global_state.change(_.removed_versions(removed))
   292     }
   293     //}}}
   294 
   295 
   296     /* resulting changes */
   297 
   298     def handle_change(change: Change_Node)
   299     //{{{
   300     {
   301       val previous = change.previous
   302       val version = change.version
   303       val name = change.name
   304       val doc_edits = change.doc_edits
   305 
   306       def id_command(command: Command)
   307       {
   308         if (!global_state().defined_command(command.id)) {
   309           global_state.change(_.define_command(command))
   310           prover.get.define_command(command)
   311         }
   312       }
   313       doc_edits foreach {
   314         case (_, edit) =>
   315           edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
   316       }
   317 
   318       val assignment = global_state().the_assignment(previous).check_finished
   319       global_state.change(_.define_version(version, assignment))
   320       prover.get.update(previous.id, version.id, doc_edits)
   321     }
   322     //}}}
   323 
   324 
   325     /* prover results */
   326 
   327     def handle_result(result: Isabelle_Process.Result)
   328     //{{{
   329     {
   330       def bad_result(result: Isabelle_Process.Result)
   331       {
   332         if (verbose)
   333           System.err.println("Ignoring prover result: " + result.message.toString)
   334       }
   335 
   336       result.properties match {
   337         case Position.Id(state_id) if !result.is_raw =>
   338           try {
   339             val st = global_state.change_yield(_.accumulate(state_id, result.message))
   340             commands_changed_delay.invoke(st.command)
   341           }
   342           catch {
   343             case _: Document.State.Fail => bad_result(result)
   344           }
   345         case Markup.Assign_Execs if result.is_raw =>
   346           XML.content(result.body).mkString match {
   347             case Isar_Document.Assign(id, assign) =>
   348               try { handle_assign(id, assign) }
   349               catch { case _: Document.State.Fail => bad_result(result) }
   350             case _ => bad_result(result)
   351           }
   352           // FIXME separate timeout event/message!?
   353           if (prover.isDefined && System.currentTimeMillis() > prune_next) {
   354             val old_versions = global_state.change_yield(_.prune_history(prune_size))
   355             if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
   356             prune_next = System.currentTimeMillis() + prune_delay.ms
   357           }
   358         case Markup.Removed_Versions if result.is_raw =>
   359           XML.content(result.body).mkString match {
   360             case Isar_Document.Removed(removed) =>
   361               try { handle_removed(removed) }
   362               catch { case _: Document.State.Fail => bad_result(result) }
   363             case _ => bad_result(result)
   364           }
   365         case Markup.Invoke_Scala(name, id) if result.is_raw =>
   366           Future.fork {
   367             val arg = XML.content(result.body).mkString
   368             val (tag, res) = Invoke_Scala.method(name, arg)
   369             prover.get.invoke_scala(id, tag, res)
   370           }
   371         case Markup.Cancel_Scala(id) =>
   372           System.err.println("cancel_scala " + id)  // FIXME cancel JVM task
   373         case _ =>
   374           if (result.is_syslog) {
   375             reverse_syslog ::= result.message
   376             if (result.is_ready) {
   377               // FIXME move to ML side (!?)
   378               syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
   379               syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
   380               phase = Session.Ready
   381             }
   382             else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
   383             else if (result.is_exit) phase = Session.Inactive
   384           }
   385           else if (result.is_stdout) { }
   386           else if (result.is_status) {
   387             result.body match {
   388               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   389               case List(Keyword.Keyword_Decl(name)) => syntax += name
   390               case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)
   391               case _ => bad_result(result)
   392             }
   393           }
   394           else bad_result(result)
   395       }
   396     }
   397     //}}}
   398 
   399 
   400     /* main loop */
   401 
   402     //{{{
   403     var finished = false
   404     while (!finished) {
   405       receiveWithin(commands_changed_delay.flush_timeout) {
   406         case TIMEOUT => commands_changed_delay.flush()
   407 
   408         case Start(timeout, args) if prover.isEmpty =>
   409           if (phase == Session.Inactive || phase == Session.Failed) {
   410             phase = Session.Startup
   411             prover =
   412               Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Isar_Document)
   413           }
   414 
   415         case Stop =>
   416           if (phase == Session.Ready) {
   417             global_state.change(_ => Document.State.init)  // FIXME event bus!?
   418             phase = Session.Shutdown
   419             prover.get.terminate
   420             prover = None
   421             phase = Session.Inactive
   422           }
   423           finished = true
   424           receiver.cancel()
   425           reply(())
   426 
   427         case Cancel_Execution if prover.isDefined =>
   428           prover.get.cancel_execution()
   429 
   430         case Init_Node(name, header, perspective, text) if prover.isDefined =>
   431           // FIXME compare with existing node
   432           handle_edits(name, header,
   433             List(Document.Node.Clear(),
   434               Document.Node.Edits(List(Text.Edit.insert(0, text))),
   435               Document.Node.Perspective(perspective)))
   436           reply(())
   437 
   438         case Edit_Node(name, header, perspective, text_edits) if prover.isDefined =>
   439           if (text_edits.isEmpty && global_state().tip_stable &&
   440               perspective.range.stop <= global_state().last_exec_offset(name))
   441             update_perspective(name, perspective)
   442           else
   443             handle_edits(name, header,
   444               List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
   445           reply(())
   446 
   447         case change: Change_Node if prover.isDefined =>
   448           handle_change(change)
   449 
   450         case Messages(msgs) =>
   451           msgs foreach {
   452             case input: Isabelle_Process.Input =>
   453               raw_messages.event(input)
   454 
   455             case result: Isabelle_Process.Result =>
   456               handle_result(result)
   457               if (result.is_syslog) syslog_messages.event(result)
   458               if (result.is_stdout) raw_output_messages.event(result)
   459               raw_messages.event(result)
   460           }
   461 
   462         case bad => System.err.println("session_actor: ignoring bad message " + bad)
   463       }
   464     }
   465     //}}}
   466   }
   467 
   468 
   469   /* actions */
   470 
   471   def start(timeout: Time, args: List[String])
   472   { session_actor ! Start(timeout, args) }
   473 
   474   def start(args: List[String]) { start (Time.seconds(25), args) }
   475 
   476   def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
   477 
   478   def cancel_execution() { session_actor ! Cancel_Execution }
   479 
   480   def init_node(name: Document.Node.Name,
   481     header: Document.Node_Header, perspective: Text.Perspective, text: String)
   482   { session_actor !? Init_Node(name, header, perspective, text) }
   483 
   484   def edit_node(name: Document.Node.Name,
   485     header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
   486   { session_actor !? Edit_Node(name, header, perspective, edits) }
   487 }