src/Pure/System/session.scala
author wenzelm
Mon Jul 11 16:48:02 2011 +0200 (2011-07-11)
changeset 43748 c70bd78ec83c
parent 43746 a41f618c641d
child 44156 6aa25b80e1a5
permissions -rw-r--r--
JVM method invocation service via Scala layer;
     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 import java.lang.System
    11 
    12 import scala.actors.TIMEOUT
    13 import scala.actors.Actor
    14 import scala.actors.Actor._
    15 
    16 
    17 object Session
    18 {
    19   /* file store */
    20 
    21   abstract class File_Store
    22   {
    23     def read(path: Path): String
    24   }
    25 
    26 
    27   /* events */
    28 
    29   //{{{
    30   case object Global_Settings
    31   case object Perspective
    32   case object Assignment
    33   case class Commands_Changed(set: Set[Command])
    34 
    35   sealed abstract class Phase
    36   case object Inactive extends Phase
    37   case object Startup extends Phase  // transient
    38   case object Failed extends Phase
    39   case object Ready extends Phase
    40   case object Shutdown extends Phase  // transient
    41   //}}}
    42 }
    43 
    44 
    45 class Session(val file_store: Session.File_Store)
    46 {
    47   /* real time parameters */  // FIXME properties or settings (!?)
    48 
    49   val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
    50   val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
    51   val update_delay = Time.seconds(0.5)  // GUI layout updates
    52 
    53 
    54   /* pervasive event buses */
    55 
    56   val global_settings = new Event_Bus[Session.Global_Settings.type]
    57   val perspective = new Event_Bus[Session.Perspective.type]
    58   val assignments = new Event_Bus[Session.Assignment.type]
    59   val commands_changed = new Event_Bus[Session.Commands_Changed]
    60   val phase_changed = new Event_Bus[Session.Phase]
    61   val raw_messages = new Event_Bus[Isabelle_Process.Message]
    62 
    63 
    64 
    65   /** buffered command changes (delay_first discipline) **/
    66 
    67   //{{{
    68   private case object Stop
    69 
    70   private val (_, command_change_buffer) =
    71     Simple_Thread.actor("command_change_buffer", daemon = true)
    72   {
    73     var changed: Set[Command] = Set()
    74     var flush_time: Option[Long] = None
    75 
    76     def flush_timeout: Long =
    77       flush_time match {
    78         case None => 5000L
    79         case Some(time) => (time - System.currentTimeMillis()) max 0
    80       }
    81 
    82     def flush()
    83     {
    84       if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
    85       changed = Set()
    86       flush_time = None
    87     }
    88 
    89     def invoke()
    90     {
    91       val now = System.currentTimeMillis()
    92       flush_time match {
    93         case None => flush_time = Some(now + output_delay.ms)
    94         case Some(time) => if (now >= time) flush()
    95       }
    96     }
    97 
    98     var finished = false
    99     while (!finished) {
   100       receiveWithin(flush_timeout) {
   101         case command: Command => changed += command; invoke()
   102         case TIMEOUT => flush()
   103         case Stop => finished = true; reply(())
   104         case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
   105       }
   106     }
   107   }
   108   //}}}
   109 
   110 
   111 
   112   /** main protocol actor **/
   113 
   114   /* global state */
   115 
   116   @volatile var verbose: Boolean = false
   117 
   118   @volatile private var loaded_theories: Set[String] = Set()
   119 
   120   @volatile private var syntax = new Outer_Syntax
   121   def current_syntax(): Outer_Syntax = syntax
   122 
   123   @volatile private var reverse_syslog = List[XML.Elem]()
   124   def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
   125 
   126   @volatile private var _phase: Session.Phase = Session.Inactive
   127   private def phase_=(new_phase: Session.Phase)
   128   {
   129     _phase = new_phase
   130     phase_changed.event(new_phase)
   131   }
   132   def phase = _phase
   133   def is_ready: Boolean = phase == Session.Ready
   134 
   135   private val global_state = new Volatile(Document.State.init)
   136   def current_state(): Document.State = global_state()
   137 
   138   def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
   139     global_state().snapshot(name, pending_edits)
   140 
   141 
   142   /* theory files */
   143 
   144   val thy_load = new Thy_Load
   145   {
   146     override def is_loaded(name: String): Boolean =
   147       loaded_theories.contains(name)
   148 
   149     override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
   150     {
   151       val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
   152       if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
   153       val text = Standard_System.read_file(file)
   154       val header = Thy_Header.read(text)
   155       (text, header)
   156     }
   157   }
   158 
   159   val thy_info = new Thy_Info(thy_load)
   160 
   161 
   162   /* actor messages */
   163 
   164   private case class Start(timeout: Time, args: List[String])
   165   private case object Interrupt
   166   private case class Init_Node(name: String, header: Document.Node.Header, text: String)
   167   private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
   168   private case class Change_Node(
   169     name: String,
   170     doc_edits: List[Document.Edit_Command],
   171     header_edits: List[(String, Thy_Header.Header)],
   172     previous: Document.Version,
   173     version: Document.Version)
   174 
   175   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   176   {
   177     val this_actor = self
   178     var prover: Option[Isabelle_Process with Isar_Document] = None
   179 
   180 
   181     /* incoming edits */
   182 
   183     def handle_edits(name: String,
   184         header: Document.Node.Header, edits: List[Option[List[Text.Edit]]])
   185     //{{{
   186     {
   187       val syntax = current_syntax()
   188       val previous = global_state().history.tip.version
   189       val doc_edits = edits.map(edit => (name, edit))
   190       val result = Future.fork {
   191         Thy_Syntax.text_edits(syntax, previous.join, doc_edits, List((name, header)))
   192       }
   193       val change =
   194         global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._3)))
   195 
   196       result.map {
   197         case (doc_edits, header_edits, _) =>
   198           assignments.await { global_state().is_assigned(previous.get_finished) }
   199           this_actor !
   200             Change_Node(name, doc_edits, header_edits, previous.join, change.version.join)
   201       }
   202     }
   203     //}}}
   204 
   205 
   206     /* resulting changes */
   207 
   208     def handle_change(change: Change_Node)
   209     //{{{
   210     {
   211       val previous = change.previous
   212       val version = change.version
   213       val name = change.name
   214       val doc_edits = change.doc_edits
   215       val header_edits = change.header_edits
   216 
   217       var former_assignment = global_state().the_assignment(previous).get_finished
   218       for {
   219         (name, Some(cmd_edits)) <- doc_edits
   220         (prev, None) <- cmd_edits
   221         removed <- previous.nodes(name).commands.get_after(prev)
   222       } former_assignment -= removed
   223 
   224       def id_command(command: Command): Document.Command_ID =
   225       {
   226         if (global_state().lookup_command(command.id).isEmpty) {
   227           global_state.change(_.define_command(command))
   228           prover.get.define_command(command.id, Symbol.encode(command.source))
   229         }
   230         command.id
   231       }
   232       val id_edits =
   233         doc_edits map {
   234           case (name, edits) =>
   235             val ids =
   236               edits.map(_.map { case (c1, c2) => (c1.map(id_command), c2.map(id_command)) })
   237             (name, ids)
   238         }
   239 
   240       global_state.change(_.define_version(version, former_assignment))
   241       prover.get.edit_version(previous.id, version.id, id_edits, header_edits)
   242     }
   243     //}}}
   244 
   245 
   246     /* prover results */
   247 
   248     def handle_result(result: Isabelle_Process.Result)
   249     //{{{
   250     {
   251       def bad_result(result: Isabelle_Process.Result)
   252       {
   253         if (verbose)
   254           System.err.println("Ignoring prover result: " + result.message.toString)
   255       }
   256 
   257       result.properties match {
   258         case Position.Id(state_id) if !result.is_raw =>
   259           try {
   260             val st = global_state.change_yield(_.accumulate(state_id, result.message))
   261             command_change_buffer ! st.command
   262           }
   263           catch {
   264             case _: Document.State.Fail => bad_result(result)
   265           }
   266         case Markup.Invoke_Scala(name, id) if result.is_raw =>
   267           Future.fork {
   268             val arg = XML.content(result.body).mkString
   269             val (tag, res) = Invoke_Scala.method(name, arg)
   270             prover.get.invoke_scala(id, tag, res)
   271           }
   272         case _ =>
   273           if (result.is_syslog) {
   274             reverse_syslog ::= result.message
   275             if (result.is_ready) {
   276               // FIXME move to ML side (!?)
   277               syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
   278               syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
   279               phase = Session.Ready
   280             }
   281             else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
   282             else if (result.is_exit) phase = Session.Inactive
   283           }
   284           else if (result.is_stdout) { }
   285           else if (result.is_status) {
   286             result.body match {
   287               case List(Isar_Document.Assign(id, edits)) =>
   288                 try {
   289                   val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
   290                   for (cmd <- cmds) command_change_buffer ! cmd
   291                   assignments.event(Session.Assignment)
   292                 }
   293                 catch { case _: Document.State.Fail => bad_result(result) }
   294               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   295               case List(Keyword.Keyword_Decl(name)) => syntax += name
   296               case List(Thy_Info.Loaded_Theory(name)) => loaded_theories += name
   297               case _ => bad_result(result)
   298             }
   299           }
   300           else bad_result(result)
   301       }
   302     }
   303     //}}}
   304 
   305 
   306     /* main loop */
   307 
   308     //{{{
   309     var finished = false
   310     while (!finished) {
   311       receive {
   312         case Start(timeout, args) if prover.isEmpty =>
   313           if (phase == Session.Inactive || phase == Session.Failed) {
   314             phase = Session.Startup
   315             prover = Some(new Isabelle_Process(timeout, this_actor, args:_*) with Isar_Document)
   316           }
   317 
   318         case Stop =>
   319           if (phase == Session.Ready) {
   320             global_state.change(_ => Document.State.init)  // FIXME event bus!?
   321             phase = Session.Shutdown
   322             prover.get.terminate
   323             prover = None
   324             phase = Session.Inactive
   325           }
   326           finished = true
   327           reply(())
   328 
   329         case Interrupt if prover.isDefined =>
   330           prover.get.interrupt
   331 
   332         case Init_Node(name, header, text) if prover.isDefined =>
   333           // FIXME compare with existing node
   334           handle_edits(name, header, List(None, Some(List(Text.Edit.insert(0, text)))))
   335           reply(())
   336 
   337         case Edit_Node(name, header, text_edits) if prover.isDefined =>
   338           handle_edits(name, header, List(Some(text_edits)))
   339           reply(())
   340 
   341         case change: Change_Node if prover.isDefined =>
   342           handle_change(change)
   343 
   344         case input: Isabelle_Process.Input =>
   345           raw_messages.event(input)
   346 
   347         case result: Isabelle_Process.Result =>
   348           handle_result(result)
   349           raw_messages.event(result)
   350 
   351         case bad => System.err.println("session_actor: ignoring bad message " + bad)
   352       }
   353     }
   354     //}}}
   355   }
   356 
   357 
   358   /* actions */
   359 
   360   def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) }
   361 
   362   def stop() { command_change_buffer !? Stop; session_actor !? Stop }
   363 
   364   def interrupt() { session_actor ! Interrupt }
   365 
   366   def init_node(name: String, header: Document.Node.Header, text: String)
   367   { session_actor !? Init_Node(name, header, text) }
   368 
   369   def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
   370   { session_actor !? Edit_Node(name, header, edits) }
   371 }