<commit_before>(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    <NAME>                                                      *)
(*    <NAME>                                           *)
(*    <NAME>                                                      *)
(*    <NAME>                                                    *)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)


(* TODO:

* bug: the file names are stored as relative, so if you restart
from another directory, they are not found
  but on the other hand, storing them as relative helps if you change the machine
  Solution: store the name relative to the database, e.g if

  dir/file.why
  dir/T/project.db

  then project.db should store "../file.why", and running the interface
  from any dir as

  > why3db foo/dir/T

  should read the file by concating foo/dir to ../file.why

* When DB contains an edited proof, use the file for the run

* when proof attempt is finished and is it the one currently selected,
the new output should be displayed on upper-right window

* when returning from edited proofs: should we run the prover again immediately ?

* bug trouve par Johannes:

Pour reproduire le bug :

1) Partir d'un répértoire sans fichier de projet
2) Lancer why3db, ajouter un fichier
3) Prouver quelques buts (pas tous)
4) Choisir "Hide Proved Goals"
5) Prouver le reste des buts, la fênetre devient vide
6) Décocher "Hide Proved Goals"

Maintenant, le fichier réapparait dans la liste, mais on ne peut pas le
déplier, donc accéder au sous-buts, stats des appels de prouvers etc ...

Ce n'est pas un bug très grave, parce qu'il suffit de quitter l'ide,
puis le relancer, et là on peut de nouveau déplier le fichier.

* Francois :

   - Les temps indiqués sont très bizarre, mais cela doit-être un bug
   plus profond, au niveau de l'appel des prouveurs (wall time au lieu
   de cpu time?)

   - Si on modifie le fichier à droite, les buts ne sont pas marqués
   obsolètes ou ajouté à gauche.

*)



open Format

let () = 
  eprintf "Init the GTK interface...@?";
  ignore (GtkMain.Main.init ());
  eprintf " done.@."


open Why
open Whyconf
open Gconfig


(************************)
(* parsing command line *)
(************************)

let includes = ref []
let file = ref None

let spec = Arg.align [
  ("-I",
   Arg.String (fun s -> includes := s :: !includes),
   "<s> add s to loadpath") ;
(*
  ("-f",
   Arg.String (fun s -> input_files := s :: !input_files),
   "<f> add file f to the project (ignored if it is already there)") ;
*)
]

let usage_str = "whydb [options] [<file.why>|<project directory>]"
let set_file f = match !file with
  | Some _ ->
      raise (Arg.Bad "only one parameter")
  | None ->
      file := Some f

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 main = get_main () in
  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);
  match languages_manager#language "why" with
    | None ->
        Format.eprintf "language file for 'why' not found in directory %s@."
          load_path;
        exit 1
    | Some _ as l -> l

let source_text fname =
  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

(********************************)
(* loading WhyIDE configuration *)
(********************************)

let gconfig =
  let c = Gconfig.config in
  let loadpath = (Whyconf.loadpath (get_main ())) @ List.rev !includes in
  c.env <- Env.create_env (Lexer.retrieve loadpath);
  let provers = Whyconf.get_provers c.Gconfig.config in
  c.provers <-
    Util.Mstr.fold (Gconfig.get_prover_data c.env) provers Util.Mstr.empty;
  c


(********************)
(* opening database *)
(********************)

let project_dir, file_to_read =
  if Sys.file_exists fname then
    begin
      if Sys.is_directory fname then
        begin
          eprintf "Info: found directory '%s' for the project@." fname;
          fname, None
        end
      else
        begin
          eprintf "Info: found regular file '%s'@." fname;
          let d = 
            try Filename.chop_extension fname<commit_msg>Plugin : loaded in ide<commit_after>(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    <NAME>                                                      *)
(*    <NAME>                                           *)
(*    <NAME>                                                      *)
(*    <NAME>                                                    *)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)


(* TODO:

* bug: the file names are stored as relative, so if you restart
from another directory, they are not found
  but on the other hand, storing them as relative helps if you change the machine
  Solution: store the name relative to the database, e.g if

  dir/file.why
  dir/T/project.db

  then project.db should store "../file.why", and running the interface
  from any dir as

  > why3db foo/dir/T

  should read the file by concating foo/dir to ../file.why

* When DB contains an edited proof, use the file for the run

* when proof attempt is finished and is it the one currently selected,
the new output should be displayed on upper-right window

* when returning from edited proofs: should we run the prover again immediately ?

* bug trouve par Johannes:

Pour reproduire le bug :

1) Partir d'un répértoire sans fichier de projet
2) Lancer why3db, ajouter un fichier
3) Prouver quelques buts (pas tous)
4) Choisir "Hide Proved Goals"
5) Prouver le reste des buts, la fênetre devient vide
6) Décocher "Hide Proved Goals"

Maintenant, le fichier réapparait dans la liste, mais on ne peut pas le
déplier, donc accéder au sous-buts, stats des appels de prouvers etc ...

Ce n'est pas un bug très grave, parce qu'il suffit de quitter l'ide,
puis le relancer, et là on peut de nouveau déplier le fichier.

* Francois :

   - Les temps indiqués sont très bizarre, mais cela doit-être un bug
   plus profond, au niveau de l'appel des prouveurs (wall time au lieu
   de cpu time?)

   - Si on modifie le fichier à droite, les buts ne sont pas marqués
   obsolètes ou ajouté à gauche.

*)



open Format

let () = 
  eprintf "Init the GTK interface...@?";
  ignore (GtkMain.Main.init ());
  eprintf " done.@."


open Why
open Whyconf
open Gconfig


(************************)
(* parsing command line *)
(************************)

let includes = ref []
let file = ref None

let spec = Arg.align [
  ("-I",
   Arg.String (fun s -> includes := s :: !includes),
   "<s> add s to loadpath") ;
(*
  ("-f",
   Arg.String (fun s -> input_files := s :: !input_files),
   "<f> add file f to the project (ignored if it is already there)") ;
*)
]

let usage_str = "whydb [options] [<file.why>|<project directory>]"
let set_file f = match !file with
  | Some _ ->
      raise (Arg.Bad "only one parameter")
  | None ->
      file := Some f

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 main = get_main () in
  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);
  match languages_manager#language "why" with
    | None ->
        Format.eprintf "language file for 'why' not found in directory %s@."
          load_path;
        exit 1
    | Some _ as l -> l

let source_text fname =
  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

(********************************)
(* loading WhyIDE configuration *)
(********************************)

let gconfig =
  let c = Gconfig.config in
  let loadpath = (Whyconf.loadpath (get_main ())) @ List.rev !includes in
  c.env <- Env.create_env (Lexer.retrieve loadpath);
  let provers = Whyconf.get_provers c.Gconfig.config in
  c.provers <-
    Util.Mstr.fold (Gconfig.get_prover_data c.env) provers Util.Mstr.empty;
  c

let () =
  Whyconf.load_plugins (get_main ())


(********************)
(* opening database *)
(********************)

let project_dir, file_to_read =
  if Sys.file_exists fname then
    begin
      if Sys.is_directory fname then
        begin
          eprintf "Info: found directory '%s' for the project@." fname;
          fname, None
        end
      else
        begin
          eprintf "Info: found regular file '%s'@." fname;
          let d = 
            try Filename.chop_extension fname
{'fraction_non_alphanumeric': 0.13665803108808292, 'fraction_numerical': 0.0033308660251665434, 'mean_word_length': 2.092703862660944, 'pattern_counts': {'":': 0, '<': 23, '<?xml version=': 0, '>': 37, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 48, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '182996', 'n_tokens_mistral': 2998, 'n_tokens_neox': 2925, 'n_words': 1155}