gmain.ml 24.3 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

20
let pname = "[Why Ide]"
MARCHE Claude's avatar
MARCHE Claude committed
21 22 23 24 25 26

let () = ignore (GtkMain.Main.init ())

open Format
open Why
open Whyconf
MARCHE Claude's avatar
MARCHE Claude committed
27
open Gconfig
MARCHE Claude's avatar
MARCHE Claude committed
28

MARCHE Claude's avatar
MARCHE Claude committed
29 30 31
(*****************************)
(* loading Why configuration *)
(*****************************)
MARCHE Claude's avatar
MARCHE Claude committed
32 33 34 35 36

let config = 
  try 
    Whyconf.read_config None
  with 
37
    | Not_found ->
MARCHE Claude's avatar
MARCHE Claude committed
38
        eprintf "%s no config file found.@." pname;
MARCHE Claude's avatar
MARCHE Claude committed
39
        exit 1
40 41
    | e ->
        eprintf "%a@." Exn_printer.exn_printer e;
MARCHE Claude's avatar
MARCHE Claude committed
42 43 44 45 46
        exit 1

let () = eprintf "%s Load path is: %a@." pname
  (Pp.print_list Pp.comma Pp.string) config.loadpath

47
(*
MARCHE Claude's avatar
MARCHE Claude committed
48 49 50 51
let timelimit = 
  match config.timelimit with
    | None -> 2
    | Some n -> n
52
*)
MARCHE Claude's avatar
MARCHE Claude committed
53 54


MARCHE Claude's avatar
MARCHE Claude committed
55 56 57 58 59 60
(********************************)
(* loading WhyIDE configuration *)
(********************************)

let gconfig = 
  eprintf "%s reading IDE config file@." pname;
MARCHE Claude's avatar
MARCHE Claude committed
61
  read_config ()
MARCHE Claude's avatar
MARCHE Claude committed
62 63 64 65

(***************************)
(* parsing comand_line *)
(***************************)
MARCHE Claude's avatar
MARCHE Claude committed
66 67 68 69

let spec = [
]

70
let usage_str = "whyide [options] <file>.why"
MARCHE Claude's avatar
MARCHE Claude committed
71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116
let file = ref None
let set_file f = match !file with
  | Some _ -> 
      raise (Arg.Bad "only one file")
  | None -> 
(*
      if not (Filename.check_suffix f ".why") then 
	raise (Arg.Bad ("don't know what to do with " ^ f));
*)
      if not (Sys.file_exists f) then begin
	Format.eprintf "%s %s: no such file@." pname f; 
        exit 1
      end;
      file := Some f

let () = Arg.parse spec set_file usage_str

let fname = match !file with
  | None -> 
      Arg.usage spec usage_str; 
      exit 1
  | Some f -> 
      f

let lang =
  let load_path = 
    List.fold_right Filename.concat 
      [Filename.dirname Sys.argv.(0); ".."; "share"] "lang" 
  in
  let languages_manager = 
    GSourceView2.source_language_manager ~default:true 
  in
  languages_manager#set_search_path 
    (load_path :: languages_manager#search_path);
  match languages_manager#language "why" with
    | None -> Format.eprintf "pas trouv@;"; None
    | Some _ as l -> l

let source_text = 
  let ic = open_in fname in
  let size = in_channel_length ic in
  let buf = String.create size in
  really_input ic buf 0 size;
  close_in ic;
  buf

117
let env = Why.Env.create_env (Why.Lexer.retrieve config.loadpath)
MARCHE Claude's avatar
MARCHE Claude committed
118 119 120 121 122 123 124 125 126 127 128 129 130 131


(***********************)
(* Parsing input file  *)
(***********************)

let theories : Theory.theory Theory.Mnm.t =
  try
    let cin = open_in fname in
    let m = Env.read_channel env fname cin in
    close_in cin;
    eprintf "Parsing/Typing Ok@.";
    m
  with e -> 
132
    eprintf "%a@." Exn_printer.exn_printer e;
MARCHE Claude's avatar
MARCHE Claude committed
133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195
    exit 1

(********************)
(* opening database *)
(********************)

(*
let () = Db.init_base (fname ^ ".db")
*)

let get_driver name = 
  let pi = Util.Mstr.find name config.provers in
  Why.Driver.load_driver env pi.Whyconf.driver

type prover_data =
    { prover : string (* Db.prover *);
      command : string;
      driver : Why.Driver.driver;
    }

let provers_data =
  printf "===============================@\nProvers: ";
  let l = 
    Util.Mstr.fold
    (fun id conf acc ->
       let name = conf.Whyconf.name in
       printf " %s, " name;
       { prover = (* Db.get_prover *) name;
         command = conf.Whyconf.command;
         driver = get_driver id; } :: acc
    ) config.provers []
  in
  printf "@\n===============================@.";
  l 

let find_prover s =
  match
    List.fold_left
      (fun acc p ->
         if (* Db.prover_name *) p.prover = s then Some p else acc)
      None provers_data
  with
    | None -> assert false
    | Some p -> p

let alt_ergo = find_prover "Alt-Ergo"
let simplify = find_prover "simplify"
let z3 = find_prover "Z3"


   
(*
let () = 
  printf "previously known goals:@\n";
  List.iter (fun s -> printf "%s@\n" (Db.goal_task_checksum s)) (Db.root_goals ());
  printf "@."
*)


(****************)
(* goals widget *)
(****************)

MARCHE Claude's avatar
MARCHE Claude committed
196

197 198 199 200 201 202 203 204 205 206 207 208 209
module Model = struct


  type proof_attempt =
      { prover : prover_data;
        status : Scheduler.proof_attempt_status;
        time : float;
        output : string;
      }

  type goal_parent =
    | Theory of theory
    | Transf of transf
MARCHE Claude's avatar
MARCHE Claude committed
210

211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236
  and goal =
      { parent : goal_parent;
        task: Task.task;
        goal_row : Gtk.tree_iter;
        mutable proved : bool;
        mutable external_proofs: proof_attempt list;
        mutable transformations : transf list;
      }

  and transf =
      { parent_goal : goal;
(*
        transf : Task.task Trans.trans;
*)
        transf_row : Gtk.tree_iter;
        mutable subgoals : goal list;
      }
        
  and theory =
      { theory : Theory.theory;
        theory_row : Gtk.tree_iter;
        mutable goals : goal list;
        mutable verified : bool;
      }

  let all : theory list ref = ref [] 
MARCHE Claude's avatar
MARCHE Claude committed
237

MARCHE Claude's avatar
MARCHE Claude committed
238 239
  let toggle_hide_proved_goals = ref false

MARCHE Claude's avatar
MARCHE Claude committed
240 241
  let cols = new GTree.column_list
  let name_column = cols#add Gobject.Data.string
MARCHE Claude's avatar
MARCHE Claude committed
242
  let icon_column = cols#add Gobject.Data.gobject
MARCHE Claude's avatar
MARCHE Claude committed
243 244 245
  let id_column = cols#add Gobject.Data.caml
  let status_column = cols#add Gobject.Data.gobject
  let time_column = cols#add Gobject.Data.string
MARCHE Claude's avatar
MARCHE Claude committed
246
  let visible_column = cols#add Gobject.Data.boolean
MARCHE Claude's avatar
MARCHE Claude committed
247 248 249
(*
  let bg_column = cols#add (Gobject.Data.unsafe_boxed (Gobject.Type.from_name "GdkColor"))
*)
MARCHE Claude's avatar
MARCHE Claude committed
250

MARCHE Claude's avatar
MARCHE Claude committed
251
  let name_renderer = GTree.cell_renderer_text [`XALIGN 0.] 
MARCHE Claude's avatar
MARCHE Claude committed
252 253
  let renderer = GTree.cell_renderer_text [`XALIGN 0.] 
  let image_renderer = GTree.cell_renderer_pixbuf [ ] 
MARCHE Claude's avatar
MARCHE Claude committed
254
  let icon_renderer = GTree.cell_renderer_pixbuf [ ]
MARCHE Claude's avatar
MARCHE Claude committed
255 256

  let view_name_column = 
MARCHE Claude's avatar
MARCHE Claude committed
257
    GTree.view_column ~title:"Theories/Goals" ()
MARCHE Claude's avatar
MARCHE Claude committed
258 259

  let () = 
MARCHE Claude's avatar
MARCHE Claude committed
260 261 262 263
    view_name_column#pack icon_renderer ;
    view_name_column#add_attribute icon_renderer "pixbuf" icon_column ;
    view_name_column#pack name_renderer;
    view_name_column#add_attribute name_renderer "text" name_column;
MARCHE Claude's avatar
MARCHE Claude committed
264
    view_name_column#set_resizable true;
MARCHE Claude's avatar
MARCHE Claude committed
265 266 267 268 269
    view_name_column#set_max_width 400;
(*
    view_name_column#add_attribute name_renderer "background-gdk" bg_column
*)
    ()
MARCHE Claude's avatar
MARCHE Claude committed
270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288

  let view_status_column = 
    GTree.view_column ~title:"Status" 
      ~renderer:(image_renderer, ["pixbuf", status_column]) 
      ()

  let view_time_column = 
    GTree.view_column ~title:"Time" 
      ~renderer:(renderer, ["text", time_column]) ()

  let () = 
    view_status_column#set_resizable false;
    view_status_column#set_visible true;
    view_time_column#set_resizable false;
    view_time_column#set_visible true


  let create ~packing () =
    let model = GTree.tree_store cols in
MARCHE Claude's avatar
MARCHE Claude committed
289 290 291
    let model_filter = GTree.model_filter model in
    model_filter#set_visible_column visible_column;
    let view = GTree.view ~model:model_filter ~packing () in
MARCHE Claude's avatar
MARCHE Claude committed
292 293 294 295 296
    let _ = view#selection#set_mode `SINGLE in
    let _ = view#set_rules_hint true in
    ignore (view#append_column view_name_column);
    ignore (view#append_column view_status_column);
    ignore (view#append_column view_time_column);
297
    model,model_filter,view
MARCHE Claude's avatar
MARCHE Claude committed
298 299 300 301 302 303 304

  let clear model = model#clear ()

  let goal_table = Ident.Hid.create 17

  let get_goal id = fst (Ident.Hid.find goal_table id)

305 306 307 308 309 310
end

(***************)
(* Main window *)
(***************)

MARCHE Claude's avatar
MARCHE Claude committed
311 312
let exit_function () =
  eprintf "%s saving IDE config file@." pname;
MARCHE Claude's avatar
MARCHE Claude committed
313 314
  save_config gconfig;
  GMain.quit ()
MARCHE Claude's avatar
MARCHE Claude committed
315

316 317
let w = GWindow.window 
  ~allow_grow:true ~allow_shrink:true
MARCHE Claude's avatar
MARCHE Claude committed
318 319
  ~width:gconfig.window_width 
  ~height:gconfig.window_height 
320 321
  ~title:"why-ide" ()

MARCHE Claude's avatar
MARCHE Claude committed
322 323 324 325 326 327
let (_ : GtkSignal.id) = w#connect#destroy ~callback:exit_function 

let (_ : GtkSignal.id) = 
  w#misc#connect#size_allocate 
    ~callback:
    (fun {Gtk.width=w;Gtk.height=h} -> 
MARCHE Claude's avatar
MARCHE Claude committed
328 329
       gconfig.window_height <- h;
       gconfig.window_width <- w)
330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347

let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () 

(* Menu *)

let menubar = GMenu.menu_bar ~packing:vbox#pack () 

let factory = new GMenu.factory menubar 

let accel_group = factory#accel_group 

(* horizontal paned *)

let hp = GPack.paned `HORIZONTAL  ~border_width:3 ~packing:vbox#add () 

(* tree view *)
let scrollview = 
  GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC 
MARCHE Claude's avatar
MARCHE Claude committed
348
    ~width:gconfig.tree_width 
MARCHE Claude's avatar
MARCHE Claude committed
349
    ~packing:hp#add () 
350 351

let () = scrollview#set_shadow_type `ETCHED_OUT 
352 353 354 355
let (_ : GtkSignal.id) = 
  scrollview#misc#connect#size_allocate 
    ~callback:
    (fun {Gtk.width=w;Gtk.height=_h} -> 
MARCHE Claude's avatar
MARCHE Claude committed
356
       gconfig.tree_width <- w)
357

358
let goals_model,filter_model,goals_view = Model.create ~packing:scrollview#add () 
359 360 361 362 363 364 365 366

module Helpers = struct

  open Model

  let set_theory_proved t =
    t.verified <- true;
    let row = t.theory_row in
MARCHE Claude's avatar
MARCHE Claude committed
367
    goals_view#collapse_row (goals_model#get_path row);
368
    goals_model#set ~row ~column:Model.status_column !image_yes;
MARCHE Claude's avatar
MARCHE Claude committed
369 370 371
    if !Model.toggle_hide_proved_goals then
      goals_model#set ~row ~column:Model.visible_column false
      
372 373 374 375 376 377
    
  let rec set_proved g =
    let row = g.goal_row in
    g.proved <- true;
    goals_view#collapse_row (goals_model#get_path row);
    goals_model#set ~row ~column:Model.status_column !image_yes;
MARCHE Claude's avatar
MARCHE Claude committed
378 379
    if !Model.toggle_hide_proved_goals then
      goals_model#set ~row ~column:Model.visible_column false;
380 381 382 383 384 385 386 387 388 389 390 391
    match g.parent with
      | Theory t ->
          if List.for_all (fun g -> g.proved) t.goals then
            set_theory_proved t
      | Transf t ->
          if List.for_all (fun g -> g.proved) t.subgoals then
            begin
              set_proved t.parent_goal;
            end
              

  let add_theory th =
MARCHE Claude's avatar
MARCHE Claude committed
392
    let tname = th.Theory.th_name.Ident.id_string in
393 394 395 396
    let parent = goals_model#append () in
    let mth = { theory = th; 
                theory_row = parent; 
                goals = [] ; 
397
                verified = false } 
398 399 400 401 402 403
    in
    all := !all @ [mth];
    goals_model#set ~row:parent ~column:name_column tname;
    goals_model#set ~row:parent ~column:icon_column !image_directory;
    goals_model#set ~row:parent ~column:id_column th.Theory.th_name;
    goals_model#set ~row:parent ~column:visible_column true;
MARCHE Claude's avatar
MARCHE Claude committed
404
    let tasks = Task.split_theory th None None in
405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427
    let goals =
      List.fold_left
        (fun acc t ->
           let id = (Task.task_goal t).Decl.pr_name in
           let name = id.Ident.id_string in
           let row = goals_model#append ~parent () in
           Ident.Hid.add goal_table id (t,row);
	   goals_model#set ~row ~column:name_column name;
           goals_model#set ~row ~column:icon_column !image_file;
	   goals_model#set ~row ~column:id_column id;
           goals_model#set ~row ~column:visible_column true;
           let goal = { parent = Theory mth; 
                        task = t ; 
                        goal_row = row;
                        external_proofs = [];
                        transformations = [];
                        proved = false;
                      }
           in
           goal :: acc
        )
        []
        (List.rev tasks)
MARCHE Claude's avatar
MARCHE Claude committed
428
    in
429 430 431
    mth.goals <- List.rev goals;
    if goals = [] then set_theory_proved mth
    
MARCHE Claude's avatar
MARCHE Claude committed
432 433 434

end

435 436 437 438
let () = 
  Theory.Mnm.iter (fun _ th -> Helpers.add_theory th) theories


MARCHE Claude's avatar
MARCHE Claude committed
439 440 441 442 443 444 445 446 447

let image_of_result = function
  | Scheduler.Scheduled -> !image_scheduled
  | Scheduler.Running -> !image_running
  | Scheduler.Success -> !image_valid
  | Scheduler.Timeout -> !image_timeout
  | Scheduler.Unknown -> !image_unknown
  | Scheduler.HighFailure -> !image_failure

448 449 450
let () = 
  begin
    Scheduler.async := GtkThread.async;
451
(*
452 453 454 455
    match config.running_provers_max with
      | None -> ()
      | Some n -> 
          if n >= 1 then Scheduler.maximum_running_proofs := n
456 457
*)
    Scheduler.maximum_running_proofs := gconfig.max_running_processes
458
  end 
MARCHE Claude's avatar
MARCHE Claude committed
459

MARCHE Claude's avatar
MARCHE Claude committed
460 461 462
(*****************************************************)
(* method: run a given prover on each unproved goals *)
(*****************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
463

464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481
let rec prover_on_goal p g =
  let row = g.Model.goal_row in
  let name = p.prover in
  let prover_row = goals_model#append ~parent:row () in
  goals_model#set ~row:prover_row ~column:Model.icon_column !image_prover;
  goals_model#set ~row:prover_row ~column:Model.name_column ("prover: " ^name);
  goals_model#set ~row:prover_row ~column:Model.visible_column true;
  goals_view#expand_row (goals_model#get_path row);
  let callback result time =
    goals_model#set ~row:prover_row ~column:Model.status_column 
      (image_of_result result);
    let t = if time > 0.0 then Format.sprintf "%.2f" time else "" in
    goals_model#set ~row:prover_row ~column:Model.time_column t;
    if result = Scheduler.Success then
      Helpers.set_proved g
  in
  callback Scheduler.Scheduled 0.0;
  Scheduler.schedule_proof_attempt
482
    ~debug:false ~timelimit:gconfig.time_limit ~memlimit:0 
483 484 485 486 487 488 489 490 491 492 493 494 495
    ~prover:p.prover ~command:p.command ~driver:p.driver 
    ~callback
    g.Model.task;
  List.iter
    (fun t -> List.iter (prover_on_goal p) t.Model.subgoals)
    g.Model.transformations
    
let prover_on_unproved_goals p () =
  List.iter
    (fun th ->
       List.iter
         (fun g -> if not g.Model.proved then prover_on_goal p g)
         th.Model.goals;
MARCHE Claude's avatar
MARCHE Claude committed
496
    )
497
    !Model.all
MARCHE Claude's avatar
MARCHE Claude committed
498

MARCHE Claude's avatar
MARCHE Claude committed
499 500 501 502
(*****************************************************)
(* method: split all unproved goals *)
(*****************************************************)

503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520
let split_transformation = Trans.lookup_transform_l "split_goal" env

let split_unproved_goals () =
  List.iter
    (fun th ->
       List.iter
         (fun g ->
            if not g.Model.proved then         
              let row = g.Model.goal_row in
              let goal_name = goals_model#get ~row ~column:Model.name_column in
              let callback subgoals =
                if List.length subgoals >= 2 then
                  let split_row = goals_model#append ~parent:row () in
                  goals_model#set ~row:split_row ~column:Model.visible_column true;
                  goals_model#set ~row:split_row ~column:Model.name_column "split";
                  goals_model#set ~row:split_row ~column:Model.icon_column !image_transf;
                  let tr =
                    { Model.parent_goal = g;
MARCHE Claude's avatar
MARCHE Claude committed
521
(*
522
                      Model.transf = split_transformation;
MARCHE Claude's avatar
MARCHE Claude committed
523
*)
524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556
                      Model.transf_row = split_row;
                      subgoals = [];
                    }
                  in
                  g.Model.transformations <- tr :: g.Model.transformations;
                  let goals,_ = List.fold_left
                    (fun (acc,count) subtask ->
                       let id = (Task.task_goal subtask).Decl.pr_name in
                       let subtask_row = goals_model#append ~parent:split_row () in
                       Ident.Hid.add Model.goal_table id (subtask,subtask_row);
	               goals_model#set ~row:subtask_row ~column:Model.id_column id;
                       goals_model#set ~row:subtask_row ~column:Model.visible_column true;
                       goals_model#set ~row:subtask_row ~column:Model.name_column 
                         (goal_name ^ "." ^ (string_of_int count));
                       goals_model#set ~row:subtask_row ~column:Model.icon_column !image_file;
                       let goal = { Model.parent = Model.Transf tr; 
                                    Model.task = subtask ; 
                                    Model.goal_row = subtask_row;
                                    Model.external_proofs = [];
                                    Model.transformations = [];
                                    Model.proved = false;
                                  }
                       in
                       (goal :: acc, count+1))
                    ([],1) subgoals 
                  in
                  tr.Model.subgoals <- List.rev goals;
                  goals_view#expand_row (goals_model#get_path row)           
              in
              
              Scheduler.apply_transformation ~callback split_transformation g.Model.task
         )
         th.Model.goals
MARCHE Claude's avatar
MARCHE Claude committed
557
    )
558 559 560 561 562 563 564 565 566
    !Model.all


(*************)
(* File menu *)
(*************)

let file_menu = factory#add_submenu "_File" 
let file_factory = new GMenu.factory file_menu ~accel_group 
MARCHE Claude's avatar
MARCHE Claude committed
567 568

let (_ : GMenu.image_menu_item) = 
569 570 571 572 573
  file_factory#add_image_item ~label:"_Preferences" ~callback:
    (fun () ->
       Gconfig.preferences gconfig;
       Scheduler.maximum_running_proofs := gconfig.max_running_processes)
    () 
MARCHE Claude's avatar
MARCHE Claude committed
574

575 576
let (_ : GMenu.image_menu_item) = 
  file_factory#add_image_item ~key:GdkKeysyms._Q ~label:"_Quit" 
MARCHE Claude's avatar
MARCHE Claude committed
577
    ~callback:exit_function () 
578 579 580 581 582 583 584 585 586 587 588

(*************)
(* View menu *)
(*************)

let view_menu = factory#add_submenu "_View" 
let view_factory = new GMenu.factory view_menu ~accel_group 
let (_ : GMenu.image_menu_item) = 
  view_factory#add_image_item ~key:GdkKeysyms._E 
    ~label:"Expand all" ~callback:(fun () -> goals_view#expand_all ()) () 

MARCHE Claude's avatar
MARCHE Claude committed
589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617
let rec collapse_proved_goal g =
  if g.Model.proved then
    begin
      let row = g.Model.goal_row in
      goals_view#collapse_row (goals_model#get_path row);
    end
  else
    List.iter 
      (fun t -> List.iter collapse_proved_goal t.Model.subgoals)
      g.Model.transformations

let collapse_verified_theories () =
  List.iter
    (fun th ->
       if th.Model.verified then
         begin
           let row = th.Model.theory_row in
           goals_view#collapse_row (goals_model#get_path row);
         end
       else
         List.iter collapse_proved_goal th.Model.goals)
    !Model.all

let (_ : GMenu.image_menu_item) = 
  view_factory#add_image_item ~key:GdkKeysyms._C
    ~label:"Collapse proved goals" 
    ~callback:collapse_verified_theories 
    () 
  
618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642
let rec hide_proved_goal g =
  if g.Model.proved then
    begin
      let row = g.Model.goal_row in
      goals_view#collapse_row (goals_model#get_path row);
      goals_model#set ~row ~column:Model.visible_column false
    end
  else
    List.iter 
      (fun t -> List.iter hide_proved_goal t.Model.subgoals)
      g.Model.transformations

let hide_verified_theories () =
  List.iter
    (fun th ->
       if th.Model.verified then
         begin
           let row = th.Model.theory_row in
           goals_view#collapse_row (goals_model#get_path row);
           goals_model#set ~row ~column:Model.visible_column false
         end
       else
         List.iter hide_proved_goal th.Model.goals)
    !Model.all
    
MARCHE Claude's avatar
MARCHE Claude committed
643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667

let rec show_all_goals g =
  let row = g.Model.goal_row in
  goals_model#set ~row ~column:Model.visible_column true;
  if g.Model.proved then
    goals_view#collapse_row (goals_model#get_path row)
  else
    goals_view#expand_row (goals_model#get_path row);
  List.iter 
    (fun t -> List.iter show_all_goals t.Model.subgoals)
    g.Model.transformations

let show_all_theories () = 
  List.iter
    (fun th ->
       let row = th.Model.theory_row in
       goals_model#set ~row ~column:Model.visible_column true;
       if th.Model.verified then
         goals_view#collapse_row (goals_model#get_path row)
       else
         goals_view#expand_row (goals_model#get_path row);
       List.iter show_all_goals th.Model.goals)
    !Model.all
    

668 669

let (_ : GMenu.check_menu_item) = view_factory#add_check_item 
MARCHE Claude's avatar
MARCHE Claude committed
670 671 672 673
  ~callback:(fun b ->
               Model.toggle_hide_proved_goals := b;
               if b then hide_verified_theories ()
               else show_all_theories ())
674 675 676
  "Hide proved goals"
  

677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722
(**************)
(* Tools menu *)
(**************)

let tools_menu = factory#add_submenu "_Tools" 
let tools_factory = new GMenu.factory tools_menu ~accel_group 

let (_ : GMenu.image_menu_item) = 
  tools_factory#add_image_item ~key:GdkKeysyms._S
    ~label:"Simplify on unproved goals" 
    ~callback:(fun () -> prover_on_unproved_goals simplify ()) 
    () 

let (_ : GMenu.image_menu_item) = 
  tools_factory#add_image_item ~key:GdkKeysyms._A 
    ~label:"Alt-Ergo on unproved goals" 
    ~callback:(fun () -> prover_on_unproved_goals alt_ergo ()) 
    () 

let (_ : GMenu.image_menu_item) = 
  tools_factory#add_image_item ~key:GdkKeysyms._Z 
    ~label:"Z3 on unproved goals" 
    ~callback:(fun () -> prover_on_unproved_goals z3 ()) 
    () 
  
let (_ : GMenu.image_menu_item) = 
  tools_factory#add_image_item 
    ~label:"Split unproved goals" 
    ~callback:split_unproved_goals
    () 

(*************)
(* Help menu *)
(*************)

let info_window t s () =
  let d = GWindow.message_dialog
    ~message:s
    ~message_type:`INFO
    ~buttons:GWindow.Buttons.close
    ~title:t
    ~show:true () 
  in
  let (_ : GtkSignal.id) =
    d#connect#response 
      ~callback:(function `CLOSE | `DELETE_EVENT -> d#destroy ())
MARCHE Claude's avatar
MARCHE Claude committed
723
  in
724
  ()
MARCHE Claude's avatar
MARCHE Claude committed
725

726 727 728 729 730 731
let help_menu = factory#add_submenu "_Help" 
let help_factory = new GMenu.factory help_menu ~accel_group 

let (_ : GMenu.image_menu_item) = 
  help_factory#add_image_item 
    ~label:"Legend" 
MARCHE Claude's avatar
MARCHE Claude committed
732
    ~callback:show_legend_window
733 734 735 736 737
    () 

let (_ : GMenu.image_menu_item) = 
  help_factory#add_image_item 
    ~label:"About" 
MARCHE Claude's avatar
MARCHE Claude committed
738
    ~callback:show_about_window
739
    () 
MARCHE Claude's avatar
MARCHE Claude committed
740 741


742 743 744
(******************************)
(* vertical paned on the right*)
(******************************)
MARCHE Claude's avatar
MARCHE Claude committed
745

746
let vp = GPack.paned `VERTICAL  ~border_width:3 ~packing:hp#add () 
MARCHE Claude's avatar
MARCHE Claude committed
747

748 749 750
(******************)
(* goal text view *)
(******************)
MARCHE Claude's avatar
MARCHE Claude committed
751

752 753 754 755
let scrolled_task_view = GBin.scrolled_window
  ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
  ~packing:vp#add ()
  
756 757 758 759
let (_ : GtkSignal.id) = 
  scrolled_task_view#misc#connect#size_allocate 
    ~callback:
    (fun {Gtk.width=_w;Gtk.height=h} -> 
MARCHE Claude's avatar
MARCHE Claude committed
760
       gconfig.task_height <- h)
761

762 763 764 765
let task_view =
  GSourceView2.source_view
    ~editable:false
    ~show_line_numbers:true
766
    ~packing:scrolled_task_view#add 
MARCHE Claude's avatar
MARCHE Claude committed
767
    ~height:gconfig.task_height
768
    ()
MARCHE Claude's avatar
MARCHE Claude committed
769

770 771
let () = task_view#source_buffer#set_language lang
let () = task_view#set_highlight_current_line true
MARCHE Claude's avatar
MARCHE Claude committed
772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802

let move_to_line (v : GText.view) line = 
  if line <= v#buffer#line_count && line <> 0 then begin
    let it = v#buffer#get_iter (`LINE line) in 
    let mark = `MARK (v#buffer#create_mark it) in
    v#scroll_to_mark ~use_align:true ~yalign:0.5 mark
  end

(* to be run when a row in the tree view is selected *)
let select_goals selected_rows = 
  List.iter
    (fun p ->
       let row = filter_model#get_iter p in
       let id = filter_model#get ~row ~column:Model.id_column in
       Format.eprintf "You clicked on %s@." id.Ident.id_string;
       try
         let g = Model.get_goal id in
         let task_text = Pp.string_of Pretty.print_task g in
         task_view#source_buffer#set_text task_text;
         task_view#scroll_to_mark `INSERT
       with Not_found -> ()

(*
       match origin with
         | Ident.User (_loc,_) -> ()
             move_to_line source_view#as_view loc.Lexing.pos_lnum
         | _ -> ()
*)
    )
    selected_rows

803 804 805 806
  
(***************)
(* source view *)
(***************)
MARCHE Claude's avatar
MARCHE Claude committed
807

808 809 810 811
let scrolled_source_view = GBin.scrolled_window
  ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
  ~packing:vp#add 
  ()
MARCHE Claude's avatar
MARCHE Claude committed
812
  
813 814 815 816 817 818 819
let source_view =
  GSourceView2.source_view
    ~auto_indent:true
    ~insert_spaces_instead_of_tabs:true ~tab_width:2
    ~show_line_numbers:true
    ~right_margin_position:80 ~show_right_margin:true
    (* ~smart_home_end:true *)
820
    ~packing:scrolled_source_view#add 
821 822
    ()

MARCHE Claude's avatar
MARCHE Claude committed
823 824 825
(*
  source_view#misc#modify_font_by_name font_name;
*)
826 827 828 829 830 831 832 833 834 835 836 837 838
let () = source_view#source_buffer#set_language lang
let () = source_view#set_highlight_current_line true
let () = source_view#source_buffer#set_text source_text

(***************)
(* Bind events *)
(***************)

(* row selection on tree view on the left *) 
let (_ : GtkSignal.id) =
  goals_view#selection#connect#after#changed ~callback:
    begin fun () ->
      let list = goals_view#selection#get_selected_rows in
MARCHE Claude's avatar
MARCHE Claude committed
839
      select_goals list
840 841 842 843 844
    end

let () = w#add_accel_group accel_group
let () = w#show () 
let () = GtkThread.main ()
MARCHE Claude's avatar
MARCHE Claude committed
845 846 847

(*
Local Variables: 
848
compile-command: "unset LANG; make -C ../.. bin/whyide.opt"
MARCHE Claude's avatar
MARCHE Claude committed
849 850
End: 
*)