author | wenzelm |
Wed, 30 Dec 2009 20:26:08 +0100 | |
changeset 34817 | b4efd0ef2f3e |
parent 34816 | d33312514220 |
child 34818 | 7df68a8f0e3e |
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 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.proofdocument |
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 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
10 |
import scala.actors.Actor._ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
11 |
|
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
12 |
|
34791 | 13 |
object Session |
14 |
{ |
|
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
15 |
/* events */ |
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
16 |
|
34791 | 17 |
case object Global_Settings |
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
18 |
|
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 |
/* managed entities */ |
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
21 |
|
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
22 |
type Entity_ID = String |
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
23 |
|
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
24 |
trait Entity |
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 |
val id: Entity_ID |
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
27 |
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
|
28 |
} |
34791 | 29 |
} |
30 |
||
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
31 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
32 |
class Session(system: Isabelle_System) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
33 |
{ |
34809 | 34 |
/* pervasive event buses */ |
35 |
||
36 |
val global_settings = new Event_Bus[Session.Global_Settings.type] |
|
37 |
val raw_results = new Event_Bus[Isabelle_Process.Result] |
|
38 |
val results = new Event_Bus[Command] |
|
39 |
||
40 |
val command_change = new Event_Bus[Command] |
|
41 |
val document_change = new Event_Bus[Proof_Document] |
|
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 |
||
34810 | 50 |
/* document state information -- owned by session_actor */ |
34809 | 51 |
|
52 |
@volatile private var outer_syntax = new Outer_Syntax(system.symbols) |
|
53 |
def syntax(): Outer_Syntax = outer_syntax |
|
54 |
||
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
55 |
@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
|
56 |
def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id) |
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
57 |
|
34809 | 58 |
@volatile private var documents = Map[Isar_Document.Document_ID, Proof_Document]() |
59 |
def document(id: Isar_Document.Document_ID): Option[Proof_Document] = documents.get(id) |
|
60 |
||
61 |
||
62 |
/** main actor **/ |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
63 |
|
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
64 |
private case class Register(entity: Session.Entity) |
34780 | 65 |
private case class Start(args: List[String]) |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
66 |
private case object Stop |
34808
e462572536e9
eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset
|
67 |
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
|
68 |
|
34809 | 69 |
private val session_actor = actor { |
70 |
||
71 |
var prover: Isabelle_Process with Isar_Document = null |
|
72 |
var prover_ready = false |
|
73 |
||
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
74 |
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
|
75 |
|
34809 | 76 |
|
77 |
/* document changes */ |
|
78 |
||
79 |
def handle_change(change: Change) |
|
80 |
{ |
|
81 |
val old = document(change.parent.get.id).get |
|
82 |
val (doc, changes) = old.text_changed(this, change) |
|
83 |
||
84 |
val id_changes = changes map { |
|
85 |
case (c1, c2) => |
|
86 |
(c1.map(_.id).getOrElse(""), |
|
87 |
c2 match { |
|
88 |
case None => None |
|
89 |
case Some(command) => // FIXME clarify -- may reuse existing commands!?? |
|
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
90 |
register(command) |
34809 | 91 |
prover.define_command(command.id, system.symbols.encode(command.content)) |
92 |
Some(command.id) |
|
93 |
}) |
|
94 |
} |
|
95 |
documents += (doc.id -> doc) |
|
96 |
prover.edit_document(old.id, doc.id, id_changes) |
|
97 |
||
98 |
document_change.event(doc) |
|
99 |
} |
|
100 |
||
101 |
||
102 |
/* prover results */ |
|
103 |
||
104 |
def handle_result(result: Isabelle_Process.Result) |
|
105 |
{ |
|
106 |
raw_results.event(result) |
|
34799
0330a4284a9b
just one variable for outer syntax keywords and completion;
wenzelm
parents:
34795
diff
changeset
|
107 |
|
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
108 |
val target: Option[Session.Entity] = |
34817 | 109 |
Position.get_id(result.props) match { |
34809 | 110 |
case None => None |
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
111 |
case Some(id) => entities.get(id) |
34809 | 112 |
} |
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34810
diff
changeset
|
113 |
if (target.isDefined) target.get.consume(this, result.message) |
34809 | 114 |
else if (result.kind == Isabelle_Process.Kind.STATUS) { |
115 |
//{{{ global status message |
|
116 |
for (elem <- result.body) { |
|
117 |
elem match { |
|
118 |
// document edits |
|
119 |
case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) => |
|
120 |
document(doc_id) match { |
|
121 |
case None => // FIXME clarify |
|
122 |
case Some(doc) => |
|
123 |
for { |
|
124 |
XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) |
|
125 |
<- edits } |
|
126 |
{ |
|
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
127 |
entities.get(cmd_id) match { |
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
128 |
case Some(cmd: Command) => |
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
129 |
val state = cmd.finish_static(state_id) |
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
130 |
register(state) |
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
131 |
doc.states += (cmd -> state) // FIXME !? |
34809 | 132 |
command_change.event(cmd) // FIXME really!? |
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
133 |
case _ => |
34809 | 134 |
} |
135 |
} |
|
136 |
} |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
137 |
|
34809 | 138 |
// command and keyword declarations |
139 |
case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => |
|
140 |
outer_syntax += (name, kind) |
|
141 |
case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => |
|
142 |
outer_syntax += name |
|
143 |
||
144 |
// process ready (after initialization) |
|
145 |
case XML.Elem(Markup.READY, _, _) => prover_ready = true |
|
146 |
||
147 |
case _ => |
|
148 |
} |
|
149 |
} |
|
150 |
//}}} |
|
151 |
} |
|
152 |
else if (result.kind == Isabelle_Process.Kind.EXIT) |
|
153 |
prover = null |
|
154 |
} |
|
155 |
||
34795 | 156 |
val xml_cache = new XML.Cache(131071) |
34809 | 157 |
|
158 |
||
159 |
/* main loop */ |
|
160 |
||
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
161 |
loop { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
162 |
react { |
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
163 |
case Register(entity: Session.Entity) => |
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
164 |
register(entity) |
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
165 |
reply(()) |
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
166 |
|
34780 | 167 |
case Start(args) => |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
168 |
if (prover == null) { |
34780 | 169 |
prover = new Isabelle_Process(system, self, args:_*) with Isar_Document |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
170 |
reply(()) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
171 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
172 |
|
34807 | 173 |
case Stop => // FIXME clarify |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
174 |
if (prover != null) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
175 |
prover.kill |
34778 | 176 |
prover_ready = false |
34808
e462572536e9
eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset
|
177 |
|
e462572536e9
eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset
|
178 |
case Begin_Document(path: String) if prover_ready => |
e462572536e9
eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset
|
179 |
val id = create_id() |
e462572536e9
eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset
|
180 |
val doc = Proof_Document.empty(id) |
e462572536e9
eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset
|
181 |
documents += (id -> doc) |
e462572536e9
eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset
|
182 |
prover.begin_document(id, path) |
e462572536e9
eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset
|
183 |
reply(doc) |
34809 | 184 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
185 |
case change: Change if prover_ready => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
186 |
handle_change(change) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
187 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
188 |
case result: Isabelle_Process.Result => |
34795 | 189 |
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
|
190 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
191 |
case bad if prover_ready => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
192 |
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
|
193 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
194 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
195 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
196 |
|
34809 | 197 |
|
198 |
/* main methods */ |
|
199 |
||
34816
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
200 |
def register_entity(entity: Session.Entity) { session_actor !? Register(entity) } |
d33312514220
maintain generic session entities -- cover commands, states, etc. (but not yet documents);
wenzelm
parents:
34815
diff
changeset
|
201 |
|
34780 | 202 |
def start(args: List[String]) { session_actor !? Start(args) } |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
203 |
def stop() { session_actor ! Stop } |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
204 |
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
|
205 |
|
34808
e462572536e9
eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset
|
206 |
def begin_document(path: String): Proof_Document = |
e462572536e9
eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset
|
207 |
(session_actor !? Begin_Document(path)).asInstanceOf[Proof_Document] |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
208 |
} |