search

andriusvelykis / isabelle-eclipse

Eclipse integration for Isabelle proof assistant.
http://andriusvelykis.github.io/isabelle-eclipse
Eclipse Public License 1.0
12 stars 4 forks source link

Protocol dialogs #15

Closed andriusvelykis closed 11 years ago

andriusvelykis commented 11 years ago

Isabelle 2013 provides functionality where ML code can raise dialogs requiring some user selection. This appears as text in Prover Output. The selected result is sent back to Isabelle to allow ML code to proceed.

Add support for this feature.

andriusvelykis commented 11 years ago

Implemented in 3bd3923ace3f98f0babddf2de600e160358d34ca

The dialog choices are rendered as hyperlinks and are disabled upon selection. The selected result is sent back to Isabelle.