why3ide.ml 82.9 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

12
open Why3
13
open Format
14
open Gconfig
15
open Wstdlib
16 17
open Ide_utils
open History
18
open Itp_communication
19

20 21
module GSourceView = GSourceView2

22 23
external reset_gc : unit -> unit = "ml_reset_gc"

24
let debug = Debug.lookup_flag "ide_info"
25
let debug_stack_trace = Debug.lookup_flag "stack_trace"
26

27 28 29 30 31
(***************************)
(* Debugging Json protocol *)
(***************************)


32
(* TODO remove print_request_json and print_notification_json *)
33 34 35 36 37
exception Badparsing

let print_request_json fmt (r: ide_request) =
  (try (
    let s = Pp.string_of Json_util.print_request r in
38
    let x = Json_util.parse_request s in
39 40 41 42 43 44 45
    if r = x then () else raise Badparsing)
  with
    _ -> Format.eprintf "Bad parsing@.");
  Json_util.print_request fmt r

let print_notification_json fmt (n: notification) =
  (try (
46
    let x = Json_util.parse_notification (Pp.string_of Json_util.print_notification n) in
47 48 49 50 51 52 53 54
    if n = x then () else raise Badparsing)
  with
    _ -> Format.eprintf "Bad parsing@.");
  Json_util.print_notification fmt n

let debug_json = Debug.register_flag "json_proto"
    ~desc:"Print@ json@ requests@ and@ notifications@"

Clément Fumex's avatar
Clément Fumex committed
55 56 57
(*******************)
(* server protocol *)
(*******************)
58

MARCHE Claude's avatar
MARCHE Claude committed
59

60
module Protocol_why3ide = struct
Clément Fumex's avatar
Clément Fumex committed
61 62

  let debug_proto = Debug.register_flag "ide_proto"
63
      ~desc:"Print@ debugging@ messages@ about@ Why3Ide@ protocol@"
Clément Fumex's avatar
Clément Fumex committed
64 65

  let print_request_debug r =
66
    Debug.dprintf debug_proto "request %a@." print_request r;
67
    Debug.dprintf debug_json "%a@." print_request_json r
Clément Fumex's avatar
Clément Fumex committed
68

69
  let print_msg_debug m =
70
    Debug.dprintf debug_proto "message %a@." print_msg m
Clément Fumex's avatar
Clément Fumex committed
71 72

  let print_notify_debug n =
73
    Debug.dprintf debug_proto "handling notification %a@." print_notify n;
74
    Debug.dprintf debug_json "%a@." print_notification_json n
Clément Fumex's avatar
Clément Fumex committed
75 76 77 78

  let list_requests: ide_request list ref = ref []

  let get_requests () =
79 80
    let n = List.length !list_requests in
    if n > 0 then
81
      Debug.dprintf debug_proto "got %d new requests@." n;
Clément Fumex's avatar
Clément Fumex committed
82 83 84 85 86
    let l = List.rev !list_requests in
    list_requests := [];
    l

  let send_request r =
87
    print_request_debug r;
Clément Fumex's avatar
Clément Fumex committed
88 89 90 91 92
    list_requests := r :: !list_requests

  let notification_list: notification list ref = ref []

  let notify n =
93
(* too early, print when handling notifications
Clément Fumex's avatar
Clément Fumex committed
94
    print_notify_debug n;
95
 *)    notification_list := n :: !notification_list
Clément Fumex's avatar
Clément Fumex committed
96 97

  let get_notified () =
98 99
    let n = List.length !notification_list in
    if n > 0 then
100
      Debug.dprintf debug_proto "got %d new notifications@." n;
Clément Fumex's avatar
Clément Fumex committed
101 102 103
    let l = List.rev !notification_list in
    notification_list := [];
    l
104 105 106

end

Clément Fumex's avatar
Clément Fumex committed
107
let get_notified = Protocol_why3ide.get_notified
108

109
let send_request r = Protocol_why3ide.send_request r
110

Clément Fumex's avatar
Clément Fumex committed
111 112 113
(****************************************)
(* server instance on the GTK scheduler *)
(****************************************)
114

115 116 117 118 119 120 121 122 123 124
(*
   The gtk scheduler is catching all exceptions avoiding the printing of the
   backtrace that is normally done by debug option stack_trace. To recover this
   behavior we catch exceptions ourselves. If "stack_trace" is on, we exit on
   first exception and print backtrace on standard output otherwise we raise
   the exception again (with information on error output).
*)
let backtrace_and_exit f () =
  try f () with
  | e ->
125 126 127 128 129 130 131 132 133 134 135 136 137 138
     if Debug.test_flag debug_stack_trace then
       begin
         Printexc.print_backtrace stderr;
         Format.eprintf "exception '%a' was raised in a LablGtk callback.@."
                        Exn_printer.exn_printer e;
         exit 1
       end
     else
       begin
         Format.eprintf "exception '%a' was raised in a LablGtk callback.@."
                        Exn_printer.exn_printer e;
         Format.eprintf "This should not happen. Please report. @.";
         raise e
       end
139

140
module Scheduler = struct
141

142 143
    let blocking = false

144
    let multiplier = 3
145

Clément Fumex's avatar
Clément Fumex committed
146
    let idle ~prio f =
147
      let (_ : GMain.Idle.id) = GMain.Idle.add ~prio (backtrace_and_exit f) in ()
148

Clément Fumex's avatar
Clément Fumex committed
149
    let timeout ~ms f =
150 151
      let (_ : GMain.Timeout.id) =
        GMain.Timeout.add ~ms ~callback:(backtrace_and_exit f) in ()
Clément Fumex's avatar
Clément Fumex committed
152
end
153

154
module Server = Itp_server.Make (Scheduler) (Protocol_why3ide)
155

Clément Fumex's avatar
Clément Fumex committed
156 157 158
(************************)
(* parsing command line *)
(************************)
159

Clément Fumex's avatar
Clément Fumex committed
160 161
let files : string Queue.t = Queue.create ()
let opt_parser = ref None
162
let opt_batch = ref None
Clément Fumex's avatar
Clément Fumex committed
163

164
let spec = [
Clément Fumex's avatar
Clément Fumex committed
165 166 167 168
  "-F", Arg.String (fun s -> opt_parser := Some s),
      "<format> select input format (default: \"why\")";
  "--format", Arg.String (fun s -> opt_parser := Some s),
      " same as -F";
169
(*
Clément Fumex's avatar
Clément Fumex committed
170 171 172
  "-f",
   Arg.String (fun s -> input_files := s :: !input_files),
   "<file> add file to the project (ignored if it is already there)";
173
*)
174 175
  Termcode.arg_extra_expl_prefix;
  "--batch", Arg.String (fun s -> opt_batch := Some s), "";
Clément Fumex's avatar
Clément Fumex committed
176
]
177

Clément Fumex's avatar
Clément Fumex committed
178 179 180
let usage_str = sprintf
  "Usage: %s [options] [<file.why>|<project directory>]..."
  (Filename.basename Sys.argv.(0))
181

182 183 184
let env, gconfig = try
  let config, base_config, env =
    Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str in
Clément Fumex's avatar
Clément Fumex committed
185 186 187
    if Queue.is_empty files then
      Whyconf.Args.exit_with_usage spec usage_str;
    Gconfig.load_config config base_config;
188
    env, Gconfig.config ()
Clément Fumex's avatar
Clément Fumex committed
189 190 191 192 193 194

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


195

MARCHE Claude's avatar
MARCHE Claude committed
196 197 198 199
(********************************)
(* Source language highlighting *)
(********************************)

200

MARCHE Claude's avatar
MARCHE Claude committed
201
let (why_lang, any_lang) =
Clément Fumex's avatar
Clément Fumex committed
202 203
  let main = Whyconf.get_main gconfig.config in
  let load_path = Filename.concat (Whyconf.datadir main) "lang" in
MARCHE Claude's avatar
MARCHE Claude committed
204
  let languages_manager =
205
    GSourceView.source_language_manager ~default:true
MARCHE Claude's avatar
MARCHE Claude committed
206 207 208 209 210 211
  in
  languages_manager#set_search_path
    (load_path :: languages_manager#search_path);
  let why_lang =
    match languages_manager#language "why3" with
    | None ->
Clément Fumex's avatar
Clément Fumex committed
212
        eprintf "language file for 'why3' not found in directory %s@."
MARCHE Claude's avatar
MARCHE Claude committed
213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235
          load_path;
        exit 1
    | 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)

(* Borrowed from Frama-C src/gui/source_manager.ml:
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

236

237 238 239 240 241 242
(****************************)
(* Color handling in source *)
(****************************)

(* For each view, we have to recreate the tags *)
let create_colors v =
243
  let premise_tag (v: GSourceView.source_view) = v#buffer#create_tag
244
      ~name:"premise_tag" [`BACKGROUND gconfig.premise_color] in
245
  let neg_premise_tag (v: GSourceView.source_view) = v#buffer#create_tag
246
      ~name:"neg_premise_tag" [`BACKGROUND gconfig.neg_premise_color] in
247
  let goal_tag (v: GSourceView.source_view) = v#buffer#create_tag
248
      ~name:"goal_tag" [`BACKGROUND gconfig.goal_color] in
249
  let error_line_tag (v: GSourceView.source_view) = v#buffer#create_tag
250
      ~name:"error_line_tag" [`BACKGROUND gconfig.error_line_color] in
251
  let error_tag (v: GSourceView.source_view) = v#buffer#create_tag
252
      ~name:"error_tag" [`BACKGROUND gconfig.error_color_bg] in
253 254 255
  let _ : GText.tag = premise_tag v in
  let _ : GText.tag = neg_premise_tag v in
  let _ : GText.tag = goal_tag v in
256
  let _ : GText.tag = error_line_tag v in
257 258 259 260
  let _ : GText.tag = error_tag v in
  ()

(* Erase all the source location tags in a source file *)
261
let erase_color_loc (v:GSourceView.source_view) =
262 263 264 265
  let buf = v#buffer in
  buf#remove_tag_by_name "premise_tag" ~start:buf#start_iter ~stop:buf#end_iter;
  buf#remove_tag_by_name "neg_premise_tag" ~start:buf#start_iter ~stop:buf#end_iter;
  buf#remove_tag_by_name "goal_tag" ~start:buf#start_iter ~stop:buf#end_iter;
266 267
  buf#remove_tag_by_name "error_tag" ~start:buf#start_iter ~stop:buf#end_iter;
  buf#remove_tag_by_name "error_line_tag" ~start:buf#start_iter ~stop:buf#end_iter
268 269


270

271 272 273 274 275 276 277 278 279 280 281 282 283 284 285
(*******************)
(* Graphical tools *)
(*******************)

(* Elements needed for usage of graphical elements *)

(* [quit_on_saved] set to true by exit function to delay quiting after Saved
   notification is received *)
let quit_on_saved = ref false

(* Exit brutally without asking anything *)
let exit_function_unsafe () =
  send_request Exit_req;
  GMain.quit ()

286
(* Contains quadruples (tab page, source_view, file_has_been_modified, label_of_tab):
287 288 289 290 291 292
   - tab_page is a unique number for each pages of the notebook
   - source_view is the graphical element inside a tab
   - has_been_modified is a reference to a boolean stating if the current tab
     source has been modified
   - label_of_tab is the mutable title of the tab
*)
293
let source_view_table : (int * GSourceView.source_view * bool ref * GMisc.label) Hstr.t =
294 295
  Hstr.create 14

296 297 298
(* The corresponding file does not have a source view *)
exception Nosourceview of string

299 300 301 302 303
let get_source_view_table (file:string) =
  match Hstr.find source_view_table file with
  | v -> v
  | exception Not_found -> raise (Nosourceview file)

304
(* This returns the source_view of a file *)
305
let get_source_view (file: string) : GSourceView.source_view =
306 307 308 309
  match Hstr.find source_view_table file with
  | (_, v, _, _) -> v
  | exception Not_found -> raise (Nosourceview file)

310 311 312
(* Saving function for sources *)
let save_sources () =
  Hstr.iter
313
    (fun k (_n, (s: GSourceView.source_view), b, _l) ->
314 315 316 317 318 319 320 321 322 323 324 325 326
      if !b then
        let text_to_save = s#source_buffer#get_text () in
        send_request (Save_file_req (k, text_to_save))
    )
    source_view_table

(* True if there exist a file which needs saving *)
let files_need_saving () =
  Hstr.fold (fun _k (_, _, b, _) acc -> !b || acc) source_view_table false

(* Ask if the user wants to save session before exit. Exit is then delayed until
   the [Saved] notification is received *)
let exit_function_safe () =
327 328 329 330
  send_request Check_need_saving_req

let exit_function_handler b =
  if not b && not (files_need_saving ()) then
331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357
    exit_function_unsafe ()
  else
    let answer =
      GToolbox.question_box
        ~title:"Why3 saving session and files"
        ~buttons:["Yes"; "No"; "Cancel"]
        "Do you want to save the session and unsaved files?"
    in
    begin
      match answer with
      | 1 -> save_sources(); send_request Save_req; quit_on_saved := true
      | 2 -> exit_function_unsafe ()
      | _ -> ()
    end

(* Update name of the tab when the label changes so that it has a * as prefix *)
let update_label_change (label: GMisc.label) =
  let s = label#text in
  if not (Strings.has_prefix "*" s) then
    label#set_text ("*" ^ s)

(* Update name of the tab when the label is saved. Removes * prefix *)
let update_label_saved (label: GMisc.label) =
  let s = label#text in
  if (Strings.has_prefix "*" s) then
    label#set_text (String.sub s 1 (String.length s - 1))

358 359 360 361 362 363
let make_sources_editable b =
  Hstr.iter
    (fun _ (_,source_view,_,_) ->
      source_view#set_editable b;
      source_view#set_auto_indent b)
    source_view_table
364

365 366 367
(**********************)
(* Graphical elements *)
(**********************)
368

369
let initialization_complete = ref false
370 371 372 373 374 375
let warnings = Queue.create ()

let record_warning ?loc msg =
  Format.eprintf "%awarning: %s@."
    (Pp.print_option Loc.report_position) loc msg;
  Queue.push (loc,msg) warnings
376 377

let () =
378
  Warning.set_hook record_warning;
379 380 381 382 383 384 385 386 387 388 389 390 391 392
  let dir =
    try
      Server_utils.get_session_dir ~allow_mkdir:true files
    with Invalid_argument s ->
      Format.eprintf "Error: %s@." s;
      Whyconf.Args.exit_with_usage spec usage_str
  in
  Server.init_server gconfig.config env dir;
  Queue.iter (fun f -> send_request (Add_file_req f)) files;
  send_request Get_global_infos;
  Debug.dprintf debug "Init the GTK interface...@?";
  ignore (GtkMain.Main.init ());
  Debug.dprintf debug " done.@.";
  Gconfig.init ()
393

394
let window_title =
395
  match !opt_batch with
396 397
  | Some _ -> "Why3 Batch Mode"
  | None -> "Why3 Interactive Proof Session"
398

399
let main_window : GWindow.window =
400 401
  let w = GWindow.window ~title:window_title () in
  w#resize ~width:gconfig.window_width ~height:gconfig.window_height;
402 403 404 405 406 407 408 409
  (* callback to record the new size of the main window when changed, so
   that on restart the window size is the same as the last session *)
  let (_ : GtkSignal.id) =
    w#misc#connect#size_allocate
      ~callback:
      (fun {Gtk.width=w;Gtk.height=h} ->
       gconfig.window_height <- h;
       gconfig.window_width <- w)
410 411
  in
  w
412 413

(* the main window contains a vertical box, containing:
414 415
   1. the menu [menubar]
   2. an horizontal box [hb]
416 417 418 419 420 421 422 423 424 425
 *)

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

let menubar = GMenu.menu_bar
  ~packing:(vbox#pack ?from:None ?expand:None ?fill:None ?padding:None)
  ()

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

426
let accel_group = GtkData.AccelGroup.create ()
427

428 429 430
(* context_tools : simplified tools menu for mouse-3 *)

let context_tools_menu = GMenu.menu ()
431

432 433 434 435 436 437 438 439 440 441 442
(****************************)
(* actions of the interface *)
(****************************)


(***********************************)
(* connection of actions to signals *)
(***********************************)

(* File menu signals *)

443 444 445 446 447 448 449 450
let send_session_config_to_server () =
  let nb = gconfig.session_nb_processes in
  send_request (Set_config_param("max_tasks",nb));
  let nb = gconfig.session_time_limit in
  send_request (Set_config_param("timelimit",nb));
  let nb = gconfig.session_mem_limit in
  send_request (Set_config_param("memlimit",nb))

451 452 453 454 455 456 457
let (_ : GtkSignal.id) =
  main_window#connect#destroy
    ~callback:exit_function_safe

let (_ : GtkSignal.id) =
  main_window#event#connect#delete
    ~callback:(fun _ -> exit_function_safe (); true)
458

459 460
(* 2. horizontal box contains:
   2.1 TODO: a tool box ?
461 462 463
   2.2 a horizontal paned [hp] containing:
     2.2.1 a scrolled window to hold the tree view of the session [scrolledview]
     2.2.2 a vertical paned containing [vpan222]
464 465 466 467
*)

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

468 469
(** {2 view for the session tree} *)
let scrolled_session_view =
470 471 472
  let sv =
    GBin.scrolled_window
      ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
473
      ~shadow_type:`ETCHED_OUT
474 475
      ~packing:hp#add ()
  in
476
  hp#set_position gconfig.tree_width;
477 478 479 480 481 482 483
  let (_ : GtkSignal.id) =
    sv#misc#connect#size_allocate
      ~callback:
      (fun {Gtk.width=w;Gtk.height=_h} ->
       gconfig.tree_width <- w)
  in sv

484 485 486 487 488 489 490
(* Vertical pan *)
let vpan222 = GPack.paned `VERTICAL ~packing:hp#add ()

(*  the scrolled window 2.2.1 [scrolled_session_view] contains a GTK tree

*)

491 492
(** {3 the model for tree view} *)

493
let cols = new GTree.column_list
494
(* first column: unique id of the object *)
Clément Fumex's avatar
Clément Fumex committed
495
let node_id_column = cols#add Gobject.Data.int
496 497 498 499 500
(* second column: an icon identifying the object: file,theory, goal, transformation *)
let icon_column = cols#add Gobject.Data.gobject
(* third column: name of the object *)
let name_column = cols#add Gobject.Data.string
(* fourth column: icon status for the object: proved/unproved, unknown, timeout, etc. *)
501
let status_column = cols#add Gobject.Data.gobject
502
(* fifth column: extra status info: time, obsolete status, limits *)
503
let time_column = cols#add Gobject.Data.string
504

505 506 507 508
let column_status_title = "Status"
let column_time_title = "Time"
let column_goals_title = "Theories/Goals"

509 510
(* first view column: icon and name *)
let view_name_column =
511
  let v = GTree.view_column ~title:column_goals_title () in
512 513
  (* icon attribute *)
  let icon_renderer = GTree.cell_renderer_pixbuf [ ] in
514
  v#pack icon_renderer ~expand:false;
515 516 517 518
  v#add_attribute icon_renderer "pixbuf" icon_column;
  let name_renderer = GTree.cell_renderer_text [`XALIGN 0.] in
  v#pack name_renderer;
  v#add_attribute name_renderer "text" name_column;
519
  (* v#set_sizing `AUTOSIZE; *)
520
  v#set_resizable true;
521
  (*  v#set_max_width 1000;*)
522 523 524 525 526
  v

(* second view column: status *)
let view_status_column =
  let status_renderer = GTree.cell_renderer_pixbuf [ ] in
527
  let v = GTree.view_column ~title:column_status_title
528 529 530 531 532 533
                            ~renderer:(status_renderer, ["pixbuf", status_column])
                            ()
  in
  v#set_resizable false;
  v#set_visible true;
  v
534 535 536

let view_time_column =
  let renderer = GTree.cell_renderer_text [`XALIGN 0.] in
537
  let v = GTree.view_column ~title:column_time_title
538 539 540 541 542
                            ~renderer:(renderer, ["text", time_column]) ()
  in
  v#set_resizable false;
  v#set_visible true;
  v
543

544
let goals_model,goals_view =
545
  Debug.dprintf debug "Creating tree model...@?";
546 547 548
  let model = GTree.tree_store cols in
  let view = GTree.view ~model ~packing:scrolled_session_view#add () in
  let () = view#selection#set_mode (* `SINGLE *) `MULTIPLE in
549
(*
550
  let () = view#set_rules_hint true in
551 552
*)
  let () = view#set_enable_search false in
553
  let _: int = view#append_column view_status_column in
554
  let _: int = view#append_column view_name_column in
555
  let _: int = view#append_column view_time_column in
556
  view#set_expander_column (Some view_name_column);
557
  Debug.dprintf debug "done@.";
558
  model,view
559

560 561 562 563 564 565 566 567 568 569 570 571

(***********************************)
(* Mapping session to the GTK tree *)
(***********************************)

type pa_status = Controller_itp.proof_attempt_status
      * bool   (* obsolete or not *) (* TODO *)
      * Call_provers.resource_limit

let node_id_type : node_type Hint.t = Hint.create 17
let node_id_proved : bool Hint.t = Hint.create 17
let node_id_pa : pa_status Hint.t = Hint.create 17
572
let node_id_detached : bool Hint.t = Hint.create 17
573 574

let get_node_type id = Hint.find node_id_type id
575 576 577 578 579

let get_node_proved id =
  try Hint.find node_id_proved id
  with Not_found -> false

580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597
let get_node_id_pa id = Hint.find node_id_pa id

let get_obs (pa_st: pa_status) = match pa_st with
| _, b, _ -> b

let get_proof_attempt (pa_st: pa_status) = match pa_st with
| pa, _, _ -> pa

let get_node_obs id = get_obs (get_node_id_pa id)
let get_node_proof_attempt id = get_proof_attempt (get_node_id_pa id)

let get_node_id iter = goals_model#get ~row:iter ~column:node_id_column

(* To each node we have the corresponding row_reference *)
let node_id_to_gtree : GTree.row_reference Hint.t = Hint.create 42
(* TODO exception for those: *)
let get_node_row id = Hint.find node_id_to_gtree id

598 599 600
let get_node_detached id =
  Hint.find node_id_detached id

601 602 603 604 605 606 607 608 609 610 611 612 613 614
(******************************)
(* Initialization of the tree *)
(******************************)

let remove_tree goals_model =
  Hint.iter (fun _x i ->
    try ignore(goals_model#remove (i#iter)) with _ -> ())
    node_id_to_gtree

let clear_tree_and_table goals_model =
  remove_tree goals_model;
  Hint.clear node_id_to_gtree;
  Hint.clear node_id_type;
  Hint.clear node_id_proved;
615 616
  Hint.clear node_id_pa;
  Hint.clear node_id_detached
617 618 619 620 621


(**************)
(* Menu items *)
(**************)
622

Clément Fumex's avatar
Clément Fumex committed
623
(* vpan222 contains:
624
   2.2.2.1 a notebook containing view of the current task, source code etc
625
   2.2.2.2 a vertical pan which contains [vbox2222]
Clément Fumex's avatar
Clément Fumex committed
626
     2.2.2.2.1 the input field to type commands
627
     2.2.2.2.2 a scrolled window to hold the output of the commands
628 629
 *)

630 631 632
(***********************************)
(*    notebook on the top 2.2.2.1  *)
(***********************************)
633

634
(* notebook is composed of a Task page and several source files pages *)
635 636
let notebook = GPack.notebook ~packing:vpan222#add ()

637 638 639
(********************************)
(* Task view (part of notebook) *)
(********************************)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
640
let scrolled_task_view =
641
  let label = GMisc.label ~text:"Task" () in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
642
  GPack.vbox ~homogeneous:false ~packing:
643 644
    (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()

645 646
let scrolled_task_view =
  GBin.scrolled_window
647
    ~height:gconfig.task_height
648 649
    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
    ~shadow_type:`ETCHED_OUT
650
    ~packing:scrolled_task_view#add ()
651

652 653 654 655 656 657 658
let (_ : GtkSignal.id) =
  scrolled_task_view#misc#connect#size_allocate
    ~callback:
    (fun {Gtk.width=_w;Gtk.height=h} ->
       gconfig.task_height <- h)


659
let task_view =
660
  GSourceView.source_view
661
    ~editable:false
Clément Fumex's avatar
Clément Fumex committed
662
    ~cursor_visible:false
663 664 665 666
    ~show_line_numbers:true
    ~packing:scrolled_task_view#add
    ()

667

668
(* Creating a page for source code view *)
669
let create_source_view =
670
  (* Counter for pages *)
671
  let n = ref 1 in
672 673
  (* Create a page with tabname [f] and buffer equal to [content] in the
     notebook. Also add a corresponding page in source_view_table. *)
674 675 676
  let create_source_view f content =
    if not (Hstr.mem source_view_table f) then
      begin
MARCHE Claude's avatar
MARCHE Claude committed
677 678
        let label = GMisc.label ~text:(Filename.basename f) () in
        label#misc#set_tooltip_markup f;
679 680
        let source_page, scrolled_source_view =
          !n, GPack.vbox ~homogeneous:false ~packing:
681 682
            (fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
        in
683 684 685 686 687 688
        let scrolled_source_view =
          GBin.scrolled_window
            ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
            ~shadow_type:`ETCHED_OUT
            ~packing:scrolled_source_view#add () in
        let source_view =
689
          GSourceView.source_view
690
            ~auto_indent:gconfig.allow_source_editing
691 692 693 694
            ~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 *)
695
            ~editable:gconfig.allow_source_editing
696 697
            ~packing:scrolled_source_view#add
            () in
698 699
        let has_changed = ref false in
        Hstr.add source_view_table f (source_page, source_view, has_changed, label);
700
        n := !n + 1;
701
        source_view#source_buffer#begin_not_undoable_action ();
702
        source_view#source_buffer#set_text content;
703
        source_view#source_buffer#end_not_undoable_action ();
704 705 706 707 708 709 710 711 712 713 714
        (* At initialization, file has not changed. When it changes, changes the
           name of the tab and update has_changed boolean. *)
        let (_: GtkSignal.id) = source_view#source_buffer#connect#changed
          ~callback:(fun () ->
            try
              let _source_page, _source_view, has_changed, label =
                Hstr.find source_view_table f in
              update_label_change label;
              has_changed := true;
              ()
            with Not_found -> () ) in
715 716
        Gconfig.add_modifiable_mono_font_view source_view#misc;
        source_view#source_buffer#set_language why_lang;
717 718 719
        (* We have to create the tags for background colors for each view.
           They are not reusable from the other views.  *)
        create_colors source_view;
720 721 722
        Gconfig.set_fonts ()
      end in
  create_source_view
723 724 725



726 727
(* End of notebook *)

728 729 730 731 732
(*
  2.2.2.2 a vertical pan which contains [vbox2222]
    2.2.2.2.1 the input field to type commands [hbox22221]
    2.2.2.2.2 a scrolled window to hold the output of the commands [message_zone]
*)
Clément Fumex's avatar
Clément Fumex committed
733
let vbox2222 = GPack.vbox ~packing:vpan222#add  ()
734

735 736 737 738
(* 2.2.2.2.1 Horizontal box [hbox22221]
     [monitor] number of scheduled/running provers
     [command_entry] Commands to run on the session
*)
739 740 741 742 743 744
let hbox22221 =
  GPack.hbox
    ~packing:(vbox2222#pack ?from:None ?expand:None ?fill:None ?padding:None) ()

let monitor =
  GMisc.label
745
    ~text:"  0/0/0"
746
    ~width:100
747
    ~xalign:0.0
748
    ~packing:(hbox22221#pack ?from:None ?expand:None ?fill:None ?padding:None) ()
749

750 751 752 753
let command_entry =
  GEdit.entry
    ~text:"type commands here"
    ~packing:hbox22221#add ()
754

755 756 757 758 759 760 761 762
(* Part 2.2.2.2.2 contains messages returned by the IDE/server *)
let messages_notebook = GPack.notebook ~packing:vbox2222#add ()

let error_page,error_view =
  let label = GMisc.label ~text:"Messages" () in
  0, GPack.vbox ~homogeneous:false ~packing:
    (fun w -> ignore(messages_notebook#append_page ~tab_label:label#coerce w)) ()

Guillaume Melquiond's avatar
Guillaume Melquiond committed
763
let log_view =
764
  let label = GMisc.label ~text:"Log" () in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
765
  GPack.vbox ~homogeneous:false ~packing:
766 767 768
    (fun w -> ignore(messages_notebook#append_page ~tab_label:label#coerce w)) ()

(* tab 3: edited proof *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
769
let edited_tab =
770
  let label = GMisc.label ~text:"Edited proof" () in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
771
  GPack.vbox ~homogeneous:false ~packing:
772 773 774 775 776 777 778 779
    (fun w -> ignore(messages_notebook#append_page ~tab_label:label#coerce w)) ()

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

let edited_view =
780
  GSourceView.source_view
781 782 783 784 785 786
    ~editable:false
    ~show_line_numbers:true
    ~packing:scrolled_edited_view#add
    ()

(* tab 4: prover output *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
787
let output_tab =
788
  let label = GMisc.label ~text:"Prover output" () in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
789
  GPack.vbox ~homogeneous:false ~packing:
790 791 792 793 794 795 796 797
    (fun w -> ignore(messages_notebook#append_page ~tab_label:label#coerce w)) ()

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

let output_view =
798
  GSourceView.source_view
799 800 801 802 803 804 805 806 807 808
    ~editable:false
    ~show_line_numbers:true
    ~packing:scrolled_output_view#add
    ()


(* tab 5: counterexample *)
let counterexample_page,counterexample_tab =
  let label = GMisc.label ~text:"Counterexample" () in
  4, GPack.vbox ~homogeneous:false ~packing:
809 810
    (fun w -> ignore(messages_notebook#append_page ~tab_label:label#coerce w)) ()

811 812 813 814 815 816
let scrolled_counterexample_view =
  GBin.scrolled_window
    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
    ~shadow_type:`ETCHED_OUT ~packing:counterexample_tab#add ()

let counterexample_view =
817
  GSourceView.source_view
818 819 820 821 822
    ~editable:false
    ~show_line_numbers:true
    ~packing:scrolled_counterexample_view#add
    ()

823 824
(* Allow colors locations on counterexample view *)
let () = create_colors counterexample_view
825

826
let message_zone =
827 828
  let sv = GBin.scrolled_window
      ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
829 830 831 832 833 834 835 836 837
      ~shadow_type:`ETCHED_OUT ~packing:error_view#add ()
  in
  GText.view ~editable:false ~cursor_visible:false
    ~packing:sv#add ()

let log_zone =
  let sv = GBin.scrolled_window
      ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
      ~shadow_type:`ETCHED_OUT ~packing:log_view#add ()
838
  in
839
  GText.view ~editable:false ~cursor_visible:false
840 841
    ~packing:sv#add ()

842 843
(* Create a tag for errors in the message zone. *)
let message_zone_error_tag = message_zone#buffer#create_tag
844
  ~name:"error_tag" [`BACKGROUND gconfig.error_color_bg; `FOREGROUND gconfig.error_color]
845

846 847
(**** Message-zone printing functions *****)

MARCHE Claude's avatar
MARCHE Claude committed
848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867
let add_to_log =
  let old = ref None in
  fun notif_kind s ->
  let (_,_,_,n) as x =
    match !old with
    | Some(line,oldnotif_kind,olds,oldn)
         when notif_kind = oldnotif_kind && s = olds ->
       let start = log_zone#buffer#get_iter (`LINE line) in
       let stop = log_zone#buffer#end_iter in
       log_zone#buffer#delete ~start ~stop;
       (line,oldnotif_kind,olds,oldn+1)
    | _ ->
       let line = log_zone#buffer#line_count in
       (line,notif_kind,s,1)
  in
  old := Some x;
  log_zone#buffer#insert ("["^ notif_kind);
  if n>1 then
    log_zone#buffer#insert (" (repeated " ^ (string_of_int n) ^ " times)");
  log_zone#buffer#insert ("] " ^ s ^ "\n");
868 869
  log_zone#scroll_to_mark `INSERT

870 871
let clear_message_zone () =
  let buf = message_zone#buffer in
872
  buf#remove_tag_by_name "error_tag" ~start:buf#start_iter ~stop:buf#end_iter;
873 874
  buf#delete ~start:buf#start_iter ~stop:buf#end_iter

875
(* Function used to print stuff on the message_zone *)
MARCHE Claude's avatar
MARCHE Claude committed
876
let print_message ~kind ~notif_kind fmt =
877
  (* TODO: use kasprintf once OCaml 4.03 is used *)
878 879
  Format.kfprintf
    (fun _ -> let s = flush_str_formatter () in
MARCHE Claude's avatar
MARCHE Claude committed
880
              let s = try_convert s in
MARCHE Claude's avatar
MARCHE Claude committed
881
              add_to_log notif_kind s;
882
              let buf = message_zone#buffer in
MARCHE Claude's avatar
MARCHE Claude committed
883 884
              if kind>0 then
                begin
885 886 887
                  if Strings.ends_with notif_kind "error" ||
                     Strings.ends_with notif_kind "Error"
                  then
888
                    buf#insert ~tags:[message_zone_error_tag] (s ^ "\n")
889
                  else
890
                    buf#insert (s ^ "\n");
891
                  messages_notebook#goto_page error_page;
MARCHE Claude's avatar
MARCHE Claude committed
892
                end)
893 894 895
    str_formatter
    fmt

896 897 898 899 900 901 902
let display_warnings fmt warnings =
  let nwarn = ref 0 in
  try
    Queue.iter (fun (loc,msg) ->
      if !nwarn = 4 then begin
        Format.fprintf fmt "[%d more warnings. See stderr for details]@\n" (Queue.length warnings - !nwarn);
        raise Exit
903
      end;
904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919
      incr nwarn;
      match loc with
      | None ->
        Format.fprintf fmt "%s@\n@\n" msg
      | Some l ->
        (* scroll_to_loc ~color:error_tag ~yalign:0.5 loc; *)
        Format.fprintf fmt "%a: %s@\n@\n" Loc.gen_report_position l msg
    ) warnings;
  with Exit -> ()

let display_warnings () =
  if Queue.is_empty warnings then ()
  else begin
    print_message ~kind:1 ~notif_kind:"warning" "%a" display_warnings warnings;
    Queue.clear warnings;
  end
920

921 922 923 924
let print_message ~kind ~notif_kind fmt =
  display_warnings (); print_message ~kind ~notif_kind fmt


925

926

927
(**** Monitor *****)
Clément Fumex's avatar
Clément Fumex committed
928

929
let fan =
930
  let s = Bytes.of_string "\226\150\129" in
931
  let c = Char.code (Bytes.get s 2) in
932
  let a = Array.init 8 (fun i ->
933 934 935
    Bytes.set s 2 (Char.chr (c + i));
    Bytes.to_string s) in
  fun n ->
936 937 938
  let n = n mod 14 in
  let n = if n < 0 then n + 14 else n in
  let n = if n >= 8 then 14 - n else n in
939
  a.(n)
940 941 942 943 944 945

let update_monitor =
  let c = ref 0 in
  fun t s r ->
  reset_gc ();
  incr c;
946 947 948
  let f = if r = 0 then " " else fan !c in
  let text = Printf.sprintf "%s %d/%d/%d" f t s r in
  monitor#set_text text
Clément Fumex's avatar
Clément Fumex committed
949

950 951 952 953 954 955 956
(**********************)
(* Cursor positioning *)
(**********************)

(* Current position in the source files *)
let current_cursor_loc = ref None

957
let move_to_line ~yalign (v : GSourceView.source_view) line =
958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996
  let line = max 0 (line - 1) in
  let line = min line v#buffer#line_count in
  let it = v#buffer#get_iter (`LINE line) in
  v#buffer#place_cursor ~where:it;
  let mark = `MARK (v#buffer#create_mark it) in
  v#scroll_to_mark ~use_align:true ~yalign mark

(* Scroll to a specific locations *)
let scroll_to_loc ~force_tab_switch loc_of_goal =
  match loc_of_goal with
  | None -> ()
  | Some loc ->
    let f, l, _, _ = Loc.get loc in
    try
      let (n, v, _, _) = get_source_view_table f in
      if force_tab_switch then
        begin
          Debug.dprintf debug "tab switch to page %d@." n;
          notebook#goto_page n;
        end;
      move_to_line ~yalign:0.0 v l
    with Nosourceview f ->
      Debug.dprintf debug "scroll_to_loc: no source know for file %s@." f

(* Reposition the cursor to the place it was saved *)
let reposition_ide_cursor () =
  scroll_to_loc ~force_tab_switch:false !current_cursor_loc

(* Save the current location of the cursor to be reused after reload *)
let save_cursor_loc () =
  let n = notebook#current_page in
  let acc = ref None in
  Hstr.iter (fun k (x, v, _, _) -> if x = n then acc := Some (k, v)) source_view_table;
  match !acc with
  | None -> ()
  | Some (cur_file, view) ->
    (* Get current line *)
    let line = (view#buffer#get_iter_at_mark `INSERT)#line + 1 in
    current_cursor_loc := Some (Loc.user_position cur_file line 1 1)
997

998 999 1000
(******************)
(* Reload actions *)
(******************)
1001

1002 1003
let reload_unsafe () =
  save_cursor_loc (); clear_message_zone (); send_request Reload_req
1004 1005 1006

let save_and_reload () = save_sources (); reload_unsafe ()

1007 1008 1009 1010 1011 1012
(****************************)
(* command entry completion *)
(****************************)

let completion_cols = new GTree.column_list
let completion_col = completion_cols#add Gobject.Data.string
1013
let completion_desc = completion_cols#add Gobject.Data.string
1014 1015 1016
let completion_model = GTree.tree_store completion_cols

let command_entry_completion : GEdit.entry_completion =
1017
  GEdit.entry_completion ~model:completion_model ~minimum_key_length:2 ~entry:command_entry ()
1018

1019
let add_completion_entry (s,desc) =
1020
  let row = completion_model#append () in
1021
  completion_model#set ~row ~column:completion_col s;
1022
  completion_model#set ~row ~column:completion_desc desc
1023

1024 1025 1026
let match_function s iter =
  let candidate = completion_model#get ~row:iter ~column:completion_col in
  try
1027
    ignore (Str.search_forward (Str.regexp_string_case_fold s) candidate 0);
1028 1029 1030
    true
  with Not_found -> false

1031
(* see also init_completion below *)
1032

Sylvain Dailler's avatar
Sylvain Dailler committed
1033
(*********************)
1034
(* Terminal history  *)
Sylvain Dailler's avatar
Sylvain Dailler committed
1035 1036
(*********************)

1037
let list_commands = create_history()
Sylvain Dailler's avatar
Sylvain Dailler committed
1038 1039 1040

let _ =
  command_entry#event#connect#key_press
1041 1042 1043
    ~callback:(fun (ev: 'a Gdk.event) ->
      match GdkEvent.Key.keyval ev with
      | k when k = GdkKeysyms._Up -> (* Arrow up *)
1044 1045 1046 1047 1048
          let s = print_next_command list_commands in
          (match s with
          | None -> true
          | Some s ->
              (command_entry#set_text s; true))
1049
      | k when k = GdkKeysyms._Down -> (* Arrow down *)
1050 1051 1052 1053 1054
          let s = print_prev_command list_commands in
          (match s with
          | None -> true
          | Some s ->
              (command_entry#set_text s; true))
1055 1056 1057
      | k when k = GdkKeysyms._Escape ->
        goals_view#misc#grab_focus ();
        true
Sylvain Dailler's avatar
Sylvain Dailler committed
1058 1059 1060
      | _ -> false
      )

1061
let () = send_session_config_to_server ()
1062

1063 1064 1065 1066 1067 1068 1069 1070 1071
(********************)
(* Locations colors *)
(********************)

let convert_color (color: color): string =
  match color with
  | Neg_premise_color -> "neg_premise_tag"
  | Premise_color -> "premise_tag"
  | Goal_color -> "goal_tag"
1072
  | Error_color -> "error_tag"
1073
  | Error_line_color -> "error_line_tag"
1074

1075
let color_line ~color loc =
1076
  let color_line (v:GSourceView.source_view) ~color l =
1077 1078 1079 1080 1081 1082 1083 1084 1085
    let buf = v#buffer in
    let top = buf#start_iter in
    let start = top#forward_lines (l-1) in
    let stop = start#forward_lines 1 in
    buf#apply_tag_by_name ~start ~stop color
  in

  let f, l, _, _ = Loc.get loc in
  try
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1086
    let v = get_source_view f in
1087 1088 1089 1090 1091 1092 1093 1094
    let color = convert_color color in
    color_line ~color v l
  with
  | Nosourceview f ->
    (* If the file is not present do nothing *)
    print_message ~kind:0 ~notif_kind:"color_loc" "No source view for file %s" f;
    Debug.dprintf debug "color_loc: no source view for file %s@." f

1095 1096
(* Add a color tag on the right locations on the correct file.
   If the file was not open yet, nothing is done *)
1097
let color_loc ?(ce=false) ~color loc =
1098 1099 1100

  (* This apply a background [color] on a location given by its file view [v] line
     [l] beginning char [b] and end char [e]. *)
1101
  let color_loc (v:GSourceView.source_view) ~color l b e =
1102 1103 1104 1105 1106 1107 1108 1109
    let buf = v#buffer in
    let top = buf#start_iter in
    let start = top#forward_lines (l-1) in
    let start = start#forward_chars b in
    let stop = start#forward_chars (e-b) in
    buf#apply_tag_by_name ~start ~stop color
  in

1110 1111
  let f, l, b, e = Loc.get loc in
  try
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1112
    let v = if ce then counterexample_view else get_source_view f in
1113 1114 1115
    let color = convert_color color in
    color_loc ~color v l b e
  with
MARCHE Claude's avatar
MARCHE Claude committed
1116
  | Nosourceview f ->
1117
      (* If the file is not present do nothing *)
MARCHE Claude's avatar
MARCHE Claude committed
1118 1119
     print_message ~kind:0 ~notif_kind:"color_loc" "No source view for file %s" f;
     Debug.dprintf debug "color_loc: no source view for file %s@." f
1120 1121 1122 1123 1124 1125

(* Erase the colors and apply the colors given by l (which come from the task)
   to appropriate source files *)
let apply_loc_on_source (l: (Loc.position * color) list) =
  Hstr.iter (fun _ (_, v, _, _) -> erase_color_loc v) source_view_table;
  List.iter (fun (loc, color) ->
1126 1127 1128 1129 1130 1131 1132 1133
    color_loc ~color loc) l;
  let loc_of_goal =
    (* TODO the last location sent seems more relevant thus the rev. This
       should be changed, the sent task should contain the information of where
       to scroll and the list of locations is far too long. *)
    try Some (List.find (fun (_, color) -> color = Goal_color) (List.rev l))
    with Not_found -> None
  in
1134
  scroll_to_loc ~force_tab_switch:false (Opt.map fst loc_of_goal)
1135

1136 1137 1138 1139 1140 1141 1142
(* Erase the colors and apply the colors given by l (which come from the task)
   to the counterexample tab *)
let apply_loc_on_ce (l: (Loc.position * color) list) =
  erase_color_loc counterexample_view;
  List.iter (fun (loc, color) ->
    color_loc ~ce:true ~color loc) l

1143
let collapse_iter iter =
1144 1145 1146
  let path = goals_model#get_path iter in
  goals_view#collapse_row path

1147 1148 1149 1150 1151 1152 1153 1154 1155 1156
let rec collapse_proven_goals_from_iter iter =
  let node_id = get_node_id iter in
  let is_proved = get_node_proved node_id in
  if is_proved then
    collapse_iter iter
  else
    let n = goals_model#iter_n_children (Some iter) in
    for i = 0 to (n - 1) do
      collapse_proven_goals_from_iter (goals_model#iter_children ?nth:(Some i) (Some iter))
    done
1157 1158 1159 1160 1161 1162 1163 1164 1165 1166

let collapse_proven_goals () =
  match goals_model#get_iter_first with
  | None -> ()
  | Some root_iter -> collapse_proven_goals_from_iter root_iter

let () =
  Gconfig.add_modifiable_sans_font_view goals_view#misc;
  Gconfig.add_modifiable_mono_font_view monitor#misc;
  Gconfig.add_modifiable_mono_font_view task_view#misc;
1167 1168 1169
  Gconfig.add_modifiable_mono_font_view edited_view#misc;
  Gconfig.add_modifiable_mono_font_view output_view#misc;
  Gconfig.add_modifiable_mono_font_view counterexample_view#misc;
1170 1171
  Gconfig.add_modifiable_mono_font_view command_entry#misc;
  Gconfig.add_modifiable_mono_font_view message_zone#misc;
MARCHE Claude's avatar
MARCHE Claude committed
1172
  task_view#source_buffer#set_language why_lang;
1173
  counterexample_view#source_buffer#set_language why_lang;
Clément Fumex's avatar
Clément Fumex committed
1174
  Gconfig.set_fonts ()
1175

1176 1177 1178



1179 1180 1181 1182
(******************)
(*    actions     *)
(******************)

Clément Fumex's avatar
Clément Fumex committed
1183 1184 1185 1186
let get_selected_row_references () =
  List.map
    (fun path -> goals_model#get_row_reference path)
    goals_view#selection#get_selected_rows
1187

Sylvain Dailler's avatar
Sylvain Dailler committed
1188 1189 1190
(**********************)
(* Contextual actions *)
(**********************)
1191 1192 1193 1194 1195 1196 1197 1198 1199 1200

(* goals_view#selection#select_iter only changes the selection for the selection
   tree, it should also change the cursor of the goal_view. The reason is that
   the cursor is used for arrow keys moves (not the selected row). *)
let select_iter iter =
  goals_view#selection#select_iter iter;
  let path = goals_model#get_path iter in
  goals_view#set_cursor path view_name_column


1201
let expand_row () =
Sylvain Dailler's avatar
Sylvain Dailler committed
1202 1203 1204 1205
  let rows = get_selected_row_references () in
  match rows with
  | [row] ->
      let path = goals_model#get_path row#iter in
1206
      goals_view#expand_row path ~all:(goals_view#row_expanded path)
Sylvain Dailler's avatar
Sylvain Dailler committed
1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225
  | _ -> ()

let collapse_row () =
  let rows = get_selected_row_references () in
  match rows with
  | [row] ->
      let path = goals_model#get_path row#iter in
      goals_view#collapse_row path
  | _ -> ()

let move_current_row_selection_to_parent () =
  let rows = get_selected_row_references () in
  match rows with
  | [row] ->
      begin
        goals_view#selection#unselect_all ();
        match goals_model#iter_parent row#iter with
        | None -> ()
        | Some iter ->
1226
            select_iter iter
Sylvain Dailler's avatar
Sylvain Dailler committed
1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240
      end
  | _ -> ()

let move_current_row_selection_to_first_child () =
  let rows = get_selected_row_references () in
  match rows with
  | [row] ->
      let n = goals_model#iter_n_children (Some row#iter) in
      if n = 0 then
        ()
      else
        begin
          goals_view#selection#unselect_all ();
          let iter = goals_model#iter_children ?nth:(Some 0) (Some row#iter) in
1241
          select_iter iter
Sylvain Dailler's avatar
Sylvain Dailler committed
1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252
        end
  | _ -> ()

let move_to_next_unproven_node_id () =
  let rows = get_selected_row_references () in
  match rows with
  | [row] ->
      let row_id = get_node_id row#iter in
      send_request (Get_first_unproven_node row_id)
  | _ -> ()

1253
(* unused
1254
let rec update_status_column_from_iter cont iter =
Clément Fumex's avatar
Clément Fumex committed
1255
  set_status_column iter;
1256
  match goals_model#iter_parent iter with
1257
  | Some p -> update_status_column_from_iter cont p
1258
  | None -> ()
1259
*)
1260

1261
let clear_command_entry () = command_entry#set_text ""
1262

Sylvain Dailler's avatar
Sylvain Dailler committed
1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283
let ide_command_list =
  ["up", "Select the parent of the current node";
   "down", "Select the first child of the current node";
   "next", "Select the \"next\" unproved node";
   "expand", "Expand the node";
   "ex_all", "Expand the node recursively";
   "collapse", "Collapse the node";
   "list_ide_command", "show this help text"]

let ide_command cmd =
  List.exists (fun x -> fst x = cmd) ide_command_list

let interp_ide cmd =
  match cmd with
  | "up" ->
      move_current_row_selection_to_parent ()
  | "down" ->
      move_current_row_selection_to_first_child ()
  | "next" ->
      move_to_next_unproven_node_id ()
  | "expand" ->
1284
      expand_row ()
Sylvain Dailler's avatar
Sylvain Dailler committed
1285 1286 1287 1288 1289 1290
  | "collapse" ->
      collapse_row ()
  | "list_ide_command" ->
      let s = List.fold_left (fun acc x -> (fst x) ^ ": " ^
                              (snd x) ^ "\n" ^ acc) "" ide_command_list in
      clear_command_entry ();
1291
      print_message ~kind:1 ~notif_kind:"Info" "%s" s
Sylvain Dailler's avatar
Sylvain Dailler committed
1292 1293
  | _ ->
      clear_command_entry ();
1294
      print_message ~kind:1 ~notif_kind:"error" "Error: %s\nPlease report." cmd
Sylvain Dailler's avatar
Sylvain Dailler committed
1295

1296
let interp cmd =
Clément Fumex's avatar
Clément Fumex committed
1297
  (* TODO: do some preprocessing for queries, or leave everything to server ? *)
Sylvain Dailler's avatar
Sylvain Dailler committed
1298
  message_zone#buffer#set_text "";
MARCHE Claude's avatar
MARCHE Claude committed
1299
  clear_command_entry ();
Sylvain Dailler's avatar
Sylvain Dailler committed
1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312
  if ide_command cmd then
    interp_ide cmd
  else
    begin
      let rows = get_selected_row_references () in
      let ids =
        match rows with
        | [] -> [root_node]
        | _ -> List.map (fun n -> get_node_id n#iter) rows
      in
      List.iter (fun id -> send_request (Command_req (id, cmd))) ids;
      (* clear previous error message if any *)
    end
1313 1314

let (_ : GtkSignal.id) =
1315 1316
  let callback () =
    let cmd = command_entry#text in
Sylvain Dailler's avatar
Sylvain Dailler committed
1317 1318 1319 1320
    match cmd with
    | ""     -> goals_view#misc#grab_focus ()
    | _ ->
      begin
1321 1322 1323 1324
        add_command list_commands cmd;
        interp cmd
      end in
  command_entry#connect#activate ~callback
1325

1326 1327 1328 1329 1330 1331 1332 1333 1334
(* remove the helper text from the command entry the first time it gets the focus *)
let () =
  let id = ref None in
  let callback _ =
    clear_command_entry ();
    GtkSignal.disconnect command_entry#as_entry (Opt.get !id);
    false in
  id := Some (command_entry#event#connect#focus_in ~callback)

1335 1336
let on_selected_row r =
  try
Clément Fumex's avatar
Clément Fumex committed
1337 1338 1339 1340
    let id = get_node_id r#iter in
    let typ = get_node_type id in
    match typ with
    | NGoal ->
1341
        let c = gconfig.show_full_context in
1342
        send_request (Get_task(id,c,true))
1343
    | NProofAttempt ->
1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355
       let (pa, _obs, _l) = Hint.find node_id_pa id in
       let output_text =
         match pa with
         | Controller_itp.Done pr -> pr.Call_provers.pr_output
         | Controller_itp.Undone -> "no result known"
         | Controller_itp.Detached -> "detached proof attempt: parent goal has no task"
         | Controller_itp.Interrupted -> "prover run was interrupted"
         | Controller_itp.Scheduled -> "proof scheduled but not running yet"
         | Controller_itp.Running -> "prover currently running"
         | Controller_itp.InternalFailure e ->
            (Pp.sprintf "internal failure: %a" Exn_printer.exn_printer e)
         | Controller_itp.Uninstalled _p -> "uninstalled prover"
1356
         | Controller_itp.Removed _p -> "removed proof attempt"