src/Tools/jEdit/src/proofdocument/session.scala
changeset 34839 3457436a1110
parent 34837 aa73039d5d14
child 34848 77ac13833972
equal deleted inserted replaced
34838:08a72dc4868e 34839:3457436a1110
   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 */