[isabelle] RC2: Sledgehammer blocks other functionality



Hi,

a running sledgehammer instance does no longer block the output window
(including goal state) [as it did in Isabelle2015], however, it still
blocks the query-panels.

The find theorems-panel will not come back with output until
sledgehammer has finished. The same for the find constants and print
context panels.

In my opinion, (usually long-running) background sledgehammer tasks
should have less priority than (usually short running) query-tasks, in
particular, as the normal usage pattern is most likely to start
sledgehammer in the background, and, in parallel, exploring ways to
solve the goal manually, e.g., using find-theorems to search for
suitable theorems.

--
  Peter






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