aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/session.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-04-07 13:58:16 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-04-07 15:34:26 +0200
commit4fdfc180bb2de6430537c7cff5d32b36c7bb8354 (patch)
tree9500ed679adb52d0b1d8c96b685e06020c57acc7 /ide/session.mli
parent61ee00dc214599ab6b17fac0586c746563eb565d (diff)
Allowing proof view to be detached in CoqIDE.
Diffstat (limited to 'ide/session.mli')
-rw-r--r--ide/session.mli6
1 files changed, 6 insertions, 0 deletions
diff --git a/ide/session.mli b/ide/session.mli
index 527e1d170..925b13567 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -16,6 +16,11 @@ class type ['a] page =
method on_update : callback:('a -> unit) -> unit
end
+class type control =
+ object
+ method detach : unit -> unit
+ end
+
type errpage = (int * string) list page
type jobpage = string Int.Map.t page
@@ -32,6 +37,7 @@ type session = {
tab_label : GMisc.label;
errpage : errpage;
jobpage : jobpage;
+ mutable control : control;
}
(** [create filename coqtop_args] *)