Skip to content

why3
why3
Commit 71306d39 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

add copyrights of Guillaume, Johannes, and Simon where relevant

parent 595cb370
Hide whitespace changes
Inline Side-by-side
Showing with 100 additions and 19 deletions
ROADMAP
View file @ 71306d39
......@@ -54,12 +54,6 @@
* increment the magic number in config (A)
* enlever les caracteres de tab des sources
et les caracteres latin1 (A)
* faire tourner headache pour refabriquer les headers (A)
** dans gappa.ml : ajouter Guillaume en dessous de l'entete
* remettre le use_api dans la doc (C)
* deplacer le bouton "Cancel" dans le menu "tools",
......@@ -76,6 +70,12 @@
* distribute bench files (A + F)
* DONE enlever les caracteres de tab des sources
et les caracteres latin1 (A)
* DONE faire tourner headache pour refabriquer les headers (A)
** dans gappa.ml : ajouter Guillaume en dessous de l'entete
* DONE Rendre optionnel la question "would you like to save the session ?"
(C) -> 3-state options (Yes/No/ask) dans la config
+ DONE dans le menu "file" : "save session" sans raccourci clavier
......
misc/headache.sh
View file @ 71306d39
#!/bin/sh
headache -c misc/headache_config.txt -h misc/header.txt "$@"
headache -c misc/headache_config.txt -h misc/header_gm.txt \
src/transform/abstraction.ml* \
src/transform/simplify_formula.ml* \
src/printer/gappa.ml*
headache -c misc/headache_config.txt -h misc/header_jk.txt \
src/transform/close_epsilon.ml* \
src/transform/lift_epsilon.ml*
headache -c misc/headache_config.txt -h misc/header_sc.txt \
src/transform/hypothesis_selection.ml* \
src/tptp2why/*.ml*
sed -i -e '
s/Francois Bobot/François Bobot/g;
s/Jean-Christophe Filliatre/Jean-Christophe Filliâtre/g;
......
misc/header_gm.txt 0 → 100644
View file @ 71306d39
Copyright (C) 2010-2011
Francois Bobot
Jean-Christophe Filliatre
Claude Marche
Guillaume Melquiond
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.
misc/header_jk.txt 0 → 100644
View file @ 71306d39
Copyright (C) 2010-2011
Francois Bobot
Jean-Christophe Filliatre
Johannes Kanig
Claude Marche
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.
misc/header_sc.txt 0 → 100644
View file @ 71306d39
Copyright (C) 2010-2011
Francois Bobot
Simon Cruanes
Jean-Christophe Filliatre
Claude Marche
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.
src/ide/gconfig.ml
View file @ 71306d39
......@@ -404,24 +404,24 @@ let preferences c =
(fun w -> ignore(notebook#append_page ~tab_label:label3#coerce w)) ()
in
(* session saving policy *)
let choice0 =
GButton.radio_button
let choice0 =
GButton.radio_button
~label:"Always save on exit"
~active:(c.saving_policy = 0)
~packing:page3#add ()
in
let choice1 =
GButton.radio_button
~packing:page3#add ()
in
let choice1 =
GButton.radio_button
~label:"Never save on exit" ~group:choice0#group
~active:(c.saving_policy = 1)
~packing:page3#add ()
in
let choice2 =
GButton.radio_button
~packing:page3#add ()
in
let choice2 =
GButton.radio_button
~label:"ask whether to save on exit" ~group:choice0#group
~active:(c.saving_policy = 2)
~packing:page3#add ()
in
~packing:page3#add ()
in
let (_ : GtkSignal.id) =
choice0#connect#toggled ~callback:(set_saving_policy 0)
in
......
src/ide/newmain.ml
View file @ 71306d39
......@@ -772,7 +772,7 @@ let exit_function () =
)
in
()
| _ ->
| _ ->
eprintf "unexpected value for saving_policy@.";
GMain.quit ()
......
src/printer/gappa.ml
View file @ 71306d39
......@@ -4,6 +4,7 @@
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
......
src/tptp2why/tptp2whymain.ml
View file @ 71306d39
......@@ -2,6 +2,7 @@
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Simon Cruanes *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
......
src/tptp2why/tptpLexer.mll
View file @ 71306d39
......@@ -2,6 +2,7 @@
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Simon Cruanes *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
......
src/tptp2why/tptpParser.mly
View file @ 71306d39
......@@ -2,6 +2,7 @@
/* */
/* Copyright (C) 2010-2011 */
/* François Bobot */
/* Simon Cruanes */
/* Jean-Christophe Filliâtre */
/* Claude Marché */
/* Andrei Paskevich */
......
src/tptp2why/tptpTranslate.ml
View file @ 71306d39
......@@ -2,6 +2,7 @@
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Simon Cruanes *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
......
src/tptp2why/tptpTranslate.mli
View file @ 71306d39
......@@ -2,6 +2,7 @@
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Simon Cruanes *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
......
src/tptp2why/tptpTree.ml
View file @ 71306d39
......@@ -2,6 +2,7 @@
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Simon Cruanes *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
......
src/transform/abstraction.ml
View file @ 71306d39
......@@ -4,6 +4,7 @@
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
......
src/transform/abstraction.mli
View file @ 71306d39
......@@ -4,6 +4,7 @@
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
......
src/transform/close_epsilon.ml
View file @ 71306d39
......@@ -3,6 +3,7 @@
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Johannes Kanig *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
......
src/transform/close_epsilon.mli
View file @ 71306d39
......@@ -3,6 +3,7 @@
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Johannes Kanig *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
......
src/transform/hypothesis_selection.ml
View file @ 71306d39
......@@ -2,6 +2,7 @@
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Simon Cruanes *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
......
src/transform/lift_epsilon.ml
View file @ 71306d39
......@@ -3,6 +3,7 @@
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Johannes Kanig *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
......
src/transform/lift_epsilon.mli
View file @ 71306d39
......@@ -3,6 +3,7 @@
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Johannes Kanig *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
......
src/transform/simplify_formula.ml
View file @ 71306d39
......@@ -4,6 +4,7 @@
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
......
src/transform/simplify_formula.mli
View file @ 71306d39
......@@ -4,6 +4,7 @@
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
......
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