Commit 47613a39 authored by MARCHE Claude's avatar MARCHE Claude

d

parent 10807078
......@@ -378,7 +378,7 @@ install_no_local::
# IDE
###############
IDE_FILES = gconfig scheduler db gmain
IDE_FILES = gconfig scheduler gmain
IDEMODULES = $(addprefix src/ide/, $(IDE_FILES))
......@@ -387,18 +387,18 @@ IDEMLI = $(addsuffix .mli, $(IDEMODULES))
IDECMO = $(addsuffix .cmo, $(IDEMODULES))
IDECMX = $(addsuffix .cmx, $(IDEMODULES))
$(IDECMO) $(IDECMX): INCLUDES += -I src/ide -I +sqlite3
$(IDECMO) $(IDECMX): INCLUDES += -I src/ide
# build targets
ifeq (@enable_ide@,yes)
byte: bin/whyide.byte
opt: bin/whyide.opt
byte: bin/whyide.byte
opt: bin/whyide.opt
endif
bin/whyide.opt bin/whyide.byte: INCLUDES += -thread -I +threads -I +lablgtk2 -I +sqlite3
bin/whyide.opt bin/whyide.byte: INCLUDES += -thread -I +threads -I +lablgtk2
bin/whyide.opt bin/whyide.byte: EXTOBJS += gtkThread
bin/whyide.opt bin/whyide.byte: EXTLIBS += threads lablgtk lablgtksourceview2 sqlite3
bin/whyide.opt bin/whyide.byte: EXTLIBS += threads lablgtk lablgtksourceview2
bin/whyide.opt: src/why.cmxa $(PGMCMX) $(IDECMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
......@@ -427,6 +427,60 @@ clean::
install_no_local::
cp -f bin/whyide.@OCAMLBEST@ $(BINDIR)/why3ide
###############
# IDE WITH DB
###############
DB_FILES = gconfig scheduler db gdbmain
DBMODULES = $(addprefix src/ide/, $(DB_FILES))
DBML = $(addsuffix .ml, $(DBMODULES))
DBMLI = $(addsuffix .mli, $(DBMODULES))
DBCMO = $(addsuffix .cmo, $(DBMODULES))
DBCMX = $(addsuffix .cmx, $(DBMODULES))
$(DBCMO) $(DBCMX): INCLUDES += -I src/ide -I +sqlite3
# build targets
ifeq (@enable_ide@,yes)
byte: bin/whydb.byte
opt: bin/whydb.opt
endif
bin/whydb.opt bin/whydb.byte: INCLUDES += -thread -I +threads -I +lablgtk2 -I +sqlite3
bin/whydb.opt bin/whydb.byte: EXTOBJS += gtkThread
bin/whydb.opt bin/whydb.byte: EXTLIBS += threads lablgtk lablgtksourceview2 sqlite3
bin/whydb.opt: src/why.cmxa $(PGMCMX) $(DBCMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
bin/whydb.byte: src/why.cma $(PGMCMO) $(DBCMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
# depend and clean targets
include .depend.db
.depend.db:
$(OCAMLDEP) -slash -I src -I src/ide $(DBML) $(DBMLI) > $@
depend: .depend.db
clean::
rm -f src/ide/*.cm[iox] src/ide/*.o
rm -f src/ide/*.annot src/ide/*~
rm -f bin/whydb.byte bin/whydb.opt
rm -f .depend.db
install_no_local::
cp -f bin/whydb.@OCAMLBEST@ $(BINDIR)/why3db
##############
# Coq plugin
##############
......
......@@ -245,10 +245,7 @@ let theory_name _ = assert false
let goals _ = assert false
let verified _ = assert false
let init_base _ = assert false
let files _ = assert false
type file
type file = int64
let file_name _ = assert false
let theories _ = assert false
......@@ -1022,27 +1019,35 @@ end
*)
(*
module Main = struct
let init db =
let sql = "CREATE TABLE IF NOT EXISTS rootgoals (goal_id INTEGER);" in
let sql = "CREATE TABLE IF NOT EXISTS files (file_name TEXT);" in
db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql);
()
let all_root_goals db =
let sql="SELECT goal_id FROM rootgoals" in
let all_files db =
let sql="SELECT file_name FROM files" in
let stmt = Sqlite3.prepare db.raw_db sql in
let of_stmt stmt = stmt_column_INT stmt 0 "Db.all_root_goals" in
let goals_ids = step_fold db stmt of_stmt in
goals_ids
let of_stmt stmt = stmt_column_string stmt 0 "Db.all_files" in
step_fold db stmt of_stmt
let add db name =
transaction db
(fun () ->
let sql = "INSERT INTO files VALUES(?)" in
let stmt = bind db sql [ Sqlite3.Data.TEXT name ] in
db_must_done db (fun () -> Sqlite3.step stmt);
let new_id = Sqlite3.last_insert_rowid db.raw_db in
new_id
(*
{ prover_id = Int64.to_int new_id ;
prover_name = name }
*)
)
end
*)
(*
let init_db ?(busyfn=default_busyfn) ?(mode=Immediate) db_name =
match !current_db with
| None ->
......@@ -1055,18 +1060,20 @@ let init_db ?(busyfn=default_busyfn) ?(mode=Immediate) db_name =
in
current_db := Some db;
ProverId.init db;
(*
Loc.init db;
External_proof.init db;
Goal.init db;
(*
Transf.init db;
*)
Main.init db
| Some _ -> failwith "Db.init_db: already opened"
let init_base f = init_db ~mode:Exclusive f
(*
let root_goals () =
let db = current () in
let l = Main.all_root_goals db in
......@@ -1074,6 +1081,8 @@ let root_goals () =
*)
let files _ = assert false
let prover_from_name n =
......@@ -1094,11 +1103,12 @@ let set_edited_as _ = assert false
let add_transformation _ = assert false
let add_goal _ = assert false
let add_theory _ = assert false
let add_file _ = assert false
let add_file f = Main.add (current()) f
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/whyide.byte"
compile-command: "unset LANG; make -C ../.. bin/whydb.byte"
End:
*)
......@@ -181,7 +181,7 @@ val add_theory : file -> string -> string -> unit
(** {3 files} *)
val add_file : string -> file
val add_file : string -> file
(** adds a file to the database.
@raise AlreadyExist if a file with the same id already exists *)
......
......@@ -25,9 +25,9 @@ open Whyconf
open Gconfig
(***************************)
(* parsing comand_line *)
(***************************)
(************************)
(* parsing command line *)
(************************)
let includes = ref []
......
......@@ -76,4 +76,4 @@ theory TestList
| Cons _ _ -> 8 = 9 /\ 10 = 11
end
end
\ No newline at end of file
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