[isabelle-dev] BASIC dialogs in Isabelle/PIDE

[Makarius]

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!  " ^
     commas
       [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.


 	Makarius