author | wenzelm |
Wed, 16 Dec 2009 21:11:04 +0100 | |
changeset 34791 | b97d5b38dea4 |
parent 34780 | d0ff1c3a91ea |
child 34792 | 65130daf2883 |
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 |
|
34791 | 12 |
object Session |
13 |
{ |
|
14 |
case object Global_Settings |
|
15 |
} |
|
16 |
||
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
17 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
18 |
class Session(system: Isabelle_System) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
19 |
{ |
34778 | 20 |
/* unique ids */ |
21 |
||
22 |
private var id_count: BigInt = 0 |
|
23 |
def create_id(): String = synchronized { id_count += 1; "j" + id_count } |
|
24 |
||
25 |
||
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
26 |
/* main actor */ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
27 |
|
34780 | 28 |
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
|
29 |
private case object Stop |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
30 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
31 |
private var prover: Isabelle_Process with Isar_Document = null |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
32 |
private var prover_ready = false |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
33 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
34 |
private val session_actor = actor { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
35 |
loop { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
36 |
react { |
34780 | 37 |
case Start(args) => |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
38 |
if (prover == null) { |
34780 | 39 |
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
|
40 |
reply(()) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
41 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
42 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
43 |
case Stop => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
44 |
if (prover != null) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
45 |
prover.kill |
34778 | 46 |
prover_ready = false |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
47 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
48 |
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
|
49 |
handle_change(change) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
50 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
51 |
case result: Isabelle_Process.Result => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
52 |
handle_result(result) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
53 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
54 |
case bad if prover_ready => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
55 |
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
|
56 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
57 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
58 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
59 |
|
34780 | 60 |
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
|
61 |
def stop() { session_actor ! Stop } |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
62 |
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
|
63 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
64 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
65 |
/* pervasive event buses */ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
66 |
|
34791 | 67 |
val global_settings = new Event_Bus[Session.Global_Settings.type] |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
68 |
val raw_results = new Event_Bus[Isabelle_Process.Result] |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
69 |
val results = new Event_Bus[Command] |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
70 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
71 |
val command_change = new Event_Bus[Command] |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
72 |
val document_change = new Event_Bus[Proof_Document] |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
73 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
74 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
75 |
/* selected state */ // FIXME!? races!? |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
76 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
77 |
private var _selected_state: Command = null |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
78 |
def selected_state = _selected_state |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
79 |
def selected_state_=(state: Command) { _selected_state = state; results.event(state) } |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
80 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
81 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
82 |
/* outer syntax keywords and completion */ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
83 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
84 |
@volatile private var _command_decls = Map[String, String]() |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
85 |
def command_decls() = _command_decls |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
86 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
87 |
@volatile private var _keyword_decls = Set[String]() |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
88 |
def keyword_decls() = _keyword_decls |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
89 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
90 |
@volatile private var _completion = new Completion + system.symbols |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
91 |
def completion() = _completion |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
92 |
|
34778 | 93 |
def is_command_keyword(s: String): Boolean = command_decls().contains(s) |
94 |
||
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
95 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
96 |
/* document state information */ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
97 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
98 |
@volatile private var states = Map[Isar_Document.State_ID, Command_State]() |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
99 |
@volatile private var commands = Map[Isar_Document.Command_ID, Command]() |
34778 | 100 |
val document_0 = Proof_Document.empty(create_id()) // FIXME fresh id (!??) |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
101 |
@volatile private var document_versions = List(document_0) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
102 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
103 |
def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
104 |
def document(id: Isar_Document.Document_ID): Option[Proof_Document] = |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
105 |
document_versions.find(_.id == id) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
106 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
107 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
108 |
/* document changes */ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
109 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
110 |
def begin_document(path: String) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
111 |
{ |
34778 | 112 |
prover.begin_document(document_0.id, path) // FIXME fresh document!?! |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
113 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
114 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
115 |
def handle_change(change: Change) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
116 |
{ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
117 |
val old = document(change.parent.get.id).get |
34778 | 118 |
val (doc, changes) = old.text_changed(this, change) |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
119 |
document_versions ::= doc |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
120 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
121 |
val id_changes = changes map { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
122 |
case (c1, c2) => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
123 |
(c1.map(_.id).getOrElse(document_0.id), |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
124 |
c2 match { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
125 |
case None => None |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
126 |
case Some(command) => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
127 |
commands += (command.id -> command) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
128 |
prover.define_command(command.id, system.symbols.encode(command.content)) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
129 |
Some(command.id) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
130 |
}) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
131 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
132 |
prover.edit_document(old.id, doc.id, id_changes) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
133 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
134 |
document_change.event(doc) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
135 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
136 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
137 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
138 |
/* prover results */ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
139 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
140 |
private def handle_result(result: Isabelle_Process.Result) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
141 |
{ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
142 |
raw_results.event(result) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
143 |
val message = Isabelle_Process.parse_message(system, result) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
144 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
145 |
val state = |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
146 |
Position.id_of(result.props) match { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
147 |
case None => None |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
148 |
case Some(id) => commands.get(id) orElse states.get(id) orElse None |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
149 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
150 |
if (state.isDefined) state.get ! (this, message) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
151 |
else if (result.kind == Isabelle_Process.Kind.STATUS) { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
152 |
//{{{ global status message |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
153 |
message match { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
154 |
case XML.Elem(Markup.MESSAGE, _, elems) => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
155 |
for (elem <- elems) { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
156 |
elem match { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
157 |
// document edits |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
158 |
case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
159 |
document_versions.find(_.id == doc_id) match { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
160 |
case Some(doc) => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
161 |
for { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
162 |
XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
163 |
<- edits } |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
164 |
{ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
165 |
commands.get(cmd_id) match { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
166 |
case Some(cmd) => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
167 |
val state = new Command_State(cmd) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
168 |
states += (state_id -> state) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
169 |
doc.states += (cmd -> state) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
170 |
command_change.event(cmd) // FIXME really!? |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
171 |
case None => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
172 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
173 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
174 |
case None => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
175 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
176 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
177 |
// command and keyword declarations |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
178 |
case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
179 |
_command_decls += (name -> kind) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
180 |
_completion += name |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
181 |
case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
182 |
_keyword_decls += name |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
183 |
_completion += name |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
184 |
|
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
185 |
// process ready (after initialization) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
186 |
case XML.Elem(Markup.READY, _, _) => prover_ready = true |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
187 |
|
34778 | 188 |
case _ => |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
189 |
} |
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 _ => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
192 |
} |
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 |
} |
34778 | 195 |
else if (result.kind == Isabelle_Process.Kind.EXIT) |
196 |
prover = null |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
197 |
} |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
diff
changeset
|
198 |
} |