support dialog via document content;
authorwenzelm
Wed Dec 12 21:50:42 2012 +0100 (2012-12-12 ago)
changeset 504986647ba2775c1
parent 50497 492953de3090
child 50499 f496b2b7bafb
support dialog via document content;
src/Pure/PIDE/active.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/ROOT.ML
src/Pure/System/session.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/active.ML	Wed Dec 12 19:03:49 2012 +0100
     1.2 +++ b/src/Pure/PIDE/active.ML	Wed Dec 12 21:50:42 2012 +0100
     1.3 @@ -11,27 +11,54 @@
     1.4    val markup: string -> string -> string
     1.5    val sendback_markup_implicit: string -> string
     1.6    val sendback_markup: string -> string
     1.7 +  val dialog: unit -> (string -> Markup.T) * string future
     1.8 +  val dialog_result: string -> string -> unit
     1.9  end;
    1.10  
    1.11  structure Active: ACTIVE =
    1.12  struct
    1.13  
    1.14 +(* active markup *)
    1.15 +
    1.16 +fun explicit_id () =
    1.17 +  (case Position.get_id (Position.thread_data ()) of
    1.18 +    SOME id => [(Markup.idN, id)]
    1.19 +  | NONE => []);
    1.20 +
    1.21  fun make_markup name {implicit, properties} =
    1.22    (name, [])
    1.23 -  |> not implicit ? (fn markup =>
    1.24 -      let
    1.25 -        val props =
    1.26 -          (case Position.get_id (Position.thread_data ()) of
    1.27 -            SOME id => [(Markup.idN, id)]
    1.28 -          | NONE => []);
    1.29 -      in Markup.properties props markup end)
    1.30 +  |> not implicit ? (fn markup => Markup.properties (explicit_id ()) markup)
    1.31    |> Markup.properties properties;
    1.32  
    1.33  fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s;
    1.34  fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s;
    1.35  
    1.36 +
    1.37 +(* sendback area *)
    1.38 +
    1.39  val sendback_markup_implicit = markup_implicit Markup.sendbackN;
    1.40  val sendback_markup = markup Markup.sendbackN;
    1.41  
    1.42 +
    1.43 +(* dialog via document content *)
    1.44 +
    1.45 +val new_name = string_of_int o Synchronized.counter ();
    1.46 +
    1.47 +val dialogs = Synchronized.var "Active.dialogs" (Symtab.empty: string future Symtab.table);
    1.48 +
    1.49 +fun dialog () =
    1.50 +  let
    1.51 +    val name = new_name ();
    1.52 +    fun abort () = Synchronized.change dialogs (Symtab.delete_safe name);
    1.53 +    val promise = Future.promise abort : string future;
    1.54 +    val _ = Synchronized.change dialogs (Symtab.update_new (name, promise));
    1.55 +    fun mk_markup result = Markup.properties (explicit_id ()) (Markup.dialog name result);
    1.56 +  in (mk_markup, promise) end;
    1.57 +
    1.58 +fun dialog_result name result =
    1.59 +  Synchronized.change_result dialogs
    1.60 +    (fn tab => (Symtab.lookup tab name, Symtab.delete_safe name tab))
    1.61 +  |> (fn NONE => () | SOME promise => Future.fulfill promise result);
    1.62 +
    1.63  end;
    1.64  
     2.1 --- a/src/Pure/PIDE/markup.ML	Wed Dec 12 19:03:49 2012 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Wed Dec 12 21:50:42 2012 +0100
     2.3 @@ -99,6 +99,7 @@
     2.4    val paddingN: string
     2.5    val padding_line: string * string
     2.6    val sendbackN: string
     2.7 +  val dialogN: string val dialog: string -> string -> T
     2.8    val graphviewN: string
     2.9    val intensifyN: string val intensify: T
    2.10    val taskN: string
    2.11 @@ -338,9 +339,13 @@
    2.12  val (subgoalN, subgoal) = markup_elem "subgoal";
    2.13  
    2.14  
    2.15 -(* active areads *)
    2.16 +(* active areas *)
    2.17  
    2.18  val sendbackN = "sendback";
    2.19 +
    2.20 +val dialogN = "dialog";
    2.21 +fun dialog name result = (dialogN, [(nameN, name), ("result", result)]);
    2.22 +
    2.23  val graphviewN = "graphview";
    2.24  
    2.25  val paddingN = "padding";
     3.1 --- a/src/Pure/PIDE/markup.scala	Wed Dec 12 19:03:49 2012 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Wed Dec 12 21:50:42 2012 +0100
     3.3 @@ -216,6 +216,11 @@
     3.4    /* active areas */
     3.5  
     3.6    val SENDBACK = "sendback"
     3.7 +
     3.8 +  val DIALOG = "dialog"
     3.9 +  val DIALOG_RESULT = "dialog_result"
    3.10 +  val Result = new Properties.String("result")
    3.11 +
    3.12    val GRAPHVIEW = "graphview"
    3.13  
    3.14    val PADDING = "padding"
     4.1 --- a/src/Pure/PIDE/protocol.ML	Wed Dec 12 19:03:49 2012 +0100
     4.2 +++ b/src/Pure/PIDE/protocol.ML	Wed Dec 12 21:50:42 2012 +0100
     4.3 @@ -76,6 +76,12 @@
     4.4        in state1 end));
     4.5  
     4.6  val _ =
     4.7 +  Isabelle_Process.protocol_command "Document.dialog_result"
     4.8 +    (fn [name, result] =>
     4.9 +      Active.dialog_result name result
    4.10 +        handle exn => if Exn.is_interrupt exn then () else reraise exn);
    4.11 +
    4.12 +val _ =
    4.13    Isabelle_Process.protocol_command "Document.invoke_scala"
    4.14      (fn [id, tag, res] =>
    4.15        Invoke_Scala.fulfill_method id tag res
     5.1 --- a/src/Pure/PIDE/protocol.scala	Wed Dec 12 19:03:49 2012 +0100
     5.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Dec 12 21:50:42 2012 +0100
     5.3 @@ -269,6 +269,14 @@
     5.4    }
     5.5  
     5.6  
     5.7 +  /* dialog via document content */
     5.8 +
     5.9 +  def dialog_result(name: String, result: String)
    5.10 +  {
    5.11 +    input("Document.dialog_result", name, result)
    5.12 +  }
    5.13 +
    5.14 +
    5.15    /* method invocation service */
    5.16  
    5.17    def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
     6.1 --- a/src/Pure/ROOT.ML	Wed Dec 12 19:03:49 2012 +0100
     6.2 +++ b/src/Pure/ROOT.ML	Wed Dec 12 21:50:42 2012 +0100
     6.3 @@ -63,7 +63,6 @@
     6.4  
     6.5  use "PIDE/xml.ML";
     6.6  use "PIDE/yxml.ML";
     6.7 -use "PIDE/active.ML";
     6.8  
     6.9  use "General/graph.ML";
    6.10  
    6.11 @@ -252,6 +251,7 @@
    6.12  use "Thy/term_style.ML";
    6.13  use "Thy/thy_output.ML";
    6.14  use "Thy/thy_syntax.ML";
    6.15 +use "PIDE/active.ML";
    6.16  use "PIDE/command.ML";
    6.17  use "Isar/outer_syntax.ML";
    6.18  use "General/graph_display.ML";
     7.1 --- a/src/Pure/System/session.scala	Wed Dec 12 19:03:49 2012 +0100
     7.2 +++ b/src/Pure/System/session.scala	Wed Dec 12 21:50:42 2012 +0100
     7.3 @@ -26,6 +26,7 @@
     7.4    case class Global_Options(options: Options)
     7.5    case object Caret_Focus
     7.6    case class Raw_Edits(edits: List[Document.Edit_Text])
     7.7 +  case class Dialog_Result(id: Document.ID, name: String, result: String)
     7.8    case class Commands_Changed(
     7.9      assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
    7.10  
    7.11 @@ -419,6 +420,14 @@
    7.12  
    7.13            reply(())
    7.14  
    7.15 +        case Session.Dialog_Result(id, name, result) if prover.isDefined =>
    7.16 +          prover.get.dialog_result(name, result)
    7.17 +
    7.18 +          val dialog_result =
    7.19 +            XML.Elem(Markup(Markup.DIALOG_RESULT, Markup.Name(name) ::: Markup.Result(result)), Nil)
    7.20 +          handle_output(new Isabelle_Process.Output(
    7.21 +            XML.Elem(Markup(Markup.REPORT, Position.Id(id)), List(dialog_result))))
    7.22 +
    7.23          case Messages(msgs) =>
    7.24            msgs foreach {
    7.25              case input: Isabelle_Process.Input =>
    7.26 @@ -469,4 +478,7 @@
    7.27  
    7.28    def update(edits: List[Document.Edit_Text])
    7.29    { session_actor !? Session.Raw_Edits(edits) }
    7.30 +
    7.31 +  def dialog_result(id: Document.ID, name: String, result: String)
    7.32 +  { session_actor ! Session.Dialog_Result(id, name, result) }
    7.33  }
     8.1 --- a/src/Tools/jEdit/etc/options	Wed Dec 12 19:03:49 2012 +0100
     8.2 +++ b/src/Tools/jEdit/etc/options	Wed Dec 12 21:50:42 2012 +0100
     8.3 @@ -43,6 +43,7 @@
     8.4  option hyperlink_color : string = "000000FF"
     8.5  option active_color : string = "DCDCDCFF"
     8.6  option active_hover_color : string = "9DC75DFF"
     8.7 +option active_result_color : string = "666633FF"
     8.8  option keyword1_color : string = "006699FF"
     8.9  option keyword2_color : string = "009966FF"
    8.10  
     9.1 --- a/src/Tools/jEdit/src/active.scala	Wed Dec 12 19:03:49 2012 +0100
     9.2 +++ b/src/Tools/jEdit/src/active.scala	Wed Dec 12 21:50:42 2012 +0100
     9.3 @@ -54,6 +54,13 @@
     9.4                      else text_area.setSelectedText(text)
     9.5                  }
     9.6  
     9.7 +              case XML.Elem(Markup(Markup.DIALOG, props), _) =>
     9.8 +                (props, props, props) match {
     9.9 +                  case (Position.Id(id), Markup.Name(name), Markup.Result(result)) =>
    9.10 +                    model.session.dialog_result(id, name, result)
    9.11 +                  case _ =>
    9.12 +                }
    9.13 +
    9.14                case XML.Elem(Markup(Markup.GRAPHVIEW, Position.Id(exec_id)), body) =>
    9.15                  default_thread_pool.submit(() =>
    9.16                    {
    10.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Dec 12 19:03:49 2012 +0100
    10.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Dec 12 21:50:42 2012 +0100
    10.3 @@ -137,6 +137,7 @@
    10.4    val hyperlink_color = color_value("hyperlink_color")
    10.5    val active_color = color_value("active_color")
    10.6    val active_hover_color = color_value("active_hover_color")
    10.7 +  val active_result_color = color_value("active_result_color")
    10.8    val keyword1_color = color_value("keyword1_color")
    10.9    val keyword2_color = color_value("keyword2_color")
   10.10  
   10.11 @@ -249,7 +250,8 @@
   10.12    }
   10.13  
   10.14  
   10.15 -  private val active_include = Set(Markup.SENDBACK, Markup.GRAPHVIEW)
   10.16 +  private val active_include =
   10.17 +    Set(Markup.SENDBACK, Markup.DIALOG, Markup.DIALOG_RESULT, Markup.GRAPHVIEW)
   10.18  
   10.19    def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
   10.20      snapshot.select_markup(range, Some(active_include),
   10.21 @@ -426,6 +428,8 @@
   10.22                  (None, Some(bad_color))
   10.23                case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   10.24                  (None, Some(intensify_color))
   10.25 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.DIALOG_RESULT, _), _))) =>
   10.26 +                (None, Some(active_result_color))
   10.27                case (_, Text.Info(_, XML.Elem(Markup(name, _), _))) if active_include(name) =>
   10.28                  (None, Some(active_color))
   10.29              })