aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/session.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-01-03 20:09:06 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-01-05 09:53:54 +0100
commitc72224832e2488b15f8f58d96554e4cf4337460d (patch)
treed7ba9651cd0e8fa745f0c4161cf6c7d72e719018 /ide/session.ml
parentc146a313b5eeee2bb567553810d57c6a8548bd9a (diff)
Implementing a segment-viewer in CoqIDE.
This allows a nifty display of the current state of the document through a dedicated progress bar. Also closes bug #3764.
Diffstat (limited to 'ide/session.ml')
-rw-r--r--ide/session.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/ide/session.ml b/ide/session.ml
index 4835307ec..ecf9a8f8b 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -33,6 +33,7 @@ type session = {
script : Wg_ScriptView.script_view;
proof : Wg_ProofView.proof_view;
messages : Wg_MessageView.message_view;
+ segment : Wg_Segment.segment;
fileops : FileOps.ops;
coqops : CoqOps.ops;
coqtop : Coq.coqtop;
@@ -368,12 +369,13 @@ let create file coqtop_args =
let script = create_script coqtop buffer in
let proof = create_proof () in
let messages = create_messages () in
+ let segment = new Wg_Segment.segment () in
let command = new Wg_Command.command_window basename coqtop in
let finder = new Wg_Find.finder basename (script :> GText.view) in
let fops = new FileOps.fileops (buffer :> GText.buffer) file reset in
let _ = fops#update_stats in
let cops =
- new CoqOps.coqops script proof messages coqtop (fun () -> fops#filename) in
+ new CoqOps.coqops script proof messages segment coqtop (fun () -> fops#filename) in
let errpage = create_errpage script in
let jobpage = create_jobpage coqtop cops in
let _ = set_buffer_handlers (buffer :> GText.buffer) script cops coqtop in
@@ -384,6 +386,7 @@ let create file coqtop_args =
script=script;
proof=proof;
messages=messages;
+ segment=segment;
fileops=fops;
coqops=cops;
coqtop=coqtop;
@@ -489,6 +492,7 @@ let build_layout (sn:session) =
end)
in
session_box#pack sn.finder#coerce;
+ session_box#pack sn.segment#coerce;
sn.command#pack_in (session_paned#pack2 ~shrink:false ~resize:false);
script_scroll#add sn.script#coerce;
proof_scroll#add sn.proof#coerce;