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