[isabelle-dev] BASIC dialogs in Isabelle/PIDE

Makarius makarius at sketis.net
Fri Dec 14 15:46:18 CET 2012

Since several people have raised this issue in the past few weeks, I am 
posting here an example how the user can interact with the document model 
in the manner of ancient TTY applications.

Anyone still remembers pause_tac?  Reading user input on stdin was ruled 
out in the Proof General model, but in Isabelle/bd145273e7c6 it works 
again like this:

ML_command {*
   val (text, promise) = Active.dialog_text ();
   writeln ("Something went utterly wrong!  " ^
       [text "Abort",
        text "Retry",
        text "Ignore",
        text "Fail"] ^ "?");
   writeln (Future.join promise);

The dialog happens in the Output panel, for example.  Tooltips are not 
dynamically updated, so clicking on one of the choices works, but there is 
no immediate feedback.


More information about the isabelle-dev mailing list