src/Pure/System/session.scala
author wenzelm
Fri, 02 Sep 2011 11:52:13 +0200
changeset 44644 317e4962dd0f
parent 44616 4beeaf2a226d
child 44661 383c9d758a56
permissions -rw-r--r--
clarified define_command: store name as structural information;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 35013
diff changeset
     1
/*  Title:      Pure/System/session.scala
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 35013
diff changeset
     2
    Author:     Makarius
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
     3
    Options:    :folding=explicit:collapseFolds=1:
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 35013
diff changeset
     4
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
     5
Main Isabelle/Scala session, potentially with running prover process.
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 35013
diff changeset
     6
*/
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
     7
34871
e596a0b71f3c incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents: 34859
diff changeset
     8
package isabelle
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
     9
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 43443
diff changeset
    10
import java.lang.System
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    11
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
    12
import scala.actors.TIMEOUT
38226
9d8848d70b0a maintain editor history independently of Swing thread, which is potentially a bottle-neck or might be unavailable (e.g. in batch mode);
wenzelm
parents: 38222
diff changeset
    13
import scala.actors.Actor
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    14
import scala.actors.Actor._
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    15
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
    16
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    17
object Session
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    18
{
34813
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    19
  /* events */
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    20
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    21
  //{{{
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    22
  case object Global_Settings
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    23
  case object Perspective
38849
2f198d107aef session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;
wenzelm
parents: 38848
diff changeset
    24
  case object Assignment
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
    25
  case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command])
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    26
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    27
  sealed abstract class Phase
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    28
  case object Inactive extends Phase
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
    29
  case object Startup extends Phase  // transient
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
    30
  case object Failed extends Phase
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    31
  case object Ready extends Phase
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
    32
  case object Shutdown extends Phase  // transient
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    33
  //}}}
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    34
}
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    35
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    36
44574
24444588fddd actual auto loading of required files;
wenzelm
parents: 44573
diff changeset
    37
class Session(thy_load: Thy_Load)
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    38
{
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    39
  /* real time parameters */  // FIXME properties or settings (!?)
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    40
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    41
  val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    42
  val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    43
  val update_delay = Time.seconds(0.5)  // GUI layout updates
44573
51f8895b9ad9 some dialog for auto loading of required files (still inactive);
wenzelm
parents: 44484
diff changeset
    44
  val load_delay = Time.seconds(0.5)  // file load operations (new buffers etc.)
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    45
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    46
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    47
  /* pervasive event buses */
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    48
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    49
  val global_settings = new Event_Bus[Session.Global_Settings.type]
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    50
  val perspective = new Event_Bus[Session.Perspective.type]
38849
2f198d107aef session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;
wenzelm
parents: 38848
diff changeset
    51
  val assignments = new Event_Bus[Session.Assignment.type]
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    52
  val commands_changed = new Event_Bus[Session.Commands_Changed]
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    53
  val phase_changed = new Event_Bus[Session.Phase]
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43720
diff changeset
    54
  val raw_messages = new Event_Bus[Isabelle_Process.Message]
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    55
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    56
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    57
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    58
  /** buffered command changes (delay_first discipline) **/
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    59
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    60
  //{{{
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    61
  private case object Stop
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    62
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39528
diff changeset
    63
  private val (_, command_change_buffer) =
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39528
diff changeset
    64
    Simple_Thread.actor("command_change_buffer", daemon = true)
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    65
  {
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
    66
    var changed_nodes: Set[Document.Node.Name] = Set.empty
44608
76c2e3ddc183 tuned Commands_Changed: cover nodes as well;
wenzelm
parents: 44582
diff changeset
    67
    var changed_commands: Set[Command] = Set.empty
76c2e3ddc183 tuned Commands_Changed: cover nodes as well;
wenzelm
parents: 44582
diff changeset
    68
    def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty
76c2e3ddc183 tuned Commands_Changed: cover nodes as well;
wenzelm
parents: 44582
diff changeset
    69
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    70
    var flush_time: Option[Long] = None
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    71
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    72
    def flush_timeout: Long =
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    73
      flush_time match {
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    74
        case None => 5000L
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40566
diff changeset
    75
        case Some(time) => (time - System.currentTimeMillis()) max 0
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    76
      }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    77
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    78
    def flush()
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    79
    {
44608
76c2e3ddc183 tuned Commands_Changed: cover nodes as well;
wenzelm
parents: 44582
diff changeset
    80
      if (changed)
76c2e3ddc183 tuned Commands_Changed: cover nodes as well;
wenzelm
parents: 44582
diff changeset
    81
        commands_changed.event(Session.Commands_Changed(changed_nodes, changed_commands))
76c2e3ddc183 tuned Commands_Changed: cover nodes as well;
wenzelm
parents: 44582
diff changeset
    82
      changed_nodes = Set.empty
76c2e3ddc183 tuned Commands_Changed: cover nodes as well;
wenzelm
parents: 44582
diff changeset
    83
      changed_commands = Set.empty
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    84
      flush_time = None
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    85
    }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    86
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    87
    def invoke()
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    88
    {
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40566
diff changeset
    89
      val now = System.currentTimeMillis()
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    90
      flush_time match {
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40566
diff changeset
    91
        case None => flush_time = Some(now + output_delay.ms)
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    92
        case Some(time) => if (now >= time) flush()
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    93
      }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    94
    }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    95
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    96
    var finished = false
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    97
    while (!finished) {
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    98
      receiveWithin(flush_timeout) {
44608
76c2e3ddc183 tuned Commands_Changed: cover nodes as well;
wenzelm
parents: 44582
diff changeset
    99
        case command: Command =>
76c2e3ddc183 tuned Commands_Changed: cover nodes as well;
wenzelm
parents: 44582
diff changeset
   100
          changed_nodes += command.node_name
76c2e3ddc183 tuned Commands_Changed: cover nodes as well;
wenzelm
parents: 44582
diff changeset
   101
          changed_commands += command
76c2e3ddc183 tuned Commands_Changed: cover nodes as well;
wenzelm
parents: 44582
diff changeset
   102
          invoke()
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   103
        case TIMEOUT => flush()
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   104
        case Stop => finished = true; reply(())
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   105
        case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   106
      }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   107
    }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   108
  }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   109
  //}}}
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   110
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   111
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   112
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   113
  /** main protocol actor **/
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   114
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   115
  /* global state */
43644
ea08ce1c314b tuned signature;
wenzelm
parents: 43553
diff changeset
   116
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   117
  @volatile var verbose: Boolean = false
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   118
43695
5130dfe1b7be simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents: 43673
diff changeset
   119
  @volatile private var syntax = new Outer_Syntax
38569
9d480f6a2589 tuned signatures;
wenzelm
parents: 38446
diff changeset
   120
  def current_syntax(): Outer_Syntax = syntax
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   121
39626
a5d0bcfb95a3 manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents: 39625
diff changeset
   122
  @volatile private var reverse_syslog = List[XML.Elem]()
39629
08eb2730a8a1 tuned signature;
wenzelm
parents: 39626
diff changeset
   123
  def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
39626
a5d0bcfb95a3 manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents: 39625
diff changeset
   124
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   125
  @volatile private var _phase: Session.Phase = Session.Inactive
39633
26a28110ece5 simplified Session.Phase;
wenzelm
parents: 39630
diff changeset
   126
  private def phase_=(new_phase: Session.Phase)
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   127
  {
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   128
    _phase = new_phase
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   129
    phase_changed.event(new_phase)
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   130
  }
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   131
  def phase = _phase
43553
df80747342cb proper tokens only if session is ready;
wenzelm
parents: 43520
diff changeset
   132
  def is_ready: Boolean = phase == Session.Ready
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   133
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   134
  private val global_state = new Volatile(Document.State.init)
43719
ba1b2c918c32 tuned signature;
wenzelm
parents: 43718
diff changeset
   135
  def current_state(): Document.State = global_state()
34816
d33312514220 maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents: 34815
diff changeset
   136
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   137
  def snapshot(name: Document.Node.Name, pending_edits: List[Text.Edit]): Document.Snapshot =
43719
ba1b2c918c32 tuned signature;
wenzelm
parents: 43718
diff changeset
   138
    global_state().snapshot(name, pending_edits)
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   139
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   140
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   141
  /* theory files */
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   142
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   143
  def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text =
44442
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   144
  {
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   145
    def norm_import(s: String): String =
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   146
    {
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   147
      val thy_name = Thy_Header.base_name(s)
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   148
      if (thy_load.is_loaded(thy_name)) thy_name
44616
4beeaf2a226d tuned signature;
wenzelm
parents: 44615
diff changeset
   149
      else thy_load.append(name.dir, Thy_Header.thy_path(Path.explode(s)))
44442
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   150
    }
44616
4beeaf2a226d tuned signature;
wenzelm
parents: 44615
diff changeset
   151
    def norm_use(s: String): String = thy_load.append(name.dir, Path.explode(s))
44442
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   152
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   153
    val header1: Document.Node_Header =
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   154
      header match {
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   155
        case Exn.Res(Thy_Header(thy_name, _, _))
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   156
        if (thy_load.is_loaded(thy_name)) =>
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   157
          Exn.Exn(ERROR("Attempt to update loaded theory " + quote(thy_name)))
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   158
        case _ => Document.Node.norm_header(norm_import, norm_use, header)
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   159
      }
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   160
    (name, Document.Node.Header(header1))
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   161
  }
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   162
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   163
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   164
  /* actor messages */
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   165
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   166
  private case class Start(timeout: Time, args: List[String])
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   167
  private case object Interrupt
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   168
  private case class Init_Node(name: Document.Node.Name,
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   169
    header: Document.Node_Header, perspective: Text.Perspective, text: String)
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   170
  private case class Edit_Node(name: Document.Node.Name,
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   171
    header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   172
  private case class Change_Node(
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   173
    name: Document.Node.Name,
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   174
    doc_edits: List[Document.Edit_Command],
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   175
    previous: Document.Version,
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   176
    version: Document.Version)
41534
f36cb6f233bd less verbosity;
wenzelm
parents: 40848
diff changeset
   177
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39528
diff changeset
   178
  private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
38639
f642faca303e main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents: 38569
diff changeset
   179
  {
43648
e32de528b5ef more explicit edit_node vs. init_node;
wenzelm
parents: 43647
diff changeset
   180
    val this_actor = self
43649
a912f0b02359 eliminated null;
wenzelm
parents: 43648
diff changeset
   181
    var prover: Option[Isabelle_Process with Isar_Document] = None
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   182
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   183
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   184
    /* perspective */
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   185
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   186
    def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective)
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   187
    {
44475
709e1d671483 tuned signature;
wenzelm
parents: 44446
diff changeset
   188
      val previous = global_state().tip_version
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   189
      val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   190
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   191
      val text_edits: List[Document.Edit_Text] =
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   192
        List((name, Document.Node.Perspective(text_perspective)))
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   193
      val change =
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   194
        global_state.change_yield(
44446
f9334afb6945 misc tuning and simplification;
wenzelm
parents: 44442
diff changeset
   195
          _.continue_history(Future.value(previous), text_edits, Future.value(version)))
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   196
44477
086bb1083552 maintain last_execs assignment on Scala side;
wenzelm
parents: 44476
diff changeset
   197
      val assignment = global_state().the_assignment(previous).check_finished
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   198
      global_state.change(_.define_version(version, assignment))
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44475
diff changeset
   199
      global_state.change_yield(_.assign(version.id, Document.no_assign))
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   200
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   201
      prover.get.update_perspective(previous.id, version.id, name, perspective)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   202
    }
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   203
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   204
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   205
    /* incoming edits */
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   206
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   207
    def handle_edits(name: Document.Node.Name,
44384
8f6054a63f96 some support for editor perspective;
wenzelm
parents: 44383
diff changeset
   208
        header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   209
    //{{{
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   210
    {
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   211
      val syntax = current_syntax()
43719
ba1b2c918c32 tuned signature;
wenzelm
parents: 43718
diff changeset
   212
      val previous = global_state().history.tip.version
44185
05641edb5d30 provide node header via Scala layer;
wenzelm
parents: 44183
diff changeset
   213
44612
990ac978854c explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents: 44608
diff changeset
   214
      prover.get.cancel_execution()
990ac978854c explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
wenzelm
parents: 44608
diff changeset
   215
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   216
      val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
44185
05641edb5d30 provide node header via Scala layer;
wenzelm
parents: 44183
diff changeset
   217
      val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   218
      val change =
44446
f9334afb6945 misc tuning and simplification;
wenzelm
parents: 44442
diff changeset
   219
        global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2)))
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   220
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   221
      result.map {
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   222
        case (doc_edits, _) =>
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   223
          assignments.await { global_state().is_assigned(previous.get_finished) }
44157
a21d3e1e64fd uniform treatment of header edits as document edits;
wenzelm
parents: 44156
diff changeset
   224
          this_actor ! Change_Node(name, doc_edits, previous.join, change.version.join)
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   225
      }
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   226
    }
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   227
    //}}}
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   228
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   229
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   230
    /* exec state assignment */
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   231
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44475
diff changeset
   232
    def handle_assign(id: Document.Version_ID, assign: Document.Assign)
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   233
    //{{{
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   234
    {
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44475
diff changeset
   235
      val cmds = global_state.change_yield(_.assign(id, assign))
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   236
      for (cmd <- cmds) command_change_buffer ! cmd
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   237
      assignments.event(Session.Assignment)
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   238
    }
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   239
    //}}}
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   240
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   241
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   242
    /* resulting changes */
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   243
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   244
    def handle_change(change: Change_Node)
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   245
    //{{{
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   246
    {
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   247
      val previous = change.previous
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   248
      val version = change.version
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   249
      val name = change.name
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   250
      val doc_edits = change.doc_edits
38366
fea82d1add74 simplified/clarified Change: transition prev --edits--> result, based on futures;
wenzelm
parents: 38365
diff changeset
   251
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   252
      def id_command(command: Command)
43720
wenzelm
parents: 43719
diff changeset
   253
      {
44582
479c07072992 tuned signature;
wenzelm
parents: 44574
diff changeset
   254
        if (!global_state().defined_command(command.id)) {
43720
wenzelm
parents: 43719
diff changeset
   255
          global_state.change(_.define_command(command))
44644
317e4962dd0f clarified define_command: store name as structural information;
wenzelm
parents: 44616
diff changeset
   256
          prover.get.define_command(command)
43720
wenzelm
parents: 43719
diff changeset
   257
        }
wenzelm
parents: 43719
diff changeset
   258
      }
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   259
      doc_edits foreach {
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   260
        case (_, edit) =>
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   261
          edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   262
      }
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   263
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   264
      val assignment = global_state().the_assignment(previous).check_finished
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   265
      global_state.change(_.define_version(version, assignment))
44481
bb42bc831570 tuned signature;
wenzelm
parents: 44479
diff changeset
   266
      prover.get.update(previous.id, version.id, doc_edits)
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   267
    }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   268
    //}}}
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   269
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   270
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   271
    /* prover results */
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   272
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   273
    def handle_result(result: Isabelle_Process.Result)
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   274
    //{{{
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   275
    {
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   276
      def bad_result(result: Isabelle_Process.Result)
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   277
      {
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   278
        if (verbose)
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   279
          System.err.println("Ignoring prover result: " + result.message.toString)
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   280
      }
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   281
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38639
diff changeset
   282
      result.properties match {
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   283
        case Position.Id(state_id) if !result.is_raw =>
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   284
          try {
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   285
            val st = global_state.change_yield(_.accumulate(state_id, result.message))
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   286
            command_change_buffer ! st.command
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   287
          }
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   288
          catch {
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   289
            case _: Document.State.Fail => bad_result(result)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   290
          }
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   291
        case Markup.Invoke_Scala(name, id) if result.is_raw =>
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   292
          Future.fork {
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   293
            val arg = XML.content(result.body).mkString
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   294
            val (tag, res) = Invoke_Scala.method(name, arg)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   295
            prover.get.invoke_scala(id, tag, res)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   296
          }
44298
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 44225
diff changeset
   297
        case Markup.Cancel_Scala(id) =>
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 44225
diff changeset
   298
          System.err.println("cancel_scala " + id)  // FIXME cancel JVM task
38722
ba31936497c2 organized markup properties via apply/unapply patterns;
wenzelm
parents: 38639
diff changeset
   299
        case _ =>
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   300
          if (result.is_syslog) {
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   301
            reverse_syslog ::= result.message
40533
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 40479
diff changeset
   302
            if (result.is_ready) {
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   303
              // FIXME move to ML side (!?)
40533
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 40479
diff changeset
   304
              syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 40479
diff changeset
   305
              syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 40479
diff changeset
   306
              phase = Session.Ready
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 40479
diff changeset
   307
            }
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   308
            else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
39696
f4da0428dc78 more informative Session.Phase;
wenzelm
parents: 39633
diff changeset
   309
            else if (result.is_exit) phase = Session.Inactive
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   310
          }
39626
a5d0bcfb95a3 manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents: 39625
diff changeset
   311
          else if (result.is_stdout) { }
39625
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39593
diff changeset
   312
          else if (result.is_status) {
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   313
            result.body match {
44476
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44475
diff changeset
   314
              case List(Isar_Document.Assign(id, assign)) =>
e8a87398f35d propagate information about last command with exec state assignment through document model;
wenzelm
parents: 44475
diff changeset
   315
                try { handle_assign(id, assign) }
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38413
diff changeset
   316
                catch { case _: Document.State.Fail => bad_result(result) }
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   317
              case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   318
              case List(Keyword.Keyword_Decl(name)) => syntax += name
44574
24444588fddd actual auto loading of required files;
wenzelm
parents: 44573
diff changeset
   319
              case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)
39625
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39593
diff changeset
   320
              case _ => bad_result(result)
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   321
            }
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   322
          }
39625
fb0c851e4f9d tuned prover message categorization;
wenzelm
parents: 39593
diff changeset
   323
          else bad_result(result)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   324
      }
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   325
    }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   326
    //}}}
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   327
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   328
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   329
    /* main loop */
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   330
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   331
    //{{{
38639
f642faca303e main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents: 38569
diff changeset
   332
    var finished = false
f642faca303e main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents: 38569
diff changeset
   333
    while (!finished) {
f642faca303e main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents: 38569
diff changeset
   334
      receive {
43649
a912f0b02359 eliminated null;
wenzelm
parents: 43648
diff changeset
   335
        case Start(timeout, args) if prover.isEmpty =>
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   336
          if (phase == Session.Inactive || phase == Session.Failed) {
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   337
            phase = Session.Startup
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
   338
            prover = Some(new Isabelle_Process(timeout, this_actor, args:_*) with Isar_Document)
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   339
          }
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   340
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   341
        case Stop =>
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   342
          if (phase == Session.Ready) {
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   343
            global_state.change(_ => Document.State.init)  // FIXME event bus!?
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   344
            phase = Session.Shutdown
43649
a912f0b02359 eliminated null;
wenzelm
parents: 43648
diff changeset
   345
            prover.get.terminate
43717
c3ddb5537a2f more precise treatment of prover definedness;
wenzelm
parents: 43716
diff changeset
   346
            prover = None
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   347
            phase = Session.Inactive
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   348
          }
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   349
          finished = true
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   350
          reply(())
38850
5c3e5c548f12 session_actor: ignore spurious TIMEOUT (again) -- probably stemming from earlier use of receiveWithin;
wenzelm
parents: 38849
diff changeset
   351
43717
c3ddb5537a2f more precise treatment of prover definedness;
wenzelm
parents: 43716
diff changeset
   352
        case Interrupt if prover.isDefined =>
c3ddb5537a2f more precise treatment of prover definedness;
wenzelm
parents: 43716
diff changeset
   353
          prover.get.interrupt
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   354
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   355
        case Init_Node(name, header, perspective, text) if prover.isDefined =>
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   356
          // FIXME compare with existing node
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   357
          handle_edits(name, header,
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   358
            List(Document.Node.Clear(),
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   359
              Document.Node.Edits(List(Text.Edit.insert(0, text))),
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   360
              Document.Node.Perspective(perspective)))
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   361
          reply(())
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   362
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   363
        case Edit_Node(name, header, perspective, text_edits) if prover.isDefined =>
44484
470f2ee5950e tuned Session.edit_node: update_perspective based on last_exec_offset;
wenzelm
parents: 44481
diff changeset
   364
          if (text_edits.isEmpty && global_state().tip_stable &&
470f2ee5950e tuned Session.edit_node: update_perspective based on last_exec_offset;
wenzelm
parents: 44481
diff changeset
   365
              perspective.range.stop <= global_state().last_exec_offset(name))
470f2ee5950e tuned Session.edit_node: update_perspective based on last_exec_offset;
wenzelm
parents: 44481
diff changeset
   366
            update_perspective(name, perspective)
470f2ee5950e tuned Session.edit_node: update_perspective based on last_exec_offset;
wenzelm
parents: 44481
diff changeset
   367
          else
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   368
            handle_edits(name, header,
44436
546adfa8a6fc update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents: 44385
diff changeset
   369
              List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
43718
4a4ca9e4a14b clarified propagation of node name and header;
wenzelm
parents: 43717
diff changeset
   370
          reply(())
4a4ca9e4a14b clarified propagation of node name and header;
wenzelm
parents: 43717
diff changeset
   371
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   372
        case change: Change_Node if prover.isDefined =>
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   373
          handle_change(change)
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   374
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43720
diff changeset
   375
        case input: Isabelle_Process.Input =>
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43720
diff changeset
   376
          raw_messages.event(input)
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43720
diff changeset
   377
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   378
        case result: Isabelle_Process.Result =>
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   379
          handle_result(result)
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43720
diff changeset
   380
          raw_messages.event(result)
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   381
43717
c3ddb5537a2f more precise treatment of prover definedness;
wenzelm
parents: 43716
diff changeset
   382
        case bad => System.err.println("session_actor: ignoring bad message " + bad)
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   383
      }
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   384
    }
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   385
    //}}}
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   386
  }
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   387
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   388
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   389
  /* actions */
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   390
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40566
diff changeset
   391
  def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) }
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   392
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   393
  def stop() { command_change_buffer !? Stop; session_actor !? Stop }
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   394
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   395
  def interrupt() { session_actor ! Interrupt }
43648
e32de528b5ef more explicit edit_node vs. init_node;
wenzelm
parents: 43647
diff changeset
   396
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   397
  def init_node(name: Document.Node.Name,
44385
e7fdb008aa7d propagate editor perspective through document model;
wenzelm
parents: 44384
diff changeset
   398
    header: Document.Node_Header, perspective: Text.Perspective, text: String)
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   399
  { session_actor !? Init_Node(name, header, perspective, text) }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   400
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   401
  def edit_node(name: Document.Node.Name,
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   402
    header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   403
  { session_actor !? Edit_Node(name, header, perspective, edits) }
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   404
}