diff --git a/src/ide/ide_main.ml b/src/ide/ide_main.ml deleted file mode 100644 index c27f471e5d20e0908b318a53b130739b098832f0..0000000000000000000000000000000000000000 --- a/src/ide/ide_main.ml +++ /dev/null @@ -1,221 +0,0 @@ -(**************************************************************************) -(* *) -(* Copyright (C) 2010- *) -(* François Bobot *) -(* Jean-Christophe Filliâtre *) -(* Claude Marché *) -(* Andrei Paskevich *) -(* *) -(* This software is free software; you can redistribute it and/or *) -(* modify it under the terms of the GNU Library General Public *) -(* License version 2.1, with the special exception on linking *) -(* described in file LICENSE. *) -(* *) -(* This software is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) -(* *) -(**************************************************************************) - -(* POUR L'INSTANT, CE NE SONT ICI QUE DES EXPÉRIENCES - MERCI DE NE PAS CONSIDÉRER CE CODE COMME DÉFINITIF - -- jcf -*) - -open Why -open Theory - -let () = ignore (GtkMain.Main.init ()) - -(* config *) -let window_width = 1024 -let window_height = 768 -let font_name = "Monospace 10" - -(* command line *) -let font_size = ref 10 -let font_family = "Monospace" - -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 -let loadpath = ref [] - -let spec = - [ - "-I", Arg.String (fun s -> loadpath := s :: !loadpath), - " Add 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 - -let lang = - let load_path = - List.fold_right Filename.concat - [Filename.dirname Sys.argv.(0); ".."; "share"] "lang" - in - let languages_manager = - GSourceView2.source_language_manager ~default:true - in - languages_manager#set_search_path - (load_path :: languages_manager#search_path); - match languages_manager#language "why" with - | None -> Format.eprintf "pas trouvé@;"; None - | Some _ as l -> l - -let 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 = Env.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 - model#set ~row ~column (th.th_name.Ident.id_string : string); - fill row th.th_export - -end - - -(* windows, etc *) - -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 - (* Replay *) - let button = - GButton.button ~label:"repousser le front d'obsolescence" - ~packing:top_box#add () - in - ignore (button#connect#clicked - ~callback:(fun () -> Format.printf "Andrei, tu es trop fort !@.")); - - (* 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; - - (* source view *) - let scrolled_win = GBin.scrolled_window - ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC - ~packing:hp#add () - in - let source_view = - GSourceView2.source_view - ~auto_indent:true - ~insert_spaces_instead_of_tabs:true ~tab_width:2 - ~show_line_numbers:true - ~right_margin_position:80 ~show_right_margin:true - (* ~smart_home_end:true *) - ~packing:scrolled_win#add ~height:500 ~width:650 - () - in - source_view#misc#modify_font_by_name font_name; - source_view#source_buffer#set_language lang; - source_view#set_highlight_current_line true; - source_view#source_buffer#set_text text; - - w#add_accel_group accel_group; - w#show () - -let () = - main (); - GtkThread.main () - -(* -Local Variables: -compile-command: "unset LANG; make -C ../.. bin/whyide.opt" -End: -*)