aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/session.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-03-12 11:30:15 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-03-12 11:30:15 +0100
commit1142dab2ee08b23cdf97cdf52d5dc7ecd7768967 (patch)
tree0deab0e9387ae32639ea08ef9703b220ef8d4ff0 /ide/session.mli
parentb2a6a5390436e6ba27d604d18e3b4c757875afd1 (diff)
CoqIDE: detachable message/error/jobs panes
Diffstat (limited to 'ide/session.mli')
-rw-r--r--ide/session.mli11
1 files changed, 4 insertions, 7 deletions
diff --git a/ide/session.mli b/ide/session.mli
index 737b6d10d..3ed1b1ee3 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -9,17 +9,14 @@
(** A session is a script buffer + proof + messages,
interacting with a coqtop, and a few other elements around *)
-class type errpage =
+class type ['a] page =
object
inherit GObj.widget
- method update : (int * string) list -> unit
+ method update : 'a -> unit
end
-class type jobpage =
- object
- inherit GObj.widget
- method update : string Int.Map.t -> unit
- end
+type errpage = (int * string) list page
+type jobpage = string Int.Map.t page
type session = {
buffer : GText.buffer;