Skip to content

GitLab

why3
why3
Commit 212c6d7e authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

remove ide_main.ml, unused since ages

parent b37c8610
Hide whitespace changes
Inline Side-by-side
Showing with 0 additions and 221 deletions
src/ide/ide_main.ml deleted 100644 → 0
View file @ b37c8610
(**************************************************************************)
(* *)
(* 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 EXPRIENCES
MERCI DE NE PAS CONSIDRER CE CODE COMME DFINITIF
-- 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),
"<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
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:
*)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment