121 else if (result.kind == Isabelle_Process.Kind.STATUS) { |
121 else if (result.kind == Isabelle_Process.Kind.STATUS) { |
122 // global status message |
122 // global status message |
123 result.body match { |
123 result.body match { |
124 |
124 |
125 // document state assignment |
125 // document state assignment |
126 case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined => |
126 case List(Isar_Document.Assign(edits)) if target_id.isDefined => |
127 documents.get(target_id.get) match { |
127 documents.get(target_id.get) match { |
128 case Some(doc) => |
128 case Some(doc) => |
129 val states = |
129 val states = |
130 for { |
130 for { |
131 XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) <- edits |
131 Isar_Document.Edit(cmd_id, state_id) <- edits |
132 cmd <- lookup_command(cmd_id) |
132 cmd <- lookup_command(cmd_id) |
133 } yield { |
133 } yield { |
134 val st = cmd.assign_state(state_id) |
134 val st = cmd.assign_state(state_id) |
135 register(st) |
135 register(st) |
136 (cmd, st) |
136 (cmd, st) |
137 } |
137 } |
138 doc.assign_states(states) |
138 doc.assign_states(states) |
139 case None => bad_result(result) |
139 case None => bad_result(result) |
140 } |
140 } |
141 |
141 |
142 // command and keyword declarations |
142 // keyword declarations |
143 case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) => |
143 case List(Outer_Keyword.Command_Decl(name, kind)) => syntax += (name, kind) |
144 syntax += (name, kind) |
144 case List(Outer_Keyword.Keyword_Decl(name)) => syntax += name |
145 case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) => |
|
146 syntax += name |
|
147 |
145 |
148 case _ => if (!result.is_ready) bad_result(result) |
146 case _ => if (!result.is_ready) bad_result(result) |
149 } |
147 } |
150 } |
148 } |
151 else if (result.kind == Isabelle_Process.Kind.EXIT) |
149 else if (result.kind == Isabelle_Process.Kind.EXIT) |