53 def syntax(): Outer_Syntax = outer_syntax |
53 def syntax(): Outer_Syntax = outer_syntax |
54 |
54 |
55 @volatile private var entities = Map[Session.Entity_ID, Session.Entity]() |
55 @volatile private var entities = Map[Session.Entity_ID, Session.Entity]() |
56 def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id) |
56 def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id) |
57 |
57 |
|
58 // FIXME eliminate |
58 @volatile private var documents = Map[Isar_Document.Document_ID, Proof_Document]() |
59 @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 def document(id: Isar_Document.Document_ID): Option[Proof_Document] = documents.get(id) |
|
61 |
60 |
62 |
61 |
63 |
62 /** main actor **/ |
64 /** main actor **/ |
63 |
65 |
64 private case class Register(entity: Session.Entity) |
66 private case class Register(entity: Session.Entity) |
90 register(command) |
92 register(command) |
91 prover.define_command(command.id, system.symbols.encode(command.content)) |
93 prover.define_command(command.id, system.symbols.encode(command.content)) |
92 Some(command.id) |
94 Some(command.id) |
93 }) |
95 }) |
94 } |
96 } |
|
97 register(doc) |
95 documents += (doc.id -> doc) |
98 documents += (doc.id -> doc) |
96 prover.edit_document(old.id, doc.id, id_changes) |
99 prover.edit_document(old.id, doc.id, id_changes) |
97 |
100 |
98 document_change.event(doc) |
101 document_change.event(doc) |
99 } |
102 } |
110 case None => None |
113 case None => None |
111 case Some(id) => entities.get(id) |
114 case Some(id) => entities.get(id) |
112 } |
115 } |
113 if (target.isDefined) target.get.consume(this, result.message) |
116 if (target.isDefined) target.get.consume(this, result.message) |
114 else if (result.kind == Isabelle_Process.Kind.STATUS) { |
117 else if (result.kind == Isabelle_Process.Kind.STATUS) { |
115 //{{{ global status message |
118 // global status message |
116 for (elem <- result.body) { |
119 for (elem <- result.body) { |
117 elem match { |
120 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 { |
|
127 entities.get(cmd_id) match { |
|
128 case Some(cmd: Command) => |
|
129 val state = cmd.finish_static(state_id) |
|
130 register(state) |
|
131 doc.states += (cmd -> state) // FIXME !? |
|
132 command_change.event(cmd) // FIXME really!? |
|
133 case _ => |
|
134 } |
|
135 } |
|
136 } |
|
137 |
|
138 // command and keyword declarations |
121 // command and keyword declarations |
139 case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => |
122 case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => |
140 outer_syntax += (name, kind) |
123 outer_syntax += (name, kind) |
141 case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => |
124 case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => |
142 outer_syntax += name |
125 outer_syntax += name |
176 prover_ready = false |
158 prover_ready = false |
177 |
159 |
178 case Begin_Document(path: String) if prover_ready => |
160 case Begin_Document(path: String) if prover_ready => |
179 val id = create_id() |
161 val id = create_id() |
180 val doc = Proof_Document.empty(id) |
162 val doc = Proof_Document.empty(id) |
|
163 register(doc) |
181 documents += (id -> doc) |
164 documents += (id -> doc) |
182 prover.begin_document(id, path) |
165 prover.begin_document(id, path) |
183 reply(doc) |
166 reply(doc) |
184 |
167 |
185 case change: Change if prover_ready => |
168 case change: Change if prover_ready => |