author | wenzelm |
Wed, 22 Sep 2010 14:53:42 +0200 | |
changeset 39588 | 507fcf86e1e0 |
parent 39585 | 00be8711082f |
child 39589 | 5b81b8df1dde |
permissions | -rw-r--r-- |
36676 | 1 |
/* Title: Pure/System/session.scala |
2 |
Author: Makarius |
|
38221 | 3 |
Options: :folding=explicit:collapseFolds=1: |
36676 | 4 |
|
5 |
Isabelle session, potentially with running prover. |
|
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 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
10 |
|
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
11 |
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
|
12 |
import scala.actors.Actor |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
13 |
import scala.actors.Actor._ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
14 |
|
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
15 |
|
34791 | 16 |
object Session |
17 |
{ |
|
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
18 |
/* events */ |
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
19 |
|
34791 | 20 |
case object Global_Settings |
37849 | 21 |
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
|
22 |
case object Assignment |
38360 | 23 |
case class Commands_Changed(set: Set[Command]) |
34791 | 24 |
} |
25 |
||
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
26 |
|
34851
304a86164dd2
provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;
wenzelm
parents:
34848
diff
changeset
|
27 |
class Session(system: Isabelle_System) |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
28 |
{ |
37849 | 29 |
/* real time parameters */ // FIXME properties or settings (!?) |
30 |
||
31 |
// user input (e.g. text edits, cursor movement) |
|
32 |
val input_delay = 300 |
|
33 |
||
34 |
// prover output (markup, common messages) |
|
35 |
val output_delay = 100 |
|
36 |
||
37 |
// GUI layout updates |
|
38 |
val update_delay = 500 |
|
39 |
||
40 |
||
34809 | 41 |
/* pervasive event buses */ |
42 |
||
43 |
val global_settings = new Event_Bus[Session.Global_Settings.type] |
|
39588 | 44 |
val raw_messages = new Event_Bus[Isabelle_Process.Result] |
38360 | 45 |
val commands_changed = new Event_Bus[Session.Commands_Changed] |
37849 | 46 |
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
|
47 |
val assignments = new Event_Bus[Session.Assignment.type] |
34809 | 48 |
|
49 |
||
34778 | 50 |
/* unique ids */ |
51 |
||
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38360
diff
changeset
|
52 |
private var id_count: Document.ID = 0 |
38419 | 53 |
def new_id(): Document.ID = synchronized { |
38355
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38260
diff
changeset
|
54 |
require(id_count > java.lang.Long.MIN_VALUE) |
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38260
diff
changeset
|
55 |
id_count -= 1 |
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38260
diff
changeset
|
56 |
id_count |
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38260
diff
changeset
|
57 |
} |
34778 | 58 |
|
59 |
||
34826 | 60 |
|
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
61 |
/** 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
|
62 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
63 |
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
|
64 |
|
39572 | 65 |
private val (_, command_change_buffer) = |
66 |
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
|
67 |
//{{{ |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
68 |
{ |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
69 |
import scala.compat.Platform.currentTime |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
70 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
71 |
var changed: Set[Command] = Set() |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
72 |
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
|
73 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
74 |
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
|
75 |
flush_time match { |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
76 |
case None => 5000L |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
77 |
case Some(time) => (time - currentTime) max 0 |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
78 |
} |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
79 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
80 |
def flush() |
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 |
if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed)) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
83 |
changed = Set() |
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 |
{ |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
89 |
val now = currentTime |
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 { |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
91 |
case None => flush_time = Some(now + output_delay) |
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) { |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
99 |
case command: Command => changed += command; invoke() |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
100 |
case TIMEOUT => flush() |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
101 |
case Stop => finished = true |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
102 |
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
|
103 |
} |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
104 |
} |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
105 |
} |
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 |
/** main protocol actor **/ |
34809 | 111 |
|
34851
304a86164dd2
provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;
wenzelm
parents:
34848
diff
changeset
|
112 |
@volatile private var syntax = new Outer_Syntax(system.symbols) |
38569 | 113 |
def current_syntax(): Outer_Syntax = syntax |
34809 | 114 |
|
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
115 |
private val global_state = new Volatile(Document.State.init) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
116 |
def current_state(): Document.State = global_state.peek() |
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
117 |
|
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
118 |
private case class Edit_Version(edits: List[Document.Node_Text_Edit]) |
38221 | 119 |
private case class Started(timeout: Int, args: List[String]) |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
120 |
|
39572 | 121 |
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
|
122 |
{ |
34809 | 123 |
var prover: Isabelle_Process with Isar_Document = null |
124 |
||
125 |
||
126 |
/* document changes */ |
|
127 |
||
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38226
diff
changeset
|
128 |
def handle_change(change: Document.Change) |
38221 | 129 |
//{{{ |
34809 | 130 |
{ |
38848
9483bb678d96
use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled;
wenzelm
parents:
38842
diff
changeset
|
131 |
val previous = change.previous.get_finished |
9483bb678d96
use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled;
wenzelm
parents:
38842
diff
changeset
|
132 |
val (node_edits, current) = change.result.get_finished |
38366
fea82d1add74
simplified/clarified Change: transition prev --edits--> result, based on futures;
wenzelm
parents:
38365
diff
changeset
|
133 |
|
38848
9483bb678d96
use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled;
wenzelm
parents:
38842
diff
changeset
|
134 |
var former_assignment = global_state.peek().the_assignment(previous).get_finished |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38366
diff
changeset
|
135 |
for { |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38366
diff
changeset
|
136 |
(name, Some(cmd_edits)) <- node_edits |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38366
diff
changeset
|
137 |
(prev, None) <- cmd_edits |
38417 | 138 |
removed <- previous.nodes(name).commands.get_after(prev) |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38366
diff
changeset
|
139 |
} former_assignment -= removed |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38366
diff
changeset
|
140 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
141 |
val id_edits = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
142 |
node_edits map { |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
143 |
case (name, None) => (name, None) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
144 |
case (name, Some(cmd_edits)) => |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38366
diff
changeset
|
145 |
val ids = |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
146 |
cmd_edits map { |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
147 |
case (c1, c2) => |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
148 |
val id1 = c1.map(_.id) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
149 |
val id2 = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
150 |
c2 match { |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
151 |
case None => None |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
152 |
case Some(command) => |
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
153 |
if (global_state.peek().lookup_command(command.id).isEmpty) { |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
154 |
global_state.change(_.define_command(command)) |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
155 |
prover.define_command(command.id, system.symbols.encode(command.source)) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
156 |
} |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
157 |
Some(command.id) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
158 |
} |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
159 |
(id1, id2) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
160 |
} |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38366
diff
changeset
|
161 |
(name -> Some(ids)) |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
162 |
} |
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
163 |
global_state.change(_.define_version(current, former_assignment)) |
38417 | 164 |
prover.edit_version(previous.id, current.id, id_edits) |
34809 | 165 |
} |
38221 | 166 |
//}}} |
34809 | 167 |
|
168 |
||
169 |
/* prover results */ |
|
170 |
||
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
171 |
def bad_result(result: Isabelle_Process.Result) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
172 |
{ |
37041 | 173 |
System.err.println("Ignoring prover result: " + result.message.toString) |
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
174 |
} |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
175 |
|
34809 | 176 |
def handle_result(result: Isabelle_Process.Result) |
38221 | 177 |
//{{{ |
34809 | 178 |
{ |
39588 | 179 |
raw_messages.event(result) |
34799
0330a4284a9b
just one variable for outer syntax keywords and completion;
wenzelm
parents:
34795
diff
changeset
|
180 |
|
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38639
diff
changeset
|
181 |
result.properties match { |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38639
diff
changeset
|
182 |
case Position.Id(state_id) => |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38366
diff
changeset
|
183 |
try { |
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
184 |
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
|
185 |
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
|
186 |
} |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38413
diff
changeset
|
187 |
catch { case _: Document.State.Fail => bad_result(result) } |
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38639
diff
changeset
|
188 |
case _ => |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38366
diff
changeset
|
189 |
if (result.is_status) { |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38366
diff
changeset
|
190 |
result.body match { |
38417 | 191 |
case List(Isar_Document.Assign(id, edits)) => |
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
|
192 |
try { |
38882
e1fb3bbc22ab
Document state assignment indicates command change;
wenzelm
parents:
38850
diff
changeset
|
193 |
val cmds: List[Command] = global_state.change_yield(_.assign(id, edits)) |
e1fb3bbc22ab
Document state assignment indicates command change;
wenzelm
parents:
38850
diff
changeset
|
194 |
for (cmd <- cmds) command_change_buffer ! cmd |
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
|
195 |
assignments.event(Session.Assignment) |
2f198d107aef
session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;
wenzelm
parents:
38848
diff
changeset
|
196 |
} |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38413
diff
changeset
|
197 |
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
|
198 |
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
|
199 |
case List(Keyword.Keyword_Decl(name)) => syntax += name |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38366
diff
changeset
|
200 |
case _ => if (!result.is_ready) bad_result(result) |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38366
diff
changeset
|
201 |
} |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38366
diff
changeset
|
202 |
} |
39525 | 203 |
else if (result.is_exit) prover = null // FIXME ?? |
39588 | 204 |
else if (!result.is_system && !result.is_stdout) bad_result(result) |
34809 | 205 |
} |
206 |
} |
|
38221 | 207 |
//}}} |
34809 | 208 |
|
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
209 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
210 |
/* prover startup */ |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
211 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
212 |
def startup_error(): String = |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
213 |
{ |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
214 |
val buf = new StringBuilder |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
215 |
while ( |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
216 |
receiveWithin(0) { |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
217 |
case result: Isabelle_Process.Result => |
39572 | 218 |
if (result.is_system) { |
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
219 |
for (text <- XML.content(result.message)) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
220 |
buf.append(text) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
221 |
} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
222 |
true |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
223 |
case TIMEOUT => false |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
224 |
}) {} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
225 |
buf.toString |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
226 |
} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
227 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
228 |
def prover_startup(timeout: Int): Option[String] = |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
229 |
{ |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
230 |
receiveWithin(timeout) { |
39525 | 231 |
case result: Isabelle_Process.Result if result.is_init => |
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
232 |
while (receive { |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
233 |
case result: Isabelle_Process.Result => |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
234 |
handle_result(result); !result.is_ready |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
235 |
}) {} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
236 |
None |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
237 |
|
39525 | 238 |
case result: Isabelle_Process.Result if result.is_exit => |
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
239 |
Some(startup_error()) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
240 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
241 |
case TIMEOUT => // FIXME clarify |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39572
diff
changeset
|
242 |
prover.terminate; Some(startup_error()) |
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
243 |
} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
244 |
} |
34809 | 245 |
|
246 |
||
39524 | 247 |
/* main loop */ // FIXME proper shutdown |
34809 | 248 |
|
38639
f642faca303e
main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents:
38569
diff
changeset
|
249 |
var finished = false |
f642faca303e
main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents:
38569
diff
changeset
|
250 |
while (!finished) { |
f642faca303e
main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents:
38569
diff
changeset
|
251 |
receive { |
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
252 |
case Edit_Version(edits) => |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
253 |
val previous = global_state.peek().history.tip.current |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
254 |
val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) } |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
255 |
val change = global_state.change_yield(_.extend_history(previous, edits, result)) |
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
|
256 |
|
2f198d107aef
session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;
wenzelm
parents:
38848
diff
changeset
|
257 |
val this_actor = self |
2f198d107aef
session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;
wenzelm
parents:
38848
diff
changeset
|
258 |
change.current.map(_ => { |
2f198d107aef
session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;
wenzelm
parents:
38848
diff
changeset
|
259 |
assignments.await { global_state.peek().is_assigned(previous.get_finished) } |
2f198d107aef
session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;
wenzelm
parents:
38848
diff
changeset
|
260 |
this_actor ! change }) |
2f198d107aef
session_actor: await state assigment of previous change before signalling current change, and avoid crash in overrun situations;
wenzelm
parents:
38848
diff
changeset
|
261 |
|
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
262 |
reply(()) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
263 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
264 |
case change: Document.Change if prover != null => |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
265 |
handle_change(change) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
266 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
267 |
case result: Isabelle_Process.Result => |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
268 |
handle_result(result) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
269 |
|
38221 | 270 |
case Started(timeout, args) => |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
271 |
if (prover == null) { |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39525
diff
changeset
|
272 |
prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document |
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
273 |
val origin = sender |
39572 | 274 |
val opt_err = prover_startup(timeout + 500) |
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
275 |
if (opt_err.isDefined) prover = null |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
276 |
origin ! opt_err |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
277 |
} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
278 |
else reply(None) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
279 |
|
38639
f642faca303e
main session actor as independent thread, to avoid starvation via regular worker pool;
wenzelm
parents:
38569
diff
changeset
|
280 |
case Stop => // FIXME synchronous!? |
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
281 |
if (prover != null) { |
39524 | 282 |
global_state.change(_ => Document.State.init) |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39572
diff
changeset
|
283 |
prover.terminate |
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
284 |
prover = null |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
285 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
286 |
|
38850
5c3e5c548f12
session_actor: ignore spurious TIMEOUT (again) -- probably stemming from earlier use of receiveWithin;
wenzelm
parents:
38849
diff
changeset
|
287 |
case TIMEOUT => // FIXME clarify |
5c3e5c548f12
session_actor: ignore spurious TIMEOUT (again) -- probably stemming from earlier use of receiveWithin;
wenzelm
parents:
38849
diff
changeset
|
288 |
|
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
289 |
case bad if prover != null => |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
290 |
System.err.println("session_actor: ignoring bad message " + bad) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
291 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
292 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
293 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
294 |
|
34809 | 295 |
|
37129 | 296 |
|
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
|
297 |
/** main methods **/ |
34809 | 298 |
|
38221 | 299 |
def started(timeout: Int, args: List[String]): Option[String] = |
300 |
(session_actor !? Started(timeout, args)).asInstanceOf[Option[String]] |
|
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
301 |
|
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
302 |
def stop() { command_change_buffer ! Stop; session_actor ! Stop } |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
303 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
304 |
def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) } |
38221 | 305 |
|
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
306 |
def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot = |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38722
diff
changeset
|
307 |
global_state.peek().snapshot(name, pending_edits) |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
308 |
} |