author | wenzelm |
Thu, 12 Aug 2010 16:01:44 +0200 | |
changeset 38364 | 827b90f18ff4 |
parent 38363 | af7f41a8a0a8 |
child 38365 | 7c6254a9c432 |
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 |
38360 | 22 |
case class Commands_Changed(set: Set[Command]) |
23 |
||
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
24 |
|
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
25 |
|
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
26 |
/* managed entities */ |
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
27 |
|
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
28 |
trait Entity |
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
29 |
{ |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38360
diff
changeset
|
30 |
val id: Document.ID |
37129 | 31 |
def consume(message: XML.Tree, forward: Command => Unit): Unit |
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
32 |
} |
34791 | 33 |
} |
34 |
||
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
35 |
|
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
|
36 |
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
|
37 |
{ |
37849 | 38 |
/* real time parameters */ // FIXME properties or settings (!?) |
39 |
||
40 |
// user input (e.g. text edits, cursor movement) |
|
41 |
val input_delay = 300 |
|
42 |
||
43 |
// prover output (markup, common messages) |
|
44 |
val output_delay = 100 |
|
45 |
||
46 |
// GUI layout updates |
|
47 |
val update_delay = 500 |
|
48 |
||
49 |
||
34809 | 50 |
/* pervasive event buses */ |
51 |
||
52 |
val global_settings = new Event_Bus[Session.Global_Settings.type] |
|
53 |
val raw_results = new Event_Bus[Isabelle_Process.Result] |
|
37065
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
37063
diff
changeset
|
54 |
val raw_output = new Event_Bus[Isabelle_Process.Result] |
38360 | 55 |
val commands_changed = new Event_Bus[Session.Commands_Changed] |
37849 | 56 |
val perspective = new Event_Bus[Session.Perspective.type] |
34809 | 57 |
|
58 |
||
34778 | 59 |
/* unique ids */ |
60 |
||
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38360
diff
changeset
|
61 |
private var id_count: Document.ID = 0 |
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38360
diff
changeset
|
62 |
def create_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
|
63 |
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
|
64 |
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
|
65 |
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
|
66 |
} |
34778 | 67 |
|
68 |
||
34826 | 69 |
|
70 |
/** main actor **/ |
|
34809 | 71 |
|
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
|
72 |
@volatile private var syntax = new Outer_Syntax(system.symbols) |
34819 | 73 |
def current_syntax: Outer_Syntax = syntax |
34809 | 74 |
|
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38360
diff
changeset
|
75 |
@volatile private var entities = Map[Document.ID, Session.Entity]() |
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38360
diff
changeset
|
76 |
def lookup_entity(id: Document.ID): Option[Session.Entity] = entities.get(id) |
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38360
diff
changeset
|
77 |
def lookup_command(id: Document.ID): Option[Command] = |
34835
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34833
diff
changeset
|
78 |
lookup_entity(id) match { |
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34833
diff
changeset
|
79 |
case Some(cmd: Command) => Some(cmd) |
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34833
diff
changeset
|
80 |
case _ => None |
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34833
diff
changeset
|
81 |
} |
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
82 |
|
38221 | 83 |
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
|
84 |
private case object Stop |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
85 |
|
37129 | 86 |
private lazy val session_actor = actor { |
34809 | 87 |
|
88 |
var prover: Isabelle_Process with Isar_Document = null |
|
89 |
||
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
90 |
def register(entity: Session.Entity) { entities += (entity.id -> entity) } |
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
91 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
92 |
var documents = Map[Document.Version_ID, Document]() |
34835
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34833
diff
changeset
|
93 |
def register_document(doc: Document) { documents += (doc.id -> doc) } |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
94 |
register_document(Document.init) |
34835
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34833
diff
changeset
|
95 |
|
34809 | 96 |
|
97 |
/* document changes */ |
|
98 |
||
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38226
diff
changeset
|
99 |
def handle_change(change: Document.Change) |
38221 | 100 |
//{{{ |
34809 | 101 |
{ |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
102 |
require(change.parent.isDefined) |
34809 | 103 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
104 |
val (node_edits, doc) = change.result.join |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
105 |
val id_edits = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
106 |
node_edits map { |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
107 |
case (name, None) => (name, None) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
108 |
case (name, Some(cmd_edits)) => |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
109 |
val chs = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
110 |
cmd_edits map { |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
111 |
case (c1, c2) => |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
112 |
val id1 = c1.map(_.id) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
113 |
val id2 = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
114 |
c2 match { |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
115 |
case None => None |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
116 |
case Some(command) => |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
117 |
if (!lookup_command(command.id).isDefined) { |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
118 |
register(command) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
119 |
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
|
120 |
} |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
121 |
Some(command.id) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
122 |
} |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
123 |
(id1, id2) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
124 |
} |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
125 |
(name -> Some(chs)) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
126 |
} |
34835
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34833
diff
changeset
|
127 |
register_document(doc) |
38364
827b90f18ff4
Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway;
wenzelm
parents:
38363
diff
changeset
|
128 |
prover.edit_document(change.parent.get.join_document.id, doc.id, id_edits) |
34809 | 129 |
} |
38221 | 130 |
//}}} |
34809 | 131 |
|
132 |
||
133 |
/* prover results */ |
|
134 |
||
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
135 |
def bad_result(result: Isabelle_Process.Result) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
136 |
{ |
37041 | 137 |
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
|
138 |
} |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
139 |
|
34809 | 140 |
def handle_result(result: Isabelle_Process.Result) |
38221 | 141 |
//{{{ |
34809 | 142 |
{ |
143 |
raw_results.event(result) |
|
34799
0330a4284a9b
just one variable for outer syntax keywords and completion;
wenzelm
parents:
34795
diff
changeset
|
144 |
|
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38360
diff
changeset
|
145 |
val target_id: Option[Document.ID] = Position.get_id(result.properties) |
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
146 |
val target: Option[Session.Entity] = |
34835
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34833
diff
changeset
|
147 |
target_id match { |
34809 | 148 |
case None => None |
34835
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34833
diff
changeset
|
149 |
case Some(id) => lookup_entity(id) |
34809 | 150 |
} |
37129 | 151 |
if (target.isDefined) target.get.consume(result.message, indicate_command_change) |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
152 |
else if (result.is_status) { |
34818
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34817
diff
changeset
|
153 |
// global status message |
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
154 |
result.body match { |
34835
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34833
diff
changeset
|
155 |
|
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38360
diff
changeset
|
156 |
// execution assignment |
36682 | 157 |
case List(Isar_Document.Assign(edits)) if target_id.isDefined => |
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
158 |
documents.get(target_id.get) match { |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
159 |
case Some(doc) => |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38360
diff
changeset
|
160 |
val execs = |
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
161 |
for { |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38360
diff
changeset
|
162 |
Isar_Document.Edit(cmd_id, exec_id) <- edits |
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
163 |
cmd <- lookup_command(cmd_id) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
164 |
} yield { |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38360
diff
changeset
|
165 |
val st = cmd.assign_exec(exec_id) // FIXME session state |
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
166 |
register(st) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
167 |
(cmd, st) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
168 |
} |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38360
diff
changeset
|
169 |
doc.assign_execs(execs) // FIXME session state |
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
170 |
case None => bad_result(result) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
171 |
} |
34809 | 172 |
|
36682 | 173 |
// keyword declarations |
36947 | 174 |
case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind) |
175 |
case List(Keyword.Keyword_Decl(name)) => syntax += name |
|
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
176 |
|
34839 | 177 |
case _ => if (!result.is_ready) bad_result(result) |
34809 | 178 |
} |
179 |
} |
|
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
180 |
else if (result.kind == Markup.EXIT) |
34809 | 181 |
prover = null |
37065
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
37063
diff
changeset
|
182 |
else if (result.is_raw) |
2a73253b5898
separate event bus and dockable for raw output (stdout);
wenzelm
parents:
37063
diff
changeset
|
183 |
raw_output.event(result) |
37063 | 184 |
else if (!result.is_system) // FIXME syslog (!?) |
34837 | 185 |
bad_result(result) |
34809 | 186 |
} |
38221 | 187 |
//}}} |
34809 | 188 |
|
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
189 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
190 |
/* prover startup */ |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
191 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
192 |
def startup_error(): String = |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
193 |
{ |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
194 |
val buf = new StringBuilder |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
195 |
while ( |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
196 |
receiveWithin(0) { |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
197 |
case result: Isabelle_Process.Result => |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
198 |
if (result.is_raw) { |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
199 |
for (text <- XML.content(result.message)) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
200 |
buf.append(text) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
201 |
} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
202 |
true |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
203 |
case TIMEOUT => false |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
204 |
}) {} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
205 |
buf.toString |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
206 |
} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
207 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
208 |
def prover_startup(timeout: Int): Option[String] = |
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 |
receiveWithin(timeout) { |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
211 |
case result: Isabelle_Process.Result |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
212 |
if result.kind == Markup.INIT => |
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
213 |
while (receive { |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
214 |
case result: Isabelle_Process.Result => |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
215 |
handle_result(result); !result.is_ready |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
216 |
}) {} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
217 |
None |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
218 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
219 |
case result: Isabelle_Process.Result |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
220 |
if result.kind == Markup.EXIT => |
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
221 |
Some(startup_error()) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
222 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
223 |
case TIMEOUT => // FIXME clarify |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
224 |
prover.kill; Some(startup_error()) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
225 |
} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
226 |
} |
34809 | 227 |
|
228 |
||
229 |
/* main loop */ |
|
230 |
||
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
231 |
val xml_cache = new XML.Cache(131071) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
232 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
233 |
loop { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
234 |
react { |
38221 | 235 |
case Started(timeout, args) => |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
236 |
if (prover == null) { |
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
|
237 |
prover = new Isabelle_Process(system, self, args:_*) with Isar_Document |
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
238 |
val origin = sender |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
239 |
val opt_err = prover_startup(timeout) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
240 |
if (opt_err.isDefined) prover = null |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
241 |
origin ! opt_err |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
242 |
} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
243 |
else reply(None) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
244 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
245 |
case Stop => // FIXME clarify; synchronous |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
246 |
if (prover != null) { |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
247 |
prover.kill |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
248 |
prover = null |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
249 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
250 |
|
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38226
diff
changeset
|
251 |
case change: Document.Change if prover != null => |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
252 |
handle_change(change) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
253 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
254 |
case result: Isabelle_Process.Result => |
34795 | 255 |
handle_result(result.cache(xml_cache)) |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
256 |
|
36782
0499d05663dd
ignore spurious TIMEOUT messages, maybe caused by change of actor semantics in scala-2.8;
wenzelm
parents:
36682
diff
changeset
|
257 |
case TIMEOUT => // FIXME clarify! |
0499d05663dd
ignore spurious TIMEOUT messages, maybe caused by change of actor semantics in scala-2.8;
wenzelm
parents:
36682
diff
changeset
|
258 |
|
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
259 |
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
|
260 |
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
|
261 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
262 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
263 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
264 |
|
34809 | 265 |
|
37129 | 266 |
|
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
|
267 |
/** buffered command changes (delay_first discipline) **/ |
37129 | 268 |
|
38221 | 269 |
private lazy val command_change_buffer = actor |
270 |
//{{{ |
|
271 |
{ |
|
37129 | 272 |
import scala.compat.Platform.currentTime |
273 |
||
274 |
var changed: Set[Command] = Set() |
|
275 |
var flush_time: Option[Long] = None |
|
276 |
||
277 |
def flush_timeout: Long = |
|
278 |
flush_time match { |
|
279 |
case None => 5000L |
|
280 |
case Some(time) => (time - currentTime) max 0 |
|
281 |
} |
|
282 |
||
283 |
def flush() |
|
284 |
{ |
|
38360 | 285 |
if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed)) |
37129 | 286 |
changed = Set() |
287 |
flush_time = None |
|
288 |
} |
|
289 |
||
290 |
def invoke() |
|
291 |
{ |
|
292 |
val now = currentTime |
|
293 |
flush_time match { |
|
37849 | 294 |
case None => flush_time = Some(now + output_delay) |
37129 | 295 |
case Some(time) => if (now >= time) flush() |
296 |
} |
|
297 |
} |
|
298 |
||
299 |
loop { |
|
300 |
reactWithin(flush_timeout) { |
|
301 |
case command: Command => changed += command; invoke() |
|
302 |
case TIMEOUT => flush() |
|
303 |
case bad => System.err.println("command_change_buffer: ignoring bad message " + bad) |
|
304 |
} |
|
305 |
} |
|
306 |
} |
|
38221 | 307 |
//}}} |
37129 | 308 |
|
309 |
def indicate_command_change(command: Command) |
|
310 |
{ |
|
311 |
command_change_buffer ! command |
|
312 |
} |
|
313 |
||
314 |
||
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
|
315 |
|
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
|
316 |
/** editor history **/ |
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
|
317 |
|
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
|
318 |
private case class Edit_Document(edits: List[Document.Node_Text_Edit]) |
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
|
319 |
|
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
|
320 |
private val editor_history = new Actor |
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
|
321 |
{ |
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38226
diff
changeset
|
322 |
@volatile private var history = Document.Change.init |
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38226
diff
changeset
|
323 |
def current_change(): Document.Change = history |
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
|
324 |
|
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
|
325 |
def act |
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
|
326 |
{ |
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
|
327 |
loop { |
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
|
328 |
react { |
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
|
329 |
case Edit_Document(edits) => |
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
|
330 |
val old_change = history |
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
|
331 |
val result: isabelle.Future[(List[Document.Edit[Command]], Document)] = |
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
|
332 |
isabelle.Future.fork { |
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
|
333 |
val old_doc = old_change.join_document |
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
|
334 |
old_doc.await_assignment |
38364
827b90f18ff4
Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway;
wenzelm
parents:
38363
diff
changeset
|
335 |
Document.text_edits(Session.this, old_doc, edits) |
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
|
336 |
} |
38364
827b90f18ff4
Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway;
wenzelm
parents:
38363
diff
changeset
|
337 |
val new_change = new Document.Change(Some(old_change), edits, result) |
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
|
338 |
history = new_change |
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
|
339 |
new_change.result.map(_ => session_actor ! new_change) |
38260
d4a1c7a19be3
edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;
wenzelm
parents:
38230
diff
changeset
|
340 |
reply(()) |
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
|
341 |
|
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
|
342 |
case bad => System.err.println("editor_model: ignoring bad message " + bad) |
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
|
343 |
} |
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
|
344 |
} |
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
|
345 |
} |
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
|
346 |
} |
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
|
347 |
editor_history.start |
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
|
348 |
|
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
|
349 |
|
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
|
350 |
|
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
|
351 |
/** main methods **/ |
34809 | 352 |
|
38221 | 353 |
def started(timeout: Int, args: List[String]): Option[String] = |
354 |
(session_actor !? Started(timeout, args)).asInstanceOf[Option[String]] |
|
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
355 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
356 |
def stop() { session_actor ! Stop } |
38221 | 357 |
|
38359
96b22dfeb56a
consider snapshot as service of Session, not Document.Change;
wenzelm
parents:
38355
diff
changeset
|
358 |
def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot = |
96b22dfeb56a
consider snapshot as service of Session, not Document.Change;
wenzelm
parents:
38355
diff
changeset
|
359 |
editor_history.current_change().snapshot(name, pending_edits) |
38260
d4a1c7a19be3
edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;
wenzelm
parents:
38230
diff
changeset
|
360 |
|
d4a1c7a19be3
edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;
wenzelm
parents:
38230
diff
changeset
|
361 |
def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) } |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
362 |
} |