gmain.ml 73.2 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13 14


open Format

15
open Why3
16 17
open Whyconf
open Gconfig
18
open Stdlib
François Bobot's avatar
François Bobot committed
19
open Debug
20

21
module C = Whyconf
François Bobot's avatar
François Bobot committed
22

23 24 25 26 27 28 29 30 31 32 33
external reset_gc : unit -> unit = "ml_reset_gc"

(* Setting a Gc.alarm is pointless; the function has to be called manually
   before each lablgtk operation. Indeed, each major slice resets
   caml_extra_heap_resources to zero, but alarms are executed only at
   finalization time, that is, after a full collection completes. Note that
   manual calls can fail to prevent extraneous collections too, if a major
   slice happens right in the middle of a sequence of lablgtk operations due
   to memory starvation. Hopefully, it seldom happens. *)
let () = reset_gc ()

34
let debug = Debug.lookup_flag "ide_info"
35

36 37 38
let debug_show_text_cntexmp = Debug.register_info_flag "show_text_cntexmp"
  ~desc:"Print@ textual@ counterexample@ before@ printing@ counterexample@ interleaved@ with@ cource@ code."

39 40 41 42
(************************)
(* parsing command line *)
(************************)

43
let files = Queue.create ()
44
let opt_parser = ref None
45 46

let spec = Arg.align [
47
  "-F", Arg.String (fun s -> opt_parser := Some s),
48
      "<format> select input format (default: \"why\")";
49 50
  "--format", Arg.String (fun s -> opt_parser := Some s),
      " same as -F";
51
(*
52
  "-f",
53
   Arg.String (fun s -> input_files := s :: !input_files),
54
   "<file> add file to the project (ignored if it is already there)";
55
*)
56
  Termcode.arg_extra_expl_prefix
57 58 59
]

let usage_str = sprintf
60
  "Usage: %s [options] [<file.why>|<project directory>]..."
61 62
  (Filename.basename Sys.argv.(0))

63 64 65 66 67 68
let gconfig = try
  let config, base_config, env =
    Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str in
  if Queue.is_empty files then Whyconf.Args.exit_with_usage spec usage_str;
  Gconfig.load_config config base_config env;
  Gconfig.config ()
69

70 71 72
  with e when not (Debug.test_flag Debug.stack_trace) ->
    eprintf "%a@." Exn_printer.exn_printer e;
    exit 1
73

74
let () =
MARCHE Claude's avatar
MARCHE Claude committed
75
  Debug.dprintf debug "[GUI] Init the GTK interface...@?";
76 77 78 79
  ignore (GtkMain.Main.init ());
  Debug.dprintf debug " done.@.";
  Gconfig.init ()

80
let (why_lang, any_lang) =
81
  let main = Gconfig.get_main () in
82 83 84 85 86 87
  let load_path = Filename.concat (datadir main) "lang" in
  let languages_manager =
    GSourceView2.source_language_manager ~default:true
  in
  languages_manager#set_search_path
    (load_path :: languages_manager#search_path);
88
  let why_lang =
89
    match languages_manager#language "why3" with
90
    | None ->
91
        eprintf "language file for 'why3' not found in directory %s@."
92 93
          load_path;
        exit 1
94 95 96 97 98 99
    | Some _ as l -> l in
  let any_lang filename =
    match languages_manager#guess_language ~filename () with
    | None -> why_lang
    | Some _ as l -> l in
  (why_lang, any_lang)
100

101
(* Borrowed from Frama-C src/gui/source_manager.ml:
102 103 104 105 106 107 108 109 110 111 112 113 114
Try to convert a source file either as UTF-8 or as locale. *)
let try_convert s =
  try
    if Glib.Utf8.validate s then s else Glib.Convert.locale_to_utf8 s
  with Glib.Convert.Error _ ->
    try
      Glib.Convert.convert_with_fallback
        ~fallback:"#neither UTF-8 nor locale nor ISO-8859-15#"
        ~to_codeset:"UTF-8"
        ~from_codeset:"ISO_8859-15"
        s
    with Glib.Convert.Error _ as e -> Printexc.to_string e

115 116 117 118 119 120 121 122
(***************)
(* Main window *)
(***************)

let w = GWindow.window
  ~allow_grow:true ~allow_shrink:true
  ~width:gconfig.window_width
  ~height:gconfig.window_height
MARCHE Claude's avatar
MARCHE Claude committed
123
  ~title:"Why3 Interactive Proof Session" ()
124

MARCHE Claude's avatar
MARCHE Claude committed
125 126 127
let () =
  w#set_icon (Some !Gconfig.why_icon)

128 129 130 131 132 133 134 135 136 137 138
let (_ : GtkSignal.id) =
  w#misc#connect#size_allocate
    ~callback:
    (fun {Gtk.width=w;Gtk.height=h} ->
       gconfig.window_height <- h;
       gconfig.window_width <- w)

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

(* Menu *)

139 140 141
let menubar = GMenu.menu_bar
  ~packing:(vbox#pack ?from:None ?expand:None ?fill:None ?padding:None)
  ()
142 143 144 145 146

let factory = new GMenu.factory menubar

let accel_group = factory#accel_group

MARCHE Claude's avatar
MARCHE Claude committed
147 148 149 150 151
let hb = GPack.hbox ~packing:vbox#add ()

let left_scrollview =
  try
    GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC
152
      ~packing:(hb#pack ~expand:false ?from:None ?fill:None ?padding:None) ()
MARCHE Claude's avatar
MARCHE Claude committed
153 154 155
  with Gtk.Error _ -> assert false

let () = left_scrollview#set_shadow_type `OUT
156 157 158

let tools_window_vbox =
  try
MARCHE Claude's avatar
MARCHE Claude committed
159
    GPack.vbox ~packing:left_scrollview#add_with_viewport ()
160 161
  with Gtk.Error _ -> assert false

162 163 164
let tools_window_vbox_pack =
  tools_window_vbox#pack ~expand:false ?from:None ?fill:None ?padding:None

165
let context_frame =
MARCHE Claude's avatar
MARCHE Claude committed
166
  GBin.frame ~label:"Context" ~shadow_type:`ETCHED_OUT
167
    ~packing:tools_window_vbox_pack ()
168 169 170 171 172 173 174 175 176 177 178

let context_box =
  GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
    ~packing:context_frame#add ()

let context_unproved_goals_only = ref true

let () =
  let b1 = GButton.radio_button
    ~packing:context_box#add ~label:"Unproved goals" ()
  in
François Bobot's avatar
François Bobot committed
179 180
  b1#misc#set_tooltip_markup
    "When selected, tools below are applied only to <b>unproved</b> goals";
181 182 183 184 185 186 187
  let (_ : GtkSignal.id) =
    b1#connect#clicked
      ~callback:(fun () -> context_unproved_goals_only := true)
  in
  let b2 = GButton.radio_button
    ~group:b1#group ~packing:context_box#add ~label:"All goals" ()
  in
François Bobot's avatar
François Bobot committed
188 189
  b2#misc#set_tooltip_markup
    "When selected, tools below are applied to all goals";
190 191 192 193 194 195
  let (_ : GtkSignal.id) =
    b2#connect#clicked
      ~callback:(fun () -> context_unproved_goals_only := false)
  in ()


196 197
let strategies_frame =
  GBin.frame ~label:"Strategies" ~shadow_type:`ETCHED_OUT
198
    ~packing:tools_window_vbox_pack ()
199 200 201 202 203

let strategies_box =
  GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
  ~packing:strategies_frame#add ()

204
let provers_frame =
MARCHE Claude's avatar
MARCHE Claude committed
205
  GBin.frame ~label:"Provers" ~shadow_type:`ETCHED_OUT
206
    ~packing:tools_window_vbox_pack ()
207

MARCHE Claude's avatar
MARCHE Claude committed
208

209 210 211 212 213 214 215
let provers_box =
  GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
  ~packing:provers_frame#add ()

let () = provers_frame#set_resize_mode `PARENT

let tools_frame =
MARCHE Claude's avatar
MARCHE Claude committed
216
  GBin.frame ~label:"Tools" ~shadow_type:`ETCHED_OUT
217
    ~packing:tools_window_vbox_pack ()
218 219 220 221 222

let tools_box =
  GPack.button_box `VERTICAL ~border_width:5 ~spacing:5
  ~packing:tools_frame#add ()

223
let monitor_frame =
MARCHE Claude's avatar
MARCHE Claude committed
224
  GBin.frame ~label:"Proof monitoring" ~shadow_type:`ETCHED_OUT
225
    ~packing:tools_window_vbox_pack ()
226 227 228 229 230 231 232 233 234 235 236 237 238 239

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

let monitor_waiting =
  GMisc.label ~text:"  Waiting: 0" ~packing:monitor_box#add ()

let monitor_scheduled =
  GMisc.label ~text:"Scheduled: 0" ~packing:monitor_box#add ()

let monitor_running =
  GMisc.label ~text:"  Running: 0" ~packing:monitor_box#add ()


240 241 242 243 244 245 246 247 248 249

(* horizontal paned *)

let hp = GPack.paned `HORIZONTAL ~packing:hb#add ()


(* tree view *)
let scrollview =
  try
    GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
MARCHE Claude's avatar
MARCHE Claude committed
250
      ~width:gconfig.tree_width ~shadow_type:`ETCHED_OUT
251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271
      ~packing:hp#add ()
  with Gtk.Error _ -> assert false

let (_ : GtkSignal.id) =
  scrollview#misc#connect#size_allocate
    ~callback:
    (fun {Gtk.width=w;Gtk.height=_h} ->
       gconfig.tree_width <- w)




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

let cols = new GTree.column_list
let name_column = cols#add Gobject.Data.string
let icon_column = cols#add Gobject.Data.gobject
let status_column = cols#add Gobject.Data.gobject
let time_column = cols#add Gobject.Data.string
272
let index_column = cols#add Gobject.Data.int
273

274 275 276 277
let name_renderer = GTree.cell_renderer_text [`XALIGN 0.]
let renderer = GTree.cell_renderer_text [`XALIGN 0.]
let image_renderer = GTree.cell_renderer_pixbuf [ ]
let icon_renderer = GTree.cell_renderer_pixbuf [ ]
278

279 280
let view_name_column =
  GTree.view_column ~title:"Theories/Goals" ()
281

282 283 284 285 286 287
let () =
  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;
  view_name_column#set_resizable true;
288 289 290 291
  view_name_column#set_max_width 800;
(*
  view_name_column#set_alignment 1.0;
*)
292
  ()
293

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

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

303 304 305 306 307
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
308

309
let goals_model,goals_view =
MARCHE Claude's avatar
MARCHE Claude committed
310
  Debug.dprintf debug "[GUI] Creating tree model...@?";
311 312
  let model = GTree.tree_store cols in
  let view = GTree.view ~model ~packing:scrollview#add () in
313
  let () = view#selection#set_mode (* `SINGLE *) `MULTIPLE in
314 315 316 317
  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);
318
  Debug.dprintf debug " done@.";
319
  model,view
320

321 322

(******************************)
323
(*    notebook on the right   *)
324 325
(******************************)

326
let notebook = GPack.notebook ~packing:hp#add ()
327

328 329 330 331
let source_page,source_tab =
  let label = GMisc.label ~text:"Source code" () in
  0, GPack.vbox ~homogeneous:false ~packing:
    (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
332

333
let task_page,task_tab =
334
  let label = GMisc.label ~text:"Task" () in
335 336 337
  1, GPack.vbox ~homogeneous:false ~packing:
    (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()

338 339 340 341 342 343 344 345 346 347
let edited_page,edited_tab =
  let label = GMisc.label ~text:"Edited proof" () in
  2, GPack.vbox ~homogeneous:false ~packing:
    (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()

let output_page,output_tab =
  let label = GMisc.label ~text:"Prover Output" () in
  3, GPack.vbox ~homogeneous:false ~packing:
    (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()

348 349
let counterexample_page,counterexample_tab =
  let label = GMisc.label ~text:"Counter-example" () in
350
  4, GPack.vbox ~homogeneous:false ~packing:
351 352
    (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()

353 354 355
let (_ : GPack.box) =
  GPack.hbox ~packing:(source_tab#pack ~expand:false ?from:None ?fill:None
                         ?padding:None) ()
356

357 358 359 360 361 362 363 364 365
let () =
  notebook#goto_page gconfig.current_tab;
  let page_selected n = gconfig.current_tab <- n in
  let (_ : GtkSignal.id) =
    notebook#connect#switch_page ~callback:page_selected
  in ()



366
(******************)
367
(* views          *)
368 369
(******************)

370 371
let current_file = ref ""

372 373 374
let scrolled_task_view =
  GBin.scrolled_window
    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
375
    ~shadow_type:`ETCHED_OUT ~packing:task_tab#add ()
376 377 378 379 380 381 382 383

let task_view =
  GSourceView2.source_view
    ~editable:false
    ~show_line_numbers:true
    ~packing:scrolled_task_view#add
    ()

384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407
let scrolled_edited_view =
  GBin.scrolled_window
    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
    ~shadow_type:`ETCHED_OUT ~packing:edited_tab#add ()

let edited_view =
  GSourceView2.source_view
    ~editable:false
    ~show_line_numbers:true
    ~packing:scrolled_edited_view#add
    ()

let scrolled_output_view =
  GBin.scrolled_window
    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
    ~shadow_type:`ETCHED_OUT ~packing:output_tab#add ()

let output_view =
  GSourceView2.source_view
    ~editable:false
    ~show_line_numbers:true
    ~packing:scrolled_output_view#add
    ()

408 409 410 411 412 413 414 415 416 417 418 419
let scrolled_counterexample_view =
  GBin.scrolled_window
    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
    ~shadow_type:`ETCHED_OUT ~packing:counterexample_tab#add ()

let counterexample_view =
  GSourceView2.source_view
    ~editable:false
    ~show_line_numbers:true
    ~packing:scrolled_counterexample_view#add
    ()

420
let modifiable_sans_font_views = ref [goals_view#misc]
421
let modifiable_mono_font_views =
422
  ref [task_view#misc;edited_view#misc;output_view#misc;
MARCHE Claude's avatar
MARCHE Claude committed
423 424
       counterexample_view#misc
]
425 426 427 428
let () = task_view#source_buffer#set_language why_lang
let () = task_view#set_highlight_current_line true


429 430 431 432
let clear model = model#clear ()

let image_of_result ~obsolete result =
  match result with
433 434 435 436 437
    | Session.Interrupted -> !image_undone
    | Session.Unedited -> !image_editor
    | Session.JustEdited -> !image_unknown
    | Session.Scheduled -> !image_scheduled
    | Session.Running -> !image_running
438 439
    | Session.InternalFailure _ -> !image_failure
    | Session.Done r -> match r.Call_provers.pr_answer with
440 441 442 443 444 445
        | Call_provers.Valid ->
            if obsolete then !image_valid_obs else !image_valid
        | Call_provers.Invalid ->
            if obsolete then !image_invalid_obs else !image_invalid
        | Call_provers.Timeout ->
            if obsolete then !image_timeout_obs else !image_timeout
446 447
        | Call_provers.OutOfMemory ->
            if obsolete then !image_outofmemory_obs else !image_outofmemory
448 449 450
        | Call_provers.StepLimitExceeded ->
            if obsolete then !image_steplimitexceeded_obs
            else !image_steplimitexceeded
451 452 453 454 455 456
        | Call_provers.Unknown _ ->
            if obsolete then !image_unknown_obs else !image_unknown
        | Call_provers.Failure _ ->
            if obsolete then !image_failure_obs else !image_failure
        | Call_provers.HighFailure ->
            if obsolete then !image_failure_obs else !image_failure
457

458
(* connecting to the Session model *)
459

460 461 462 463 464 465 466 467
let fan n =
  match n mod 4 with
    | 0 -> "|"
    | 1 | -3 -> "\\"
    | 2 | -2 -> "-"
    | 3 | -1 -> "/"
    | _ -> assert false

François Bobot's avatar
François Bobot committed
468
module S = Session
MARCHE Claude's avatar
MARCHE Claude committed
469

470 471
let session_needs_saving = ref false

MARCHE Claude's avatar
MARCHE Claude committed
472
let set_row_status row b =
473 474 475
  match b with
  | Some t ->
    goals_model#set ~row:row#iter ~column:status_column !image_yes;
476
    let t = Format.sprintf "%.2f" t in
477 478 479 480
    goals_model#set ~row:row#iter ~column:time_column t
  | None ->
    goals_model#set ~row:row#iter ~column:status_column !image_unknown;
    goals_model#set ~row:row#iter ~column:time_column ""
MARCHE Claude's avatar
MARCHE Claude committed
481

482 483
let set_proof_state a =
  let obsolete = a.S.proof_obsolete in
François Bobot's avatar
François Bobot committed
484 485
  let row = a.S.proof_key in
  let res = a.S.proof_state in
486
  goals_model#set ~row:row#iter ~column:status_column
MARCHE Claude's avatar
MARCHE Claude committed
487 488
    (image_of_result ~obsolete res);
  let t = match res with
489
    | S.Done { Call_provers.pr_time = time; Call_provers.pr_steps = steps } ->
490
       let s =
François Bobot's avatar
François Bobot committed
491 492
        if gconfig.show_time_limit then
          Format.sprintf "%.2f [%d.0]" time a.S.proof_timelimit
MARCHE Claude's avatar
MARCHE Claude committed
493 494
        else
          Format.sprintf "%.2f" time
495
       in
496
       if steps >= 0 then
497 498 499
	 Format.sprintf "%s (steps: %d)" s steps
       else
	 s
500 501
    | S.Unedited -> "(not yet edited)"
    | S.JustEdited -> "(edited)"
François Bobot's avatar
François Bobot committed
502
    | S.InternalFailure _ -> "(internal failure)"
503 504
    | S.Interrupted -> "(interrupted)"
    | S.Scheduled | S.Running ->
505
        Format.sprintf "[limit=%d sec., %d M]"
506
          a.S.proof_timelimit a.S.proof_memlimit
MARCHE Claude's avatar
MARCHE Claude committed
507 508
  in
  let t = if obsolete then t ^ " (obsolete)" else t in
509 510
  (* TODO find a better way to signal arhived row *)
  let t = if a.S.proof_archived then t ^ " (archived)" else t in
511
  goals_model#set ~row:row#iter ~column:time_column t
MARCHE Claude's avatar
MARCHE Claude committed
512

513
let model_index = Hint.create 17
514

515
let get_any_from_iter row =
MARCHE Claude's avatar
MARCHE Claude committed
516
  try
517
    let idx = goals_model#get ~row ~column:index_column in
518
    Hint.find model_index idx
519 520
  with Not_found -> invalid_arg "Gmain.get_any_from_iter"

521
(*
522 523
let get_any (row:Gtk.tree_path) : M.any =
  get_any_from_iter (goals_model#get_iter row)
524 525 526 527 528 529 530 531
*)

let get_any_from_row_reference r = get_any_from_iter r#iter

let get_selected_row_references () =
  List.map
    (fun path -> goals_model#get_row_reference path)
    goals_view#selection#get_selected_rows
532

533
let row_expanded b iter _path =
534
  session_needs_saving := true;
535 536 537
  let expand_g g = goals_view#expand_row g.S.goal_key#path in
  let expand_tr _ tr = goals_view#expand_row tr.S.transf_key#path in
  let expand_m _ m = goals_view#expand_row m.S.metas_key#path in
538
  match get_any_from_iter iter with
François Bobot's avatar
François Bobot committed
539 540 541 542 543
    | S.File f ->
        S.set_file_expanded f b
    | S.Theory t ->
        S.set_theory_expanded t b
    | S.Goal g ->
544 545 546 547 548
        S.set_goal_expanded g b;
        if b then begin
          Session.PHstr.iter expand_tr g.S.goal_transformations;
          Session.Mmetas_args.iter expand_m g.S.goal_metas
        end
François Bobot's avatar
François Bobot committed
549
    | S.Transf tr ->
550 551 552 553 554
        S.set_transf_expanded tr b;
        if b then begin match tr.S.transf_goals with
          | [g] -> expand_g g
          | _ -> ()
        end
François Bobot's avatar
François Bobot committed
555
    | S.Proof_attempt _ -> ()
François Bobot's avatar
François Bobot committed
556
    | S.Metas m ->
557 558
        S.set_metas_expanded m b;
        if b then expand_g m.S.metas_goal
559

560 561 562 563 564 565 566
let current_selected_row = ref None
let current_env_session = ref None
let env_session () =
  match !current_env_session with
    | None -> assert false
    | Some e -> e

567
let task_text t =
MARCHE Claude's avatar
MARCHE Claude committed
568 569
  let max_boxes = (Gconfig.config ()).max_boxes in
  Pp.string_of ~max_boxes Pretty.print_task t
570

571
let split_transformation = "split_goal_wp"
572 573 574
let inline_transformation = "inline_goal"
let intro_transformation = "introduce_premises"

575 576 577 578 579 580 581 582 583 584 585 586 587 588 589
let goal_task_text g =
  if (Gconfig.config ()).intro_premises then
    let trans =
      Trans.lookup_transform intro_transformation (env_session()).S.env
    in
    task_text (try Trans.apply trans (S.goal_task g) with
      e -> eprintf "@.%a@." Exn_printer.exn_printer e; raise e)
  else
    task_text (S.goal_task g)

let update_tabs a =
  let task_text =
    match a with
    | S.Goal g -> goal_task_text g
    | S.Proof_attempt a -> goal_task_text a.S.proof_parent
590 591
    | S.Theory th -> "Theory " ^ th.S.theory_name.Ident.id_string
    | S.File file -> "File " ^ file.S.file_name
592 593 594 595 596 597 598 599 600 601
    | S.Transf tr -> "transformation \"" ^ tr.S.transf_name ^ "\""
    | S.Metas _ -> "metas"
  in
  let edited_text =
    match a with
    | S.Proof_attempt a ->
      begin
        let env = env_session () in
        match S.get_edited_as_abs env.S.session a with
        | None -> ""
MARCHE Claude's avatar
MARCHE Claude committed
602
        | Some f -> Sysutil.file_contents f
603 604 605 606 607
      end
    | _ -> ""
  in
  let output_text =
    match a with
608
    | S.Proof_attempt a ->
609
        begin
610
          match a.S.proof_state with
611
            | S.Interrupted -> "proof not yet scheduled for running"
François Bobot's avatar
François Bobot committed
612 613 614 615 616 617
            | S.Unedited ->
              "Interactive proof, not yet edited. Edit with \"Edit\" button"
            | S.JustEdited ->
              "Edited interactive proof. Run it with \"Replay\" button"
            | S.Done
                ({Call_provers.pr_answer = Call_provers.HighFailure} as r) ->
618
              Call_provers.print_prover_result str_formatter r;
619
                  flush_str_formatter ()
Andrei Paskevich's avatar
Andrei Paskevich committed
620
            | S.Done r ->
621
              let out = r.Call_provers.pr_output in
622 623 624
              if out = "" then
                "Output not available. Rerun it with \"Replay\" button"
              else out
625 626
            | S.Scheduled-> "proof scheduled but not running yet"
            | S.Running -> "prover currently running"
627
            | S.InternalFailure e ->
628 629
              fprintf str_formatter "%a" Exn_printer.exn_printer e;
              flush_str_formatter ()
630
        end
631 632 633 634 635 636 637 638 639 640
    | S.Metas m ->
      let print_meta_args =
        Pp.hov 2 (Pp.print_list Pp.space Pretty.print_meta_arg) in
      let print =
        Pp.print_iter2 Mstr.iter Pp.newline2 Pp.newline Pp.string
          (Pp.indent 2
             (Pp.print_iter1 S.Smeta_args.iter Pp.newline print_meta_args))
      in
      (Pp.string_of (Pp.hov 2 print) m.S.metas_added)
    | _ -> ""
641
 in
642

643
  let counterexample_text =
644 645 646 647 648
    match a with
    | S.Proof_attempt a ->
      begin
        match a.S.proof_state with
	  | S.Done r ->
649
	    if not (Model_parser.is_model_empty r.Call_provers.pr_model) then begin
650 651 652 653 654 655 656 657
	      let cntexample_text =
		if Debug.test_flag debug_show_text_cntexmp then
		  "Counterexample:\n" ^
		    (Model_parser.model_to_string r.Call_provers.pr_model) ^
		    "\n\nSource code interleaved with counterexample:"
		else
		  "" in
	      let cntexample_text = cntexample_text ^
658 659 660
		(Model_parser.interleave_with_source
		   r.Call_provers.pr_model
		   ~filename:!current_file
661 662
		   ~source_code:(Sysutil.file_contents !current_file)) in
	      cntexample_text
663 664
	    end else
	      ""
665
	  | _ -> ""
666 667 668
      end
    | _ -> ""
  in
669 670 671 672 673 674 675

  let lang =
    if Filename.check_suffix !current_file ".why" ||
      Filename.check_suffix !current_file ".mlw"
    then why_lang else any_lang !current_file
  in
  counterexample_view#source_buffer#set_language lang;
676

677 678 679 680 681 682
  task_view#source_buffer#set_text task_text;
  task_view#scroll_to_mark `INSERT;
  edited_view#source_buffer#set_text edited_text;
  edited_view#scroll_to_mark `INSERT;
  output_view#source_buffer#set_text output_text;
  counterexample_view#source_buffer#set_text counterexample_text;
683
  counterexample_view#scroll_to_mark `INSERT;
François Bobot's avatar
François Bobot committed
684

685

François Bobot's avatar
François Bobot committed
686 687

module MA = struct
François Bobot's avatar
François Bobot committed
688 689 690
     type key = GTree.row_reference

     let create ?parent () =
691
       reset_gc ();
692
       session_needs_saving := true;
François Bobot's avatar
François Bobot committed
693 694 695 696 697 698 699 700
       let parent = match parent with
         | None -> None
         | Some r -> Some r#iter
       in
       let iter = goals_model#append ?parent () in
       goals_model#set ~row:iter ~column:index_column (-1);
       goals_model#get_row_reference (goals_model#get_path iter)

François Bobot's avatar
François Bobot committed
701
     let keygen = create
François Bobot's avatar
François Bobot committed
702 703

     let remove row =
704
       session_needs_saving := true;
François Bobot's avatar
François Bobot committed
705 706
       let (_:bool) = goals_model#remove row#iter in ()

707
     let reset () =
708 709
       session_needs_saving := true;
       goals_model#clear ()
François Bobot's avatar
François Bobot committed
710 711 712 713 714 715 716 717 718 719 720

     let idle f =
       let (_ : GMain.Idle.id) = GMain.Idle.add f in ()

     let timeout ~ms f =
       let (_ : GMain.Timeout.id) = GMain.Timeout.add ~ms ~callback:f in
       ()

     let notify_timer_state =
       let c = ref 0 in
       fun t s r ->
721
         reset_gc ();
François Bobot's avatar
François Bobot committed
722 723 724 725 726 727 728
         incr c;
         monitor_waiting#set_text ("Waiting: " ^ (string_of_int t));
         monitor_scheduled#set_text ("Scheduled: " ^ (string_of_int s));
         monitor_running#set_text
           (if r=0 then "Running: 0" else
              "Running: " ^ (string_of_int r)^ " " ^ (fan (!c / 10)))

MARCHE Claude's avatar
MARCHE Claude committed
729
let notify any =
730
  reset_gc ();
731
  session_needs_saving := true;
732
  let row,expanded =
733
    match any with
734
      | S.Goal g -> g.S.goal_key, g.S.goal_expanded
François Bobot's avatar
François Bobot committed
735 736 737
      | S.Theory t -> t.S.theory_key, t.S.theory_expanded
      | S.File f -> f.S.file_key, f.S.file_expanded
      | S.Proof_attempt a -> a.S.proof_key,false
MARCHE Claude's avatar
MARCHE Claude committed
738
      | S.Transf tr ->
739
        tr.S.transf_key,tr.S.transf_expanded
François Bobot's avatar
François Bobot committed
740
      | S.Metas m -> m.S.metas_key,m.S.metas_expanded
741
  in
742 743 744 745 746 747 748 749 750
  (* name is set by notify since upgrade policy may update the prover name *)
  goals_model#set ~row:row#iter ~column:name_column
    (match any with
      | S.Goal g -> S.goal_expl g
      | S.Theory th -> th.S.theory_name.Ident.id_string
      | S.File f -> Filename.basename f.S.file_name
      | S.Proof_attempt a ->
        let p = a.S.proof_prover in
        Pp.string_of_wnl C.print_prover p
François Bobot's avatar
François Bobot committed
751 752 753
      | S.Transf tr -> tr.S.transf_name
      | S.Metas _m -> "Metas..."
   );
754 755 756 757
  let ind = goals_model#get ~row:row#iter ~column:index_column in
  begin
    match !current_selected_row with
      | Some r when r == ind ->
758
        update_tabs any
759
      | _ -> ()
760
  end;
761
  if expanded then goals_view#expand_to_path row#path else
762
    goals_view#collapse_row row#path;
MARCHE Claude's avatar
MARCHE Claude committed
763
  match any with
François Bobot's avatar
François Bobot committed
764 765 766 767 768 769 770
    | S.Goal g ->
        set_row_status row g.S.goal_verified
    | S.Theory th ->
        set_row_status row th.S.theory_verified
    | S.File file ->
        set_row_status row file.S.file_verified
    | S.Proof_attempt a ->
771
        set_proof_state a
François Bobot's avatar
François Bobot committed
772 773
    | S.Transf tr ->
        set_row_status row tr.S.transf_verified
774
    | S.Metas m ->
François Bobot's avatar
François Bobot committed
775
        set_row_status row m.S.metas_verified
776

MARCHE Claude's avatar
MARCHE Claude committed
777 778
let init =
  let cpt = ref (-1) in
779
  fun row any ->
780
    reset_gc ();
MARCHE Claude's avatar
MARCHE Claude committed
781 782 783 784
    let ind = goals_model#get ~row:row#iter ~column:index_column in
    if ind < 0 then
      begin
        incr cpt;
785
        Hint.add model_index !cpt any;
MARCHE Claude's avatar
MARCHE Claude committed
786 787 788 789
        goals_model#set ~row:row#iter ~column:index_column !cpt
      end
    else
      begin
790
        Hint.replace model_index ind any;
MARCHE Claude's avatar
MARCHE Claude committed
791
      end;
792
    (* useless since it has no child: goals_view#expand_row row#path; *)
MARCHE Claude's avatar
MARCHE Claude committed
793
    goals_model#set ~row:row#iter ~column:icon_column
794
      (match any with
MARCHE Claude's avatar
MARCHE Claude committed
795 796 797
         | S.Goal _ -> !image_goal
         | S.Theory _ -> !image_theory
         | S.File _ -> !image_file
François Bobot's avatar
François Bobot committed
798
         | S.Proof_attempt _ -> !image_prover
François Bobot's avatar
François Bobot committed
799 800
         | S.Transf _ -> !image_transf
         | S.Metas _ -> !image_metas);
MARCHE Claude's avatar
MARCHE Claude committed
801
    notify any
MARCHE Claude's avatar
MARCHE Claude committed
802

François Bobot's avatar
François Bobot committed
803 804 805 806
let rec init_any any =
  init (S.key_any any) any;
  S.iter init_any any

807
let uninstalled_prover = Gconfig.uninstalled_prover gconfig
808

François Bobot's avatar
François Bobot committed
809 810 811 812
end

module M = Session_scheduler.Make(MA)

813

MARCHE Claude's avatar
MARCHE Claude committed
814 815
let () = w#add_accel_group accel_group
let () = w#show ()
816

817 818 819 820
(********************)
(* opening database *)
(********************)

821
(** TODO remove that should done only in session *)
822 823
let project_dir =
  let fname = Queue.pop files in
824
  (* The remaining files in [files] are going to be open *)
825 826 827 828
  if Sys.file_exists fname then
    begin
      if Sys.is_directory fname then
        begin
829
          Debug.dprintf debug
MARCHE Claude's avatar
MARCHE Claude committed
830
            "[GUI] found directory '%s' for the project@." fname;
831
          fname
832 833
        end
      else
834
        if Queue.is_empty files then (* that was the only file *) begin
MARCHE Claude's avatar
MARCHE Claude committed
835
          Debug.dprintf debug "[GUI] found regular file '%s'@." fname;
836 837 838 839
          let d =
            try Filename.chop_extension fname
            with Invalid_argument _ -> fname
          in
840
          Debug.dprintf debug
MARCHE Claude's avatar
MARCHE Claude committed
841
            "[GUI] using '%s' as directory for the project@." d;
842
          Queue.push fname files; (* we need to open [fname] *)
843 844 845
          d
        end
        else begin
846
          (* The first argument is not a directory and it's not the
847 848 849 850 851 852
              only file *)
          Format.eprintf
            "[Error] @[When@ more@ than@ one@ file@ is@ given@ on@ the@ \
             command@ line@ the@ first@ one@ must@ be@ the@ directory@ \
             of@ the@ session.@]@.";
          Arg.usage spec usage_str; exit 1
853 854 855
        end
    end
  else
856
    fname
857 858 859 860

let () =
  if not (Sys.file_exists project_dir) then
    begin
MARCHE Claude's avatar
MARCHE Claude committed
861
      Debug.dprintf debug "[GUI] '%s' does not exist. \
862
        Creating directory of that name for the project@." project_dir;
863 864 865 866 867 868 869 870 871 872 873 874
      Unix.mkdir project_dir 0o777
    end

let info_window ?(callback=(fun () -> ())) mt s =
  let buttons = match mt with
    | `INFO -> GWindow.Buttons.close
    | `WARNING -> GWindow.Buttons.close
    | `QUESTION -> GWindow.Buttons.ok_cancel
    | `ERROR -> GWindow.Buttons.close
  in
  let d = GWindow.message_dialog
    ~message:s
875
    ~message_type:(mt :> Gtk.Tags.message_type)
876
    ~buttons
877
    ~title:"Why3IDE"
878
    ~icon:(!Gconfig.why_icon)
879
    ~modal:true
880 881 882 883
    ~show:true ()
  in
  let (_ : GtkSignal.id) =
    d#connect#response
884
      ~callback:(function x ->
885 886
                   d#destroy ();
                   if mt <> `QUESTION || x = `OK then callback ())
887 888
  in ()

889
let file_info = GMisc.label ~text:""
890
  ~packing:(source_tab#pack ~fill:true ?from:None ?expand:None ?padding:None) ()
891

892
let warnings = Queue.create ()
MARCHE Claude's avatar
MARCHE Claude committed
893

894 895 896 897
let record_warning ?loc msg =
  Format.eprintf "%awarning: %s@."
    (Pp.print_option Loc.report_position) loc msg;
  Queue.push (loc,msg) warnings
MARCHE Claude's avatar
MARCHE Claude committed
898

899 900 901 902 903
let () = Warning.set_hook record_warning

let display_warnings () =
  if Queue.is_empty warnings then () else
    begin
904 905
      let nwarn = ref 0 in
      begin try
Andrei Paskevich's avatar
Andrei Paskevich committed
906
      Queue.iter
907
        (fun (loc,msg) ->
908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925
         if !nwarn = 4 then
           begin
             Format.fprintf Format.str_formatter "[%d more warnings. See stderr for details]@\n" (Queue.length warnings - !nwarn);
             raise Exit
           end
         else
           begin
             incr nwarn;
             match loc with
             | None ->
                Format.fprintf Format.str_formatter "%s@\n@\n" msg
             | Some l ->
                (* scroll_to_loc ~color:error_tag ~yalign:0.5 loc; *)
                Format.fprintf Format.str_formatter "%a: %s@\n@\n"
                               Loc.gen_report_position l msg
           end) warnings;
        with Exit -> ();
      end;
926 927 928 929 930 931
      Queue.clear warnings;
      let msg =
        Format.flush_str_formatter ()
      in
  (* file_info#set_text msg; *)
      info_window `WARNING msg
Andrei Paskevich's avatar
Andrei Paskevich committed
932
    end
MARCHE Claude's avatar
MARCHE Claude committed
933

934 935
(* check if provers are present *)
let () =
936
  if C.Mprover.is_empty (C.get_provers gconfig.Gconfig.config) then
937
    begin
François Bobot's avatar
François Bobot committed
938
      info_window `ERROR
939
        "No prover configured.\nPlease run 'why3 config --detect-provers' first"
940 941 942 943 944
        ~callback:GMain.quit;
      GMain.main ();
      exit 2;
    end

945
let sched =
946
  try
MARCHE Claude's avatar
MARCHE Claude committed
947
    Debug.dprintf debug "@[<hov 2>[GUI session] Opening session...@\n";
948
    let session,use_shapes =
MARCHE Claude's avatar
MARCHE Claude committed
949
      if Sys.file_exists project_dir then
950
        S.read_session project_dir
MARCHE Claude's avatar
MARCHE Claude committed
951
      else
952
        S.create_session project_dir, false
MARCHE Claude's avatar
MARCHE Claude committed
953
    in
954
    let env,(_:bool),(_:bool) =
955 956
      M.update_session ~allow_obsolete:true ~release:false ~use_shapes
        session gconfig.env gconfig.Gconfig.config
957
    in
MARCHE Claude's avatar
MARCHE Claude committed
958
    Debug.dprintf debug "@]@\n[GUI session] Opening session: update done@.  @[<hov 2>";
959
    let sched = M.init (gconfig.session_nb_processes)
960
    in
MARCHE Claude's avatar
MARCHE Claude committed
961
    Debug.dprintf debug "@]@\n[GUI session] Opening session: done@.";
962
    session_needs_saving := false;
963 964
    current_env_session := Some env;
    sched
965
  with e when not (Debug.test_flag Debug.stack_trace) ->
966 967 968 969 970
    eprintf "@[Error while opening session:@ %a@.@]"
      Exn_printer.exn_printer e;
    exit 1


971 972 973 974
(**********************************)
(* add new file from command line *)
(**********************************)

975
let open_file ?(start=false) f =
976
  let f = Sysutil.relativize_filename project_dir f in
MARCHE Claude's avatar
MARCHE Claude committed
977
  Debug.dprintf debug "[GUI session] Adding file '%s'@." f;
978
  if S.PHstr.mem (env_session()).S.session.S.session_files f then
MARCHE Claude's avatar
MARCHE Claude committed
979
    Debug.dprintf debug "[GUI] file %s already in database@." f
980 981
  else
    try
MARCHE Claude's avatar
MARCHE Claude committed
982
      Debug.dprintf debug "[GUI] adding file %s in database@." f;
983 984
      ignore (M.add_file (env_session()) ?format:!opt_parser f);
    with e ->
985 986 987 988 989 990 991 992 993 994 995
      if start
      then begin
        eprintf "@[Error while reading file@ '%s':@ %a@]@." f
          Exn_printer.exn_printer e;
        exit 1
      end
      else
        let msg =
          Pp.sprintf_wnl "@[Error while reading file@ '%s':@ %a@]" f
            Exn_printer.exn_printer e in
        info_window `ERROR msg