Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing



On Fri, 8 Aug 2014, Andreas Lochbihler wrote:

When I use the Query and Sledgehammer panels heavily, PIDE regularly gets into a state where the theory text has a grey background, but I cannot get it to resume working any more (There is also no process running, the CPU is idle). The GUI itself is reactive, but I cannot get any feedback from Isabelle any more. The Syslog only shows the welcome message and Raw Output is empty. I then have to shut down jEdit and restart PIDE.

There must have been a protocol crash somewhere at the bottom. The next time when this happens, there are a few things that can be checked to pin it down more precisely:

  * jEdit menu Utilities / Troubleshooting / Activity Log for JVM
    exception traces -- if you run "isabelle jedit" on the command line
    there should be information on the terminal as well.

  * The following simple test of the ML/Scala protocol handler:

    - open Raw Output panel, to make it active before trying anything

    - open Console/Scala and emit this command:

        PIDE.session.protocol_command("Prover.echo", "test")

      The result "test" should appear on raw output.  This is the command
      loop of the prover process in PIDE wrapping.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.