src/Pure/System/session.scala
author wenzelm
Fri, 07 Sep 2012 15:00:03 +0200
changeset 49196 1d63ceb0d177
parent 48999 3bdebf6ad9da
child 49250 332ab3748350
permissions -rw-r--r--
postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
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
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
    10
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 43443
diff changeset
    11
import java.lang.System
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
    12
import java.util.{Timer, TimerTask}
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    13
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
    14
import scala.collection.mutable
46771
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
    15
import scala.collection.immutable.Queue
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
    16
import scala.actors.TIMEOUT
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    17
import scala.actors.Actor._
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    18
34815
6bae73cd8e33 unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents: 34813
diff changeset
    19
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    20
object Session
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    21
{
34813
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    22
  /* events */
f0107bc96961 more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents: 34810
diff changeset
    23
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    24
  //{{{
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    25
  case object Global_Settings
44805
48a5c104d434 clarified terminology;
wenzelm
parents: 44775
diff changeset
    26
  case object Caret_Focus
49196
1d63ceb0d177 postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents: 48999
diff changeset
    27
  case class Raw_Edits(edits: List[Document.Edit_Text])
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
    28
  case class Commands_Changed(
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
    29
    assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    30
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    31
  sealed abstract class Phase
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    32
  case object Inactive extends Phase
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
    33
  case object Startup extends Phase  // transient
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
    34
  case object Failed extends Phase
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    35
  case object Ready extends Phase
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
    36
  case object Shutdown extends Phase  // transient
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    37
  //}}}
34791
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    38
}
b97d5b38dea4 explicit object Session.Global_Settings;
wenzelm
parents: 34780
diff changeset
    39
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    40
48870
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents: 48794
diff changeset
    41
class Session(val thy_load: Thy_Load)
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
    42
{
47653
4605d4341b8b some builtin session timing;
wenzelm
parents: 47629
diff changeset
    43
  /* global flags */
4605d4341b8b some builtin session timing;
wenzelm
parents: 47629
diff changeset
    44
4605d4341b8b some builtin session timing;
wenzelm
parents: 47629
diff changeset
    45
  @volatile var timing: Boolean = false
4605d4341b8b some builtin session timing;
wenzelm
parents: 47629
diff changeset
    46
  @volatile var verbose: Boolean = false
4605d4341b8b some builtin session timing;
wenzelm
parents: 47629
diff changeset
    47
4605d4341b8b some builtin session timing;
wenzelm
parents: 47629
diff changeset
    48
46771
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
    49
  /* tuning parameters */  // FIXME properties or settings (!?)
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    50
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
    51
  val message_delay = Time.seconds(0.01)  // prover messages
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    52
  val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    53
  val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    54
  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
    55
  val load_delay = Time.seconds(0.5)  // file load operations (new buffers etc.)
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
    56
  val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
    57
  val prune_size = 0  // size of retained history
46771
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
    58
  val syslog_limit = 100
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    59
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37689
diff changeset
    60
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    61
  /* pervasive event buses */
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    62
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    63
  val global_settings = new Event_Bus[Session.Global_Settings.type]
44805
48a5c104d434 clarified terminology;
wenzelm
parents: 44775
diff changeset
    64
  val caret_focus = new Event_Bus[Session.Caret_Focus.type]
49196
1d63ceb0d177 postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents: 48999
diff changeset
    65
  val raw_edits = new Event_Bus[Session.Raw_Edits]
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    66
  val commands_changed = new Event_Bus[Session.Commands_Changed]
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    67
  val phase_changed = new Event_Bus[Session.Phase]
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
    68
  val syslog_messages = new Event_Bus[Isabelle_Process.Output]
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
    69
  val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
    70
  val all_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    71
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    72
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
    73
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    74
  /** 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
    75
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
    76
  //{{{
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    77
  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
    78
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
    79
  private val (_, commands_changed_buffer) =
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
    80
    Simple_Thread.actor("commands_changed_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
    81
  {
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    82
    var finished = false
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    83
    while (!finished) {
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
    84
      receive {
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
    85
        case Stop => finished = true; reply(())
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
    86
        case changed: Session.Commands_Changed => commands_changed.event(changed)
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
    87
        case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad)
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    88
      }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    89
    }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    90
  }
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    91
  //}}}
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    92
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
    93
45635
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    94
  /** pipelined change parsing **/
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    95
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    96
  //{{{
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    97
  private case class Text_Edits(
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    98
    previous: Future[Document.Version],
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
    99
    text_edits: List[Document.Edit_Text],
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   100
    version_result: Promise[Document.Version])
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   101
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   102
  private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true)
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   103
  {
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   104
    var finished = false
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   105
    while (!finished) {
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   106
      receive {
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   107
        case Stop => finished = true; reply(())
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   108
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   109
        case Text_Edits(previous, text_edits, version_result) =>
45635
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   110
          val prev = previous.get_finished
47653
4605d4341b8b some builtin session timing;
wenzelm
parents: 47629
diff changeset
   111
          val (doc_edits, version) =
4605d4341b8b some builtin session timing;
wenzelm
parents: 47629
diff changeset
   112
            Timing.timeit("Thy_Syntax.text_edits", timing) {
48870
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents: 48794
diff changeset
   113
              Thy_Syntax.text_edits(thy_load.base_syntax, prev, text_edits)
47653
4605d4341b8b some builtin session timing;
wenzelm
parents: 47629
diff changeset
   114
            }
45635
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   115
          version_result.fulfill(version)
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   116
          sender ! Change(doc_edits, prev, version)
45635
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   117
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   118
        case bad => System.err.println("change_parser: ignoring bad message " + bad)
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   119
      }
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   120
    }
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   121
  }
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   122
  //}}}
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   123
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   124
47653
4605d4341b8b some builtin session timing;
wenzelm
parents: 47629
diff changeset
   125
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   126
  /** main protocol actor **/
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   127
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   128
  /* global state */
43644
ea08ce1c314b tuned signature;
wenzelm
parents: 43553
diff changeset
   129
46771
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
   130
  private val syslog = Volatile(Queue.empty[XML.Elem])
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
   131
  def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
39626
a5d0bcfb95a3 manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents: 39625
diff changeset
   132
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   133
  @volatile private var _phase: Session.Phase = Session.Inactive
39633
26a28110ece5 simplified Session.Phase;
wenzelm
parents: 39630
diff changeset
   134
  private def phase_=(new_phase: Session.Phase)
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   135
  {
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   136
    _phase = new_phase
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   137
    phase_changed.event(new_phase)
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   138
  }
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   139
  def phase = _phase
43553
df80747342cb proper tokens only if session is ready;
wenzelm
parents: 43520
diff changeset
   140
  def is_ready: Boolean = phase == Session.Ready
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   141
45248
3b7b64b194ee class Volatile as abstract datatype;
wenzelm
parents: 45158
diff changeset
   142
  private val global_state = Volatile(Document.State.init)
43719
ba1b2c918c32 tuned signature;
wenzelm
parents: 43718
diff changeset
   143
  def current_state(): Document.State = global_state()
46944
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   144
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   145
  def recent_syntax(): Outer_Syntax =
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   146
  {
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   147
    val version = current_state().recent_finished.version.get_finished
48870
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents: 48794
diff changeset
   148
    if (version.is_init) thy_load.base_syntax
46944
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   149
    else version.syntax
9fc22eb6408c more recent recent_syntax, e.g. relevant for document rendering during startup;
wenzelm
parents: 46942
diff changeset
   150
  }
34816
d33312514220 maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents: 34815
diff changeset
   151
44960
640c2b957f16 graph traversal in topological order;
wenzelm
parents: 44953
diff changeset
   152
  def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
640c2b957f16 graph traversal in topological order;
wenzelm
parents: 44953
diff changeset
   153
      pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
43719
ba1b2c918c32 tuned signature;
wenzelm
parents: 43718
diff changeset
   154
    global_state().snapshot(name, pending_edits)
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   155
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   156
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   157
  /* theory files */
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   158
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48422
diff changeset
   159
  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
   160
  {
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48422
diff changeset
   161
    val header1 =
48870
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents: 48794
diff changeset
   162
      if (thy_load.loaded_theories(name.theory))
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48422
diff changeset
   163
        header.error("Attempt to update loaded theory " + quote(name.theory))
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48422
diff changeset
   164
      else header
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48422
diff changeset
   165
    (name, Document.Node.Deps(header1))
44442
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   166
  }
cb18e4f09053 clarified norm_header/header_edit -- disallow update of loaded theories;
wenzelm
parents: 44436
diff changeset
   167
43651
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   168
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   169
  /* actor messages */
511df47bcadc some support for theory files within Isabelle/Scala session;
wenzelm
parents: 43649
diff changeset
   170
48870
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents: 48794
diff changeset
   171
  private case class Start(args: List[String])
44775
27930cf6f0f7 added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents: 44734
diff changeset
   172
  private case object Cancel_Execution
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   173
  private case class Change(
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)
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   177
  private case class Messages(msgs: List[Isabelle_Process.Message])
41534
f36cb6f233bd less verbosity;
wenzelm
parents: 40848
diff changeset
   178
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39528
diff changeset
   179
  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
   180
  {
43648
e32de528b5ef more explicit edit_node vs. init_node;
wenzelm
parents: 43647
diff changeset
   181
    val this_actor = self
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   182
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   183
    var prune_next = System.currentTimeMillis() + prune_delay.ms
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   184
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   185
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   186
    /* buffered prover messages */
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   187
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   188
    object receiver
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   189
    {
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   190
      private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   191
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   192
      def flush(): Unit = synchronized {
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   193
        if (!buffer.isEmpty) {
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   194
          val msgs = buffer.toList
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   195
          this_actor ! Messages(msgs)
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   196
          buffer = new mutable.ListBuffer[Isabelle_Process.Message]
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   197
        }
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   198
      }
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   199
      def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   200
        buffer += msg
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   201
        msg match {
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   202
          case output: Isabelle_Process.Output =>
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   203
            if (output.is_syslog)
46771
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
   204
              syslog >> (queue =>
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
   205
                {
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   206
                  val queue1 = queue.enqueue(output.message)
46771
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
   207
                  if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
06a9b24c4a36 explicit syslog_limit reduces danger of low-level message flooding;
wenzelm
parents: 46739
diff changeset
   208
                })
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   209
            if (output.is_protocol) flush()
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   210
          case _ =>
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   211
        }
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   212
      }
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   213
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   214
      private val timer = new Timer("session_actor.receiver", true)
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   215
      timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   216
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   217
      def cancel() { timer.cancel() }
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   218
    }
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   219
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   220
    var prover: Option[Isabelle_Process with Protocol] = None
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   221
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   222
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   223
    /* delayed command changes */
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   224
46570
wenzelm
parents: 46196
diff changeset
   225
    object delay_commands_changed
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   226
    {
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   227
      private var changed_assignment: Boolean = false
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   228
      private var changed_nodes: Set[Document.Node.Name] = Set.empty
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   229
      private var changed_commands: Set[Command] = Set.empty
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   230
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   231
      private var flush_time: Option[Long] = None
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   232
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   233
      def flush_timeout: Long =
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   234
        flush_time match {
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   235
          case None => 5000L
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   236
          case Some(time) => (time - System.currentTimeMillis()) max 0
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   237
        }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   238
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   239
      def flush()
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   240
      {
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   241
        if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty)
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   242
          commands_changed_buffer !
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   243
            Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands)
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   244
        changed_assignment = false
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   245
        changed_nodes = Set.empty
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   246
        changed_commands = Set.empty
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   247
        flush_time = None
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   248
      }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   249
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   250
      def invoke(assign: Boolean, commands: List[Command])
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   251
      {
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   252
        changed_assignment |= assign
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   253
        for (command <- commands) {
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   254
          changed_nodes += command.node_name
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   255
          changed_commands += command
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   256
        }
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   257
        val now = System.currentTimeMillis()
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   258
        flush_time match {
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   259
          case None => flush_time = Some(now + output_delay.ms)
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   260
          case Some(time) => if (now >= time) flush()
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   261
        }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   262
      }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   263
    }
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   264
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   265
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   266
    /* resulting changes */
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   267
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   268
    def handle_change(change: Change)
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   269
    //{{{
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   270
    {
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   271
      val previous = change.previous
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   272
      val version = change.version
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   273
      val doc_edits = change.doc_edits
38366
fea82d1add74 simplified/clarified Change: transition prev --edits--> result, based on futures;
wenzelm
parents: 38365
diff changeset
   274
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   275
      def id_command(command: Command)
43720
wenzelm
parents: 43719
diff changeset
   276
      {
44582
479c07072992 tuned signature;
wenzelm
parents: 44574
diff changeset
   277
        if (!global_state().defined_command(command.id)) {
46687
7e47ae85e161 tuned signature (in accordance with ML);
wenzelm
parents: 46682
diff changeset
   278
          global_state >> (_.define_command(command))
44644
317e4962dd0f clarified define_command: store name as structural information;
wenzelm
parents: 44616
diff changeset
   279
          prover.get.define_command(command)
43720
wenzelm
parents: 43719
diff changeset
   280
        }
wenzelm
parents: 43719
diff changeset
   281
      }
44383
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   282
      doc_edits foreach {
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   283
        case (_, edit) =>
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   284
          edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
f99906c2a1d3 discontinued redundant Edit_Command_ID;
wenzelm
parents: 44298
diff changeset
   285
      }
43722
9b5dadb0c28d propagate header changes to prover process;
wenzelm
parents: 43721
diff changeset
   286
44479
9a04e7502e22 refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents: 44477
diff changeset
   287
      val assignment = global_state().the_assignment(previous).check_finished
46687
7e47ae85e161 tuned signature (in accordance with ML);
wenzelm
parents: 46682
diff changeset
   288
      global_state >> (_.define_version(version, assignment))
44481
bb42bc831570 tuned signature;
wenzelm
parents: 44479
diff changeset
   289
      prover.get.update(previous.id, version.id, doc_edits)
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   290
    }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   291
    //}}}
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   292
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   293
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   294
    /* prover output */
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   295
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   296
    def handle_output(output: Isabelle_Process.Output)
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   297
    //{{{
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   298
    {
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   299
      def bad_output(output: Isabelle_Process.Output)
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   300
      {
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   301
        if (verbose)
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   302
          System.err.println("Ignoring prover output: " + output.message.toString)
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   303
      }
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   304
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   305
      output.properties match {
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   306
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   307
        case Position.Id(state_id) if !output.is_protocol =>
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   308
          try {
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   309
            val st = global_state >>> (_.accumulate(state_id, output.message))
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 46944
diff changeset
   310
            delay_commands_changed.invoke(false, List(st.command))
38370
8b15d0f98962 explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents: 38366
diff changeset
   311
          }
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   312
          catch {
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   313
            case _: Document.State.Fail => bad_output(output)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   314
          }
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   315
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   316
        case Isabelle_Markup.Assign_Execs if output.is_protocol =>
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   317
          XML.content(output.body).mkString match {
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   318
            case Protocol.Assign(id, assign) =>
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   319
              try {
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   320
                val cmds = global_state >>> (_.assign(id, assign))
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   321
                delay_commands_changed.invoke(true, cmds)
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   322
              }
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   323
              catch { case _: Document.State.Fail => bad_output(output) }
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   324
            case _ => bad_output(output)
44661
383c9d758a56 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents: 44644
diff changeset
   325
          }
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   326
          // FIXME separate timeout event/message!?
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   327
          if (prover.isDefined && System.currentTimeMillis() > prune_next) {
46687
7e47ae85e161 tuned signature (in accordance with ML);
wenzelm
parents: 46682
diff changeset
   328
            val old_versions = global_state >>> (_.prune_history(prune_size))
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   329
            if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   330
            prune_next = System.currentTimeMillis() + prune_delay.ms
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   331
          }
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   332
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   333
        case Isabelle_Markup.Removed_Versions if output.is_protocol =>
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   334
          XML.content(output.body).mkString match {
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   335
            case Protocol.Removed(removed) =>
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   336
              try {
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   337
                global_state >> (_.removed_versions(removed))
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   338
              }
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   339
              catch { case _: Document.State.Fail => bad_output(output) }
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   340
            case _ => bad_output(output)
44676
7de87f1ae965 Document.removed_versions on Scala side;
wenzelm
parents: 44661
diff changeset
   341
          }
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   342
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   343
        case Isabelle_Markup.Invoke_Scala(name, id) if output.is_protocol =>
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   344
          Future.fork {
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   345
            val arg = XML.content(output.body).mkString
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   346
            val (tag, res) = Invoke_Scala.method(name, arg)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   347
            prover.get.invoke_scala(id, tag, res)
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   348
          }
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   349
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   350
        case Isabelle_Markup.Cancel_Scala(id) if output.is_protocol =>
46121
30a69cd8a9a0 prefer raw_message for protocol implementation;
wenzelm
parents: 46120
diff changeset
   351
          System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   352
48712
6b7a9bcc0bae simplified process startup phases: INIT suffices for is_ready;
wenzelm
parents: 48710
diff changeset
   353
        case _ if output.is_init =>
46121
30a69cd8a9a0 prefer raw_message for protocol implementation;
wenzelm
parents: 46120
diff changeset
   354
            phase = Session.Ready
46122
1e9ec1a44dfc prefer raw_message for protocol implementation;
wenzelm
parents: 46121
diff changeset
   355
48016
edbc8e8accd9 more explicit treatment of return code vs. session phase;
wenzelm
parents: 47653
diff changeset
   356
        case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
edbc8e8accd9 more explicit treatment of return code vs. session phase;
wenzelm
parents: 47653
diff changeset
   357
          if (rc == 0) phase = Session.Inactive
edbc8e8accd9 more explicit treatment of return code vs. session phase;
wenzelm
parents: 47653
diff changeset
   358
          else phase = Session.Failed
edbc8e8accd9 more explicit treatment of return code vs. session phase;
wenzelm
parents: 47653
diff changeset
   359
48712
6b7a9bcc0bae simplified process startup phases: INIT suffices for is_ready;
wenzelm
parents: 48710
diff changeset
   360
        case _ => bad_output(output)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
   361
      }
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   362
    }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   363
    //}}}
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   364
34820
a8ba6cde13e9 basic setup for synchronous / modal (!) prover startup;
wenzelm
parents: 34819
diff changeset
   365
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   366
    /* main loop */
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   367
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   368
    //{{{
38639
f642faca303e main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents: 38569
diff changeset
   369
    var finished = false
f642faca303e main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents: 38569
diff changeset
   370
    while (!finished) {
46570
wenzelm
parents: 46196
diff changeset
   371
      receiveWithin(delay_commands_changed.flush_timeout) {
wenzelm
parents: 46196
diff changeset
   372
        case TIMEOUT => delay_commands_changed.flush()
44722
a8331fb5c959 commands_change_delay within main actor -- prevents overloading of commands_change_buffer input channel;
wenzelm
parents: 44721
diff changeset
   373
48870
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents: 48794
diff changeset
   374
        case Start(args) if prover.isEmpty =>
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   375
          if (phase == Session.Inactive || phase == Session.Failed) {
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   376
            phase = Session.Startup
48020
a4f9957878ab clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents: 48016
diff changeset
   377
            prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   378
          }
38841
4df7b76249a0 include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents: 38722
diff changeset
   379
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   380
        case Stop =>
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   381
          if (phase == Session.Ready) {
46687
7e47ae85e161 tuned signature (in accordance with ML);
wenzelm
parents: 46682
diff changeset
   382
            global_state >> (_ => Document.State.init)  // FIXME event bus!?
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   383
            phase = Session.Shutdown
43649
a912f0b02359 eliminated null;
wenzelm
parents: 43648
diff changeset
   384
            prover.get.terminate
43717
c3ddb5537a2f more precise treatment of prover definedness;
wenzelm
parents: 43716
diff changeset
   385
            prover = None
39701
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   386
            phase = Session.Inactive
7c351c1c0624 simplified / clarified Session.Phase;
wenzelm
parents: 39698
diff changeset
   387
          }
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   388
          finished = true
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   389
          receiver.cancel()
39630
44181423183a explicit Session.Phase indication with associated event bus;
wenzelm
parents: 39629
diff changeset
   390
          reply(())
38850
5c3e5c548f12 session_actor: ignore spurious TIMEOUT (again) -- probably stemming from earlier use of receiveWithin;
wenzelm
parents: 38849
diff changeset
   391
44775
27930cf6f0f7 added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents: 44734
diff changeset
   392
        case Cancel_Execution if prover.isDefined =>
27930cf6f0f7 added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents: 44734
diff changeset
   393
          prover.get.cancel_execution()
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   394
49196
1d63ceb0d177 postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents: 48999
diff changeset
   395
        case raw @ Session.Raw_Edits(edits) if prover.isDefined =>
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   396
          prover.get.discontinue_execution()
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   397
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   398
          val previous = global_state().history.tip.version
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   399
          val version = Future.promise[Document.Version]
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   400
          val change = global_state >>> (_.continue_history(previous, edits, version))
49196
1d63ceb0d177 postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents: 48999
diff changeset
   401
          raw_edits.event(raw)
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   402
          change_parser ! Text_Edits(previous, edits, version)
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   403
43718
4a4ca9e4a14b clarified propagation of node name and header;
wenzelm
parents: 43717
diff changeset
   404
          reply(())
4a4ca9e4a14b clarified propagation of node name and header;
wenzelm
parents: 43717
diff changeset
   405
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   406
        case Messages(msgs) =>
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   407
          msgs foreach {
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   408
            case input: Isabelle_Process.Input =>
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   409
              all_messages.event(input)
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43720
diff changeset
   410
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   411
            case output: Isabelle_Process.Output =>
48999
3bdebf6ad9da clarified handling of raw output messages;
wenzelm
parents: 48884
diff changeset
   412
              if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
3bdebf6ad9da clarified handling of raw output messages;
wenzelm
parents: 48884
diff changeset
   413
              else handle_output(output)
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46771
diff changeset
   414
              if (output.is_syslog) syslog_messages.event(output)
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46772
diff changeset
   415
              all_messages.event(output)
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
   416
          }
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   417
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   418
        case change: Change
45635
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   419
        if prover.isDefined && global_state().is_assigned(change.previous) =>
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   420
          handle_change(change)
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   421
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   422
        case bad if !bad.isInstanceOf[Change] =>
45635
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   423
          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
   424
      }
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   425
    }
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   426
    //}}}
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   427
  }
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   428
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   429
43716
1d64662c1bfd tuned source structure;
wenzelm
parents: 43697
diff changeset
   430
  /* actions */
34809
0fed930f2992 misc tuning;
wenzelm
parents: 34808
diff changeset
   431
48870
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents: 48794
diff changeset
   432
  def start(args: List[String])
4accee106f0f clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents: 48794
diff changeset
   433
  { session_actor ! Start(args) }
45076
dd803d319d5b tuned signature;
wenzelm
parents: 45075
diff changeset
   434
45635
d9cf3520083c explicit change_parser thread, which avoids undirected Future.fork with its tendency towards hundreds of worker threads;
wenzelm
parents: 45633
diff changeset
   435
  def stop() { commands_changed_buffer !? Stop; change_parser !? 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
   436
44775
27930cf6f0f7 added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents: 44734
diff changeset
   437
  def cancel_execution() { session_actor ! Cancel_Execution }
43648
e32de528b5ef more explicit edit_node vs. init_node;
wenzelm
parents: 43647
diff changeset
   438
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   439
  def edit(edits: List[Document.Edit_Text])
49196
1d63ceb0d177 postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents: 48999
diff changeset
   440
  { session_actor !? Session.Raw_Edits(edits) }
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   441
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   442
  def init_node(name: Document.Node.Name,
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48422
diff changeset
   443
    header: Document.Node.Header, perspective: Text.Perspective, text: String)
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   444
  {
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   445
    edit(List(header_edit(name, header),
48755
393a37003851 apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
wenzelm
parents: 48713
diff changeset
   446
      name -> Document.Node.Clear(),
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   447
      name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   448
      name -> Document.Node.Perspective(perspective)))
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   449
  }
38221
e0f00f0945b4 misc tuning and clarification;
wenzelm
parents: 38150
diff changeset
   450
44615
a4ff8a787202 more abstract Document.Node.Name;
wenzelm
parents: 44612
diff changeset
   451
  def edit_node(name: Document.Node.Name,
48707
ba531af91148 simplified Document.Node.Header -- internalized errors;
wenzelm
parents: 48422
diff changeset
   452
    header: Document.Node.Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
47629
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   453
  {
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   454
    edit(List(header_edit(name, header),
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   455
      name -> Document.Node.Edits(text_edits),
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   456
      name -> Document.Node.Perspective(perspective)))
645163d3b964 simplified internal actor protocol;
wenzelm
parents: 47390
diff changeset
   457
  }
34777
91d6089cef88 class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff changeset
   458
}