|
1 /* |
|
2 * Isabelle session, potentially with running prover |
|
3 * |
|
4 * @author Makarius |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 import scala.actors.TIMEOUT |
|
11 import scala.actors.Actor._ |
|
12 |
|
13 |
|
14 object Session |
|
15 { |
|
16 /* events */ |
|
17 |
|
18 case object Global_Settings |
|
19 |
|
20 |
|
21 /* managed entities */ |
|
22 |
|
23 type Entity_ID = String |
|
24 |
|
25 trait Entity |
|
26 { |
|
27 val id: Entity_ID |
|
28 def consume(session: Session, message: XML.Tree): Unit |
|
29 } |
|
30 } |
|
31 |
|
32 |
|
33 class Session(system: Isabelle_System) |
|
34 { |
|
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 |
|
44 /* unique ids */ |
|
45 |
|
46 private var id_count: BigInt = 0 |
|
47 def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count } |
|
48 |
|
49 |
|
50 |
|
51 /** main actor **/ |
|
52 |
|
53 @volatile private var syntax = new Outer_Syntax(system.symbols) |
|
54 def current_syntax: Outer_Syntax = syntax |
|
55 |
|
56 @volatile private var entities = Map[Session.Entity_ID, Session.Entity]() |
|
57 def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id) |
|
58 def lookup_command(id: Session.Entity_ID): Option[Command] = |
|
59 lookup_entity(id) match { |
|
60 case Some(cmd: Command) => Some(cmd) |
|
61 case _ => None |
|
62 } |
|
63 |
|
64 private case class Start(timeout: Int, args: List[String]) |
|
65 private case object Stop |
|
66 private case class Begin_Document(path: String) |
|
67 |
|
68 private val session_actor = actor { |
|
69 |
|
70 var prover: Isabelle_Process with Isar_Document = null |
|
71 |
|
72 def register(entity: Session.Entity) { entities += (entity.id -> entity) } |
|
73 |
|
74 var documents = Map[Isar_Document.Document_ID, Document]() |
|
75 def register_document(doc: Document) { documents += (doc.id -> doc) } |
|
76 |
|
77 |
|
78 /* document changes */ |
|
79 |
|
80 def handle_change(change: Change) |
|
81 { |
|
82 require(change.parent.isDefined) |
|
83 |
|
84 val (changes, doc) = change.result.join |
|
85 val id_changes = changes map { |
|
86 case (c1, c2) => |
|
87 (c1.map(_.id).getOrElse(""), |
|
88 c2 match { |
|
89 case None => None |
|
90 case Some(command) => |
|
91 if (!lookup_command(command.id).isDefined) { |
|
92 register(command) |
|
93 prover.define_command(command.id, system.symbols.encode(command.source)) |
|
94 } |
|
95 Some(command.id) |
|
96 }) |
|
97 } |
|
98 register_document(doc) |
|
99 prover.edit_document(change.parent.get.id, doc.id, id_changes) |
|
100 } |
|
101 |
|
102 |
|
103 /* prover results */ |
|
104 |
|
105 def bad_result(result: Isabelle_Process.Result) |
|
106 { |
|
107 System.err.println("Ignoring prover result: " + result) |
|
108 } |
|
109 |
|
110 def handle_result(result: Isabelle_Process.Result) |
|
111 { |
|
112 raw_results.event(result) |
|
113 |
|
114 val target_id: Option[Session.Entity_ID] = Position.get_id(result.props) |
|
115 val target: Option[Session.Entity] = |
|
116 target_id match { |
|
117 case None => None |
|
118 case Some(id) => lookup_entity(id) |
|
119 } |
|
120 if (target.isDefined) target.get.consume(this, result.message) |
|
121 else if (result.kind == Isabelle_Process.Kind.STATUS) { |
|
122 // global status message |
|
123 result.body match { |
|
124 |
|
125 // document state assigment |
|
126 case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined => |
|
127 documents.get(target_id.get) match { |
|
128 case Some(doc) => |
|
129 val states = |
|
130 for { |
|
131 XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) |
|
132 <- edits |
|
133 cmd <- lookup_command(cmd_id) |
|
134 } yield { |
|
135 val st = cmd.assign_state(state_id) |
|
136 register(st) |
|
137 (cmd, st) |
|
138 } |
|
139 doc.assign_states(states) |
|
140 case None => bad_result(result) |
|
141 } |
|
142 |
|
143 // command and keyword declarations |
|
144 case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) => |
|
145 syntax += (name, kind) |
|
146 case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) => |
|
147 syntax += name |
|
148 |
|
149 case _ => if (!result.is_ready) bad_result(result) |
|
150 } |
|
151 } |
|
152 else if (result.kind == Isabelle_Process.Kind.EXIT) |
|
153 prover = null |
|
154 else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_raw) |
|
155 bad_result(result) |
|
156 } |
|
157 |
|
158 |
|
159 /* prover startup */ |
|
160 |
|
161 def startup_error(): String = |
|
162 { |
|
163 val buf = new StringBuilder |
|
164 while ( |
|
165 receiveWithin(0) { |
|
166 case result: Isabelle_Process.Result => |
|
167 if (result.is_raw) { |
|
168 for (text <- XML.content(result.message)) |
|
169 buf.append(text) |
|
170 } |
|
171 true |
|
172 case TIMEOUT => false |
|
173 }) {} |
|
174 buf.toString |
|
175 } |
|
176 |
|
177 def prover_startup(timeout: Int): Option[String] = |
|
178 { |
|
179 receiveWithin(timeout) { |
|
180 case result: Isabelle_Process.Result |
|
181 if result.kind == Isabelle_Process.Kind.INIT => |
|
182 while (receive { |
|
183 case result: Isabelle_Process.Result => |
|
184 handle_result(result); !result.is_ready |
|
185 }) {} |
|
186 None |
|
187 |
|
188 case result: Isabelle_Process.Result |
|
189 if result.kind == Isabelle_Process.Kind.EXIT => |
|
190 Some(startup_error()) |
|
191 |
|
192 case TIMEOUT => // FIXME clarify |
|
193 prover.kill; Some(startup_error()) |
|
194 } |
|
195 } |
|
196 |
|
197 |
|
198 /* main loop */ |
|
199 |
|
200 val xml_cache = new XML.Cache(131071) |
|
201 |
|
202 loop { |
|
203 react { |
|
204 case Start(timeout, args) => |
|
205 if (prover == null) { |
|
206 prover = new Isabelle_Process(system, self, args:_*) with Isar_Document |
|
207 val origin = sender |
|
208 val opt_err = prover_startup(timeout) |
|
209 if (opt_err.isDefined) prover = null |
|
210 origin ! opt_err |
|
211 } |
|
212 else reply(None) |
|
213 |
|
214 case Stop => // FIXME clarify; synchronous |
|
215 if (prover != null) { |
|
216 prover.kill |
|
217 prover = null |
|
218 } |
|
219 |
|
220 case Begin_Document(path: String) if prover != null => |
|
221 val id = create_id() |
|
222 val doc = Document.empty(id) |
|
223 register_document(doc) |
|
224 prover.begin_document(id, path) |
|
225 reply(doc) |
|
226 |
|
227 case change: Change if prover != null => |
|
228 handle_change(change) |
|
229 |
|
230 case result: Isabelle_Process.Result => |
|
231 handle_result(result.cache(xml_cache)) |
|
232 |
|
233 case bad if prover != null => |
|
234 System.err.println("session_actor: ignoring bad message " + bad) |
|
235 } |
|
236 } |
|
237 } |
|
238 |
|
239 |
|
240 /* main methods */ |
|
241 |
|
242 def start(timeout: Int, args: List[String]): Option[String] = |
|
243 (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]] |
|
244 |
|
245 def stop() { session_actor ! Stop } |
|
246 def input(change: Change) { session_actor ! change } |
|
247 |
|
248 def begin_document(path: String): Document = |
|
249 (session_actor !? Begin_Document(path)).asInstanceOf[Document] |
|
250 } |