equal
deleted
inserted
replaced
144 case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) => |
144 case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) => |
145 syntax += (name, kind) |
145 syntax += (name, kind) |
146 case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) => |
146 case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) => |
147 syntax += name |
147 syntax += name |
148 |
148 |
149 case _ => bad_result(result) |
149 case _ => if (!result.is_ready) bad_result(result) |
150 } |
150 } |
151 } |
151 } |
152 else if (result.kind == Isabelle_Process.Kind.EXIT) |
152 else if (result.kind == Isabelle_Process.Kind.EXIT) |
153 prover = null |
153 prover = null |
154 else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_ready) |
154 else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_raw) |
155 bad_result(result) |
155 bad_result(result) |
156 } |
156 } |
157 |
157 |
158 |
158 |
159 /* prover startup */ |
159 /* prover startup */ |