author | wenzelm |
Mon, 03 May 2010 20:13:36 +0200 | |
changeset 36615 | 88756a5a92fc |
parent 35013 | f3d491658893 |
child 36676 | ac7961d42ac3 |
permissions | -rw-r--r-- |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
1 |
/* |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
2 |
* Isabelle session, potentially with running prover |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
3 |
* |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
4 |
* @author Makarius |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
5 |
*/ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
6 |
|
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
|
7 |
package isabelle |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
8 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
9 |
|
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
10 |
import scala.actors.TIMEOUT |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
11 |
import scala.actors.Actor._ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
12 |
|
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
13 |
|
34791 | 14 |
object Session |
15 |
{ |
|
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
16 |
/* events */ |
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
17 |
|
34791 | 18 |
case object Global_Settings |
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
19 |
|
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
20 |
|
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
21 |
/* managed entities */ |
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
22 |
|
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
23 |
type Entity_ID = String |
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 |
trait Entity |
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
26 |
{ |
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
27 |
val id: Entity_ID |
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
28 |
def consume(session: Session, message: XML.Tree): Unit |
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
29 |
} |
34791 | 30 |
} |
31 |
||
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
32 |
|
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
|
33 |
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
|
34 |
{ |
34809 | 35 |
/* pervasive event buses */ |
36 |
||
37 |
val global_settings = new Event_Bus[Session.Global_Settings.type] |
|
38 |
val raw_results = new Event_Bus[Isabelle_Process.Result] |
|
39 |
val results = new Event_Bus[Command] |
|
40 |
||
41 |
val command_change = new Event_Bus[Command] |
|
42 |
||
43 |
||
34778 | 44 |
/* unique ids */ |
45 |
||
46 |
private var id_count: BigInt = 0 |
|
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
47 |
def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count } |
34778 | 48 |
|
49 |
||
34826 | 50 |
|
51 |
/** main actor **/ |
|
34809 | 52 |
|
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
|
53 |
@volatile private var syntax = new Outer_Syntax(system.symbols) |
34819 | 54 |
def current_syntax: Outer_Syntax = syntax |
34809 | 55 |
|
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
56 |
@volatile private var entities = Map[Session.Entity_ID, Session.Entity]() |
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
57 |
def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id) |
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
|
58 |
def lookup_command(id: Session.Entity_ID): Option[Command] = |
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
|
59 |
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
|
60 |
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
|
61 |
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
|
62 |
} |
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
63 |
|
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
64 |
private case class Start(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
|
65 |
private case object Stop |
34808
e462572536e9
eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset
|
66 |
private case class Begin_Document(path: String) |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
67 |
|
34809 | 68 |
private val session_actor = actor { |
69 |
||
70 |
var prover: Isabelle_Process with Isar_Document = null |
|
71 |
||
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
72 |
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
|
73 |
|
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
|
74 |
var documents = Map[Isar_Document.Document_ID, Document]() |
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
|
75 |
def register_document(doc: Document) { documents += (doc.id -> doc) } |
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
|
76 |
|
34809 | 77 |
|
78 |
/* document changes */ |
|
79 |
||
80 |
def handle_change(change: Change) |
|
81 |
{ |
|
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
82 |
require(change.parent.isDefined) |
34809 | 83 |
|
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34851
diff
changeset
|
84 |
val (changes, doc) = change.result.join |
34809 | 85 |
val id_changes = changes map { |
86 |
case (c1, c2) => |
|
87 |
(c1.map(_.id).getOrElse(""), |
|
88 |
c2 match { |
|
89 |
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
|
90 |
case Some(command) => |
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
|
91 |
if (!lookup_command(command.id).isDefined) { |
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
|
92 |
register(command) |
34859 | 93 |
prover.define_command(command.id, system.symbols.encode(command.source)) |
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
|
94 |
} |
34809 | 95 |
Some(command.id) |
96 |
}) |
|
97 |
} |
|
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
|
98 |
register_document(doc) |
34833
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34831
diff
changeset
|
99 |
prover.edit_document(change.parent.get.id, doc.id, id_changes) |
34809 | 100 |
} |
101 |
||
102 |
||
103 |
/* prover results */ |
|
104 |
||
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
105 |
def bad_result(result: Isabelle_Process.Result) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
106 |
{ |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
107 |
System.err.println("Ignoring prover result: " + result) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
108 |
} |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
109 |
|
34809 | 110 |
def handle_result(result: Isabelle_Process.Result) |
111 |
{ |
|
112 |
raw_results.event(result) |
|
34799
0330a4284a9b
just one variable for outer syntax keywords and completion;
wenzelm
parents:
34795
diff
changeset
|
113 |
|
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
|
114 |
val target_id: Option[Session.Entity_ID] = Position.get_id(result.props) |
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
115 |
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
|
116 |
target_id match { |
34809 | 117 |
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
|
118 |
case Some(id) => lookup_entity(id) |
34809 | 119 |
} |
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
120 |
if (target.isDefined) target.get.consume(this, result.message) |
34809 | 121 |
else if (result.kind == Isabelle_Process.Kind.STATUS) { |
34818
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34817
diff
changeset
|
122 |
// global status message |
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
123 |
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
|
124 |
|
35013 | 125 |
// document state assignment |
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
126 |
case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined => |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
127 |
documents.get(target_id.get) match { |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
128 |
case Some(doc) => |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
129 |
val states = |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
130 |
for { |
35013 | 131 |
XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) <- edits |
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
132 |
cmd <- lookup_command(cmd_id) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
133 |
} yield { |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
134 |
val st = cmd.assign_state(state_id) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
135 |
register(st) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
136 |
(cmd, st) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
137 |
} |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
138 |
doc.assign_states(states) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
139 |
case None => bad_result(result) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
140 |
} |
34809 | 141 |
|
34836
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
142 |
// command and keyword declarations |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
143 |
case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) => |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
144 |
syntax += (name, kind) |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
145 |
case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) => |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
146 |
syntax += name |
b83c7a738eb8
singleton status messages, with more precise patterns -- report bad messages;
wenzelm
parents:
34835
diff
changeset
|
147 |
|
34839 | 148 |
case _ => if (!result.is_ready) bad_result(result) |
34809 | 149 |
} |
150 |
} |
|
151 |
else if (result.kind == Isabelle_Process.Kind.EXIT) |
|
152 |
prover = null |
|
34839 | 153 |
else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_raw) |
34837 | 154 |
bad_result(result) |
34809 | 155 |
} |
156 |
||
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
157 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
158 |
/* prover startup */ |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
159 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
160 |
def startup_error(): String = |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
161 |
{ |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
162 |
val buf = new StringBuilder |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
163 |
while ( |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
164 |
receiveWithin(0) { |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
165 |
case result: Isabelle_Process.Result => |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
166 |
if (result.is_raw) { |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
167 |
for (text <- XML.content(result.message)) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
168 |
buf.append(text) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
169 |
} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
170 |
true |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
171 |
case TIMEOUT => false |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
172 |
}) {} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
173 |
buf.toString |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
174 |
} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
175 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
176 |
def prover_startup(timeout: Int): Option[String] = |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
177 |
{ |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
178 |
receiveWithin(timeout) { |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
179 |
case result: Isabelle_Process.Result |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
180 |
if result.kind == Isabelle_Process.Kind.INIT => |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
181 |
while (receive { |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
182 |
case result: Isabelle_Process.Result => |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
183 |
handle_result(result); !result.is_ready |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
184 |
}) {} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
185 |
None |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
186 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
187 |
case result: Isabelle_Process.Result |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
188 |
if result.kind == Isabelle_Process.Kind.EXIT => |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
189 |
Some(startup_error()) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
190 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
191 |
case TIMEOUT => // FIXME clarify |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
192 |
prover.kill; Some(startup_error()) |
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 |
} |
34809 | 195 |
|
196 |
||
197 |
/* main loop */ |
|
198 |
||
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
199 |
val xml_cache = new XML.Cache(131071) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
200 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
201 |
loop { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
202 |
react { |
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
203 |
case Start(timeout, args) => |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
204 |
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
|
205 |
prover = new Isabelle_Process(system, self, args:_*) with Isar_Document |
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
206 |
val origin = sender |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
207 |
val opt_err = prover_startup(timeout) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
208 |
if (opt_err.isDefined) prover = null |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
209 |
origin ! opt_err |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
210 |
} |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
211 |
else reply(None) |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
212 |
|
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
213 |
case Stop => // FIXME clarify; synchronous |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
214 |
if (prover != null) { |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
215 |
prover.kill |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
216 |
prover = null |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
217 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
218 |
|
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
219 |
case Begin_Document(path: String) if prover != null => |
34808
e462572536e9
eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset
|
220 |
val id = create_id() |
34823 | 221 |
val doc = Document.empty(id) |
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
|
222 |
register_document(doc) |
34808
e462572536e9
eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset
|
223 |
prover.begin_document(id, path) |
e462572536e9
eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset
|
224 |
reply(doc) |
34809 | 225 |
|
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
226 |
case change: Change if prover != null => |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
227 |
handle_change(change) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
228 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
229 |
case result: Isabelle_Process.Result => |
34795 | 230 |
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
|
231 |
|
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
232 |
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
|
233 |
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
|
234 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
235 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
236 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
237 |
|
34809 | 238 |
|
239 |
/* main methods */ |
|
240 |
||
34820
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
241 |
def start(timeout: Int, args: List[String]): Option[String] = |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
242 |
(session_actor !? Start(timeout, args)).asInstanceOf[Option[String]] |
a8ba6cde13e9
basic setup for synchronous / modal (!) prover startup;
wenzelm
parents:
34819
diff
changeset
|
243 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
244 |
def stop() { session_actor ! Stop } |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
245 |
def input(change: Change) { session_actor ! change } |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
246 |
|
34823 | 247 |
def begin_document(path: String): Document = |
248 |
(session_actor !? Begin_Document(path)).asInstanceOf[Document] |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
249 |
} |