ide_main.ml 5.24 KB
Newer Older
1

2 3 4 5 6
(* POUR L'INSTANT, CE NE SONT ICI QUE DES EXPRIENCES 
   MERCI DE NE PAS CONSIDRER CE CODE COMME DFINITIF
   -- jcf
*)

7
open Why
8 9
open Theory

10 11 12 13 14
let () = ignore (GtkMain.Main.init ())

(* config *)
let window_width = 1024
let window_height = 768
15
let font_name = "Monospace 10"
16

17
(* command line *)
18 19 20
let font_size = ref 10
let font_family = "Monospace"

21 22 23 24 25 26 27 28 29 30 31
let file = ref None
let set_file f = match !file with
  | Some _ -> 
      raise (Arg.Bad "only one file, please")
  | 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 "why-ide: %s: no such file@." f; exit 1
      end;
      file := Some f
32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
let loadpath = ref []

let spec = 
  [
    "-I", Arg.String (fun s -> loadpath := s :: !loadpath), 
    "<dir> Add <dir> to the library search path";
  ]
let usage_str = "why-ide [options] file.why"
let () = Arg.parse spec set_file usage_str

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

48
let lang =
49
  let load_path = 
50
    List.fold_right Filename.concat 
51
      [Filename.dirname Sys.argv.(0); ".."; "share"] "lang" 
52
  in
53 54 55 56 57 58 59 60
  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
61

62 63 64 65 66 67 68 69 70 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 117 118 119 120
let 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

let env = Env.create_env (Typing.retrieve !loadpath)

let theories = 
  let cin = open_in fname in
  let m = Typing.read_channel env fname cin in
  close_in cin;
  m

(* namespace widget *)
module Ide_namespace = struct

  let cols = new GTree.column_list
  let column = cols#add Gobject.Data.string

  let renderer = GTree.cell_renderer_text [`XALIGN 0.] 
  let vcolumn = 
    GTree.view_column ~title:"theories" 
      ~renderer:(renderer, ["text", column]) () 

  let () = 
    vcolumn#set_resizable true;
    vcolumn#set_max_width 400

  let create ~packing () =
    let model = GTree.tree_store cols in
    let view = GTree.view ~model ~packing () in
    let _ = view#selection#set_mode `SINGLE in
    let _ = view#set_rules_hint true in
    ignore (view#append_column vcolumn);
    model

  let clear model = 
    model#clear ()

  let add_theory (model : GTree.tree_store) th =
    let rec fill parent ns =
      let add_s k s _ = 
	let row = model#append ~parent () in
	model#set ~row ~column (k ^ s)
      in
      Mnm.iter (add_s "type ")  ns.ns_ts;
      Mnm.iter (add_s "logic ") ns.ns_ls;
      Mnm.iter (add_s "prop ")  ns.ns_pr;
      let add_ns s ns =
	let row = model#append ~parent () in
	model#set ~row ~column s;
	fill row ns
      in
      Mnm.iter add_ns ns.ns_ns
    in
    let row = model#append () in
121
    model#set ~row ~column (th.th_name.Ident.id_string : string);
122 123 124
    fill row th.th_export

end
125 126 127


(* windows, etc *)
128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150

let main () =
  let w = GWindow.window 
    ~allow_grow:true ~allow_shrink:true
    ~width:window_width ~height:window_height 
    ~title:"why-ide" ()
  in
  let _ = w#connect#destroy ~callback:(fun () -> exit 0) in
  let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in

  (* Menu *)
  let menubar = GMenu.menu_bar ~packing:vbox#pack () in
  let factory = new GMenu.factory menubar in
  let accel_group = factory#accel_group in
  let file_menu = factory#add_submenu "_File" in
  let file_factory = new GMenu.factory file_menu ~accel_group in
  let _ = 
    file_factory#add_image_item ~key:GdkKeysyms._Q ~label:"_Quit" 
      ~callback:(fun () -> exit 0) () 
  in

  (* top line *)
  let top_box = GPack.hbox ~packing:vbox#pack () in
151
  (* Replay *)
152 153
  let button = 
    GButton.button ~label:"repousser le front d'obsolescence" 
154
      ~packing:top_box#add ()
155 156 157 158
  in
  ignore (button#connect#clicked
	    (fun () -> Format.printf "Andrei, tu es trop fort !@."));

159 160 161 162 163 164 165 166 167 168 169 170 171
  (* horizontal paned *)
  let hp = GPack.paned `HORIZONTAL  ~border_width:3 ~packing:vbox#add () in

  (* left tree of namespace *)
  let scrollview = 
    GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC 
    ~width:(window_width / 3) ~packing:hp#add () 
  in
  let _ = scrollview#set_shadow_type `ETCHED_OUT in

  let namespace_view = Ide_namespace.create ~packing:scrollview#add () in
  Mnm.iter (fun _ th -> Ide_namespace.add_theory namespace_view th) theories;

172 173 174
  (* source view *)
  let scrolled_win = GBin.scrolled_window
    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
175
    ~packing:hp#add ()
176 177
  in
  let source_view =
178
    GSourceView2.source_view
179
      ~auto_indent:true
180
      ~insert_spaces_instead_of_tabs:true ~tab_width:2
181
      ~show_line_numbers:true
182 183
      ~right_margin_position:80 ~show_right_margin:true
      (* ~smart_home_end:true *)
184 185 186 187
      ~packing:scrolled_win#add ~height:500 ~width:650
      ()
  in
  source_view#misc#modify_font_by_name font_name;
188 189
  source_view#source_buffer#set_language lang;
  source_view#set_highlight_current_line true;
190
  source_view#source_buffer#set_text text;
191
 
192 193 194 195 196 197 198 199 200
  w#add_accel_group accel_group;
  w#show ()

let () =
  main ();
  GtkThread.main ()

(*
Local Variables: 
201
compile-command: "unset LANG; make -C ../.. ide-opt-yes"
202 203
End: 
*)