licenses: convert license tags to SPDX

Isabelle2018: new "op x" syntax; now is "(x)"

(result of "isabelle update_op -m <dir>")

globally use session-qualified imports; add Lib session

Session-qualified imports will be required for Isabelle2018 and help clarify
the structure of sessions in the build tree.

This commit mainly adds a new set of sessions for lib/, including a Lib
session that includes most theories in lib/ and a few separate sessions for
parts that have dependencies beyond CParser or are separate AFP sessions.
The group "lib" collects all lib/ sessions.

As a consequence, other theories should use lib/ theories by session name,
not by path, which in turns means spec and proof sessions should also refer
to each other by session name, not path, to avoid duplicate theory errors in
theory merges later.

lib/apply_debug: show protected subgoals

This overrides the default proof state printing function to also
show any subgoals which have been hidden (protected).

This makes proof states shown during apply_debug more
comprehensible.

apply_debug: avoid hanging in batch mode

apply_debug: added "show_running" flag

Default behaviour now doesn't mark up the currently
running method - this seemed too confusing.

apply_debug: hilight calling method

Both the breakpoint and "calling" method from
the original expression are highlighted as the breakpoint.

Note jEdit doesn't seem to highlight across theories (buffers?)

apply_debug: use entity markup from Isabelle2016-1

This makes use of modern dynamic markup so that
clicking on a "continue" can show us the current
breakpoint without needed strange proof state print
hacks.

apply_debug: remove per-continue flags

The implementation here was too messy for such an
esoteric feature.

apply_debug: hack max_threads to avoid scheduling issues

I can't figure out how to keep the cleanup phase of the
Executions module while circumventing the scheduling limitation
imposed by max_threads.

This workaround just keeps max_threads high enough to schedule the threads needed
by all active apply_debug sessions.

apply_debug: more robust fact binding for break method

apply_debug: fix match issue

add testing file

apply_debug: make "break" syntax to capture tokens

This avoids mandatory "bounds" and lets break highlighting occur
inside of matches/eisbach methods

apply_debug: bind Eisbach context during break

This requires a few tricks, since this isn't readily available.

apply_debug: discard context modifications

Demotes "break" to a regular tactic, simplifying its integration with other tools

apply_debug: avoid hacks in evaluation markup

Fixed issue where match was executed in closure state

apply_debug: clear initial dependencies for trace

apply_debug: allow tags/trace in either order

apply_debug: integrate apply_trace

New "trace" modifier lets you trace between continues

apply_debug: use one less thread

Naive use of futures/forking causes apply_debug to block if
not enough threads are available.

apply_debug: add "wp" breakpoint

Lift low-level wp tactic into context_tactic to support
breakpoints modifying context (i.e. wp set)

apply_debug: cleanup test code

apply_debug: allow per-continue tags

apply_debug: add method-based breakpoint filtering

Also fix breakpoint hilights to work when no subgoals are present

apply_debug: support break tags

Only trigger breakpoints based on active tags

apply_debug: hilight active breakpoint, cleanup

Inject a dummy print translation to guess which breakpoint is being looked at.

apply_debug: capture execution errors

- Avoid throwing exceptions on the proof thread, instead defer it to the final slot

- Manage current-method markup with extra thread, this properly clears on proof thread restarts

apply_debug: more synchronization issues

- Avoid starting the restart-managing thread until we have the first result.
- Fix accidental immediate restart.
- Better generational tracking to avoid stale threads manipulating the current
proof thread.

apply_debug: fix some synchronization issues

Generational tracking of tactic excursions and restarts
should block until previous results have been processed

apply_debug: add support for method re-play

This allows for execution to restart and re-play up
to the current "continue", regardless of whether or not
the overall execution has moved past it.