Commit 6c95e9a5 authored by Bruno Guillaume's avatar Bruno Guillaume

version 0.46.0:

 * Remove GUI (now available in a different opam package `grew_gui`)
 * New command line parsing of arguments, see `grew help`
parent 092cc9de
# 0.46.0 (2017/12/14)
* Remove GUI (now available in a different opam package `grew_gui`)
* New command line parsing of arguments, see `grew help`
## 0.45.1 (2017/12/07)
Bugfix: [#3](https://gitlab.inria.fr/grew/grew/issues/3) (Bug in GUI with graphviz 2.40)
......
PREFIX?=/usr/local
BINDIR=$(PREFIX)/bin
DATA_DIR=$(PREFIX)/share/grew/
OCB_FLAGS = -use-ocamlfind -I src
OCB = ocamlbuild $(OCB_FLAGS)
......@@ -9,34 +8,19 @@ VERSION = `cat VERSION`
all: native
native: src/grew_glade.ml datadir
native:
$(OCB) -tag-line "true: package(libgrew)" grew_main.native
datadir:
echo $(DATA_DIR) > DATA_DIR
install:
cp grew_main.native $(BINDIR)/grew
mkdir -p $(DATA_DIR)
cp src/grew.glade $(DATA_DIR)
uninstall:
rm -f $(BINDIR)/grew
rm -f $(DATA_DIR)/grew.glade
.PHONY: all clean byte native install uninstall
clean:
$(OCB) -clean
rm -f DATA_DIR
rm -f src/grew_glade.ml
info:
@echo "BINDIR = $(BINDIR)"
@echo "DATA_DIR = $(DATA_DIR)"
# glade file are not handle by ocamlbuild
src/grew_glade.ml : src/grew.glade
lablgladecc2 $< > $@
sed -iback 's|src/grew.glade|$(DATA_DIR)grew.glade|g' src/grew_glade.ml
rm -f src/grew_glade.mlback
@echo "BINDIR = $(BINDIR)"
true: package(yojson, containers, str, ANSITerminal, camomile, cairo2, log, svg, conll, dep2pict, lablgtk2, lablgtk2.rsvg, lablgtk2.glade, lablwebkit)
true: package(yojson, containers, str, ANSITerminal, camomile, cairo2, log, svg, conll, dep2pict)
true: bin_annot
\ No newline at end of file
......@@ -11,12 +11,7 @@ remove: [
]
depends: [
"cppo"
"lablgtk"
"lablwebkit" {= "1.8.2.1"}
"cairo2"
"ANSITerminal"
"libcaml-log"
"camomile"
"libcaml-dep2pict"
"libcaml-grew"
]
<?xml version="1.0" encoding="UTF-8"?>
<glade-interface>
<!-- interface-requires gtk+ 2.16 -->
<!-- interface-naming-policy project-wide -->
<widget class="GtkWindow" id="config_window">
<property name="can_focus">False</property>
<child>
<widget class="GtkVBox" id="config_vbox">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<widget class="GtkHBox" id="hbox20">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<widget class="GtkLabel" id="label4">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="xalign">0.89999997615814209</property>
<property name="xpad">3</property>
<property name="label" translatable="yes">&lt;b&gt; Main feat : &lt;/b&gt;</property>
<property name="use_markup">True</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">0</property>
</packing>
</child>
<child>
<widget class="GtkEntry" id="main_feat">
<property name="width_request">85</property>
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="invisible_char"></property>
<property name="invisible_char_set">True</property>
<property name="primary_icon_activatable">False</property>
<property name="secondary_icon_activatable">False</property>
<property name="primary_icon_sensitive">True</property>
<property name="secondary_icon_sensitive">True</property>
</widget>
<packing>
<property name="expand">True</property>
<property name="fill">True</property>
<property name="position">1</property>
</packing>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">0</property>
</packing>
</child>
<child>
<widget class="GtkLabel" id="label_features">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="label" translatable="yes">Features to display:</property>
<property name="ellipsize">end</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">1</property>
</packing>
</child>
<child>
<placeholder/>
</child>
<child>
<widget class="GtkButton" id="btn_config_close">
<property name="label">gtk-close</property>
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="receives_default">True</property>
<property name="use_stock">True</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="pack_type">end</property>
<property name="position">3</property>
</packing>
</child>
</widget>
</child>
</widget>
<widget class="GtkWindow" id="grew_window">
<property name="width_request">1024</property>
<property name="height_request">768</property>
<property name="can_focus">False</property>
<property name="window_position">center</property>
<property name="default_width">1024</property>
<property name="default_height">768</property>
<child>
<widget class="GtkVBox" id="vbox1">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<widget class="GtkHBox" id="hbox3">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<widget class="GtkLabel" id="label_20">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="xalign">0.89999997615814209</property>
<property name="label" translatable="yes">&lt;b&gt;Corpus:&lt;/b&gt;</property>
<property name="use_markup">True</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="padding">3</property>
<property name="position">0</property>
</packing>
</child>
<child>
<widget class="GtkButton" id="graph_button">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="receives_default">True</property>
<child>
<widget class="GtkHBox" id="hbox19">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<widget class="GtkLabel" id="graph_label">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="xpad">3</property>
<property name="label" translatable="yes">No corpus loaded</property>
</widget>
<packing>
<property name="expand">True</property>
<property name="fill">True</property>
<property name="position">0</property>
</packing>
</child>
<child>
<widget class="GtkImage" id="image6">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="stock">gtk-open</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">1</property>
</packing>
</child>
</widget>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">1</property>
</packing>
</child>
<child>
<widget class="GtkButton" id="btn_refresh_gr">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="receives_default">True</property>
<property name="relief">none</property>
<child>
<widget class="GtkImage" id="image2">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="stock">gtk-refresh</property>
</widget>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">2</property>
</packing>
</child>
<child>
<widget class="GtkVSeparator" id="vseparator4">
<property name="visible">True</property>
<property name="can_focus">False</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="padding">5</property>
<property name="position">3</property>
</packing>
</child>
<child>
<widget class="GtkLabel" id="label2">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="xalign">0.89999997615814209</property>
<property name="xpad">3</property>
<property name="label" translatable="yes">&lt;b&gt;GRS:&lt;/b&gt;</property>
<property name="use_markup">True</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="padding">3</property>
<property name="position">4</property>
</packing>
</child>
<child>
<widget class="GtkButton" id="grs_button">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="receives_default">True</property>
<child>
<widget class="GtkHBox" id="hbox21">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<widget class="GtkLabel" id="grs_label">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="label" translatable="yes">No GRS loaded</property>
</widget>
<packing>
<property name="expand">True</property>
<property name="fill">True</property>
<property name="position">0</property>
</packing>
</child>
<child>
<widget class="GtkImage" id="image7">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="stock">gtk-open</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">1</property>
</packing>
</child>
</widget>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">5</property>
</packing>
</child>
<child>
<widget class="GtkButton" id="btn_refresh_grs">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="receives_default">True</property>
<property name="relief">none</property>
<child>
<widget class="GtkImage" id="image3">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="stock">gtk-refresh</property>
</widget>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">6</property>
</packing>
</child>
<child>
<widget class="GtkVSeparator" id="vseparator6">
<property name="visible">True</property>
<property name="can_focus">False</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">True</property>
<property name="padding">5</property>
<property name="position">7</property>
</packing>
</child>
<child>
<widget class="GtkLabel" id="label3">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="xalign">0.89999997615814209</property>
<property name="xpad">3</property>
<property name="label" translatable="yes">&lt;b&gt;Strategy: &lt;/b&gt;</property>
<property name="use_markup">True</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">8</property>
</packing>
</child>
<child>
<widget class="GtkEntry" id="strat">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="invisible_char"></property>
<property name="primary_icon_activatable">False</property>
<property name="secondary_icon_activatable">False</property>
<property name="primary_icon_sensitive">True</property>
<property name="secondary_icon_sensitive">True</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">True</property>
<property name="position">9</property>
</packing>
</child>
<child>
<widget class="GtkViewport" id="strat_list_viewport">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="resize_mode">queue</property>
<property name="shadow_type">none</property>
<child>
<placeholder/>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">10</property>
</packing>
</child>
<child>
<widget class="GtkVSeparator" id="vseparator7">
<property name="visible">True</property>
<property name="can_focus">False</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="padding">5</property>
<property name="position">11</property>
</packing>
</child>
<child>
<widget class="GtkButton" id="btn_run">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="receives_default">True</property>
<child>
<widget class="GtkHBox" id="run_box">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<widget class="GtkLabel" id="label20">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="label" translatable="yes">Run</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">0</property>
</packing>
</child>
<child>
<widget class="GtkImage" id="image11">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="stock">gtk-go-forward</property>
<property name="icon-size">3</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">13</property>
</packing>
</child>
</widget>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">12</property>
</packing>
</child>
<child>
<widget class="GtkToggleButton" id="synchronize">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="receives_default">True</property>
<property name="has_tooltip">True</property>
<property name="tooltip" translatable="yes">Synchronise</property>
<property name="relief">none</property>
<child>
<widget class="GtkImage" id="image10">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="tooltip" translatable="yes">Synchronise</property>
<property name="stock">gtk-network</property>
</widget>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">True</property>
<property name="pack_type">end</property>
<property name="position">13</property>
</packing>
</child>
<child>
<widget class="GtkButton" id="btn_preferences">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="receives_default">True</property>
<property name="relief">none</property>
<child>
<widget class="GtkImage" id="image1">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="stock">gtk-preferences</property>
</widget>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="pack_type">end</property>
<property name="position">14</property>
</packing>
</child>
<child>
<widget class="GtkButton" id="btn_leave_fullscreen">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="receives_default">True</property>
<property name="relief">none</property>
<child>
<widget class="GtkImage" id="image5">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="stock">gtk-leave-fullscreen</property>
</widget>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="pack_type">end</property>
<property name="position">15</property>
</packing>
</child>
<child>
<widget class="GtkButton" id="btn_enter_fullscreen">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="receives_default">True</property>
<property name="relief">none</property>
<child>
<widget class="GtkImage" id="image4">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="stock">gtk-fullscreen</property>
</widget>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="pack_type">end</property>
<property name="position">16</property>
</packing>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">True</property>
<property name="position">0</property>
</packing>
</child>
<child>
<widget class="GtkHPaned" id="vpaned_corpus">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="border_width">5</property>
<property name="position">30</property>
<property name="position_set">True</property>
<child>
<widget class="GtkHBox" id="hbox10">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<widget class="GtkVBox" id="vbox_corpus">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<placeholder/>
</child>
</widget>
<packing>
<property name="expand">True</property>
<property name="fill">True</property>
<property name="position">0</property>
</packing>
</child>
<child>
<widget class="GtkVBox" id="vbox6">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<placeholder/>
</child>
<child>
<widget class="GtkViewport" id="viewport4">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="resize_mode">queue</property>
<property name="shadow_type">none</property>
<child>
<placeholder/>
</child>
</widget>
<packing>
<property name="expand">True</property>
<property name="fill">True</property>
<property name="position">1</property>
</packing>
</child>
<child>
<widget class="GtkToggleButton" id="btn_show_corpus">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="receives_default">True</property>
<property name="relief">none</property>
<child>
<widget class="GtkLabel" id="corpus_label">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="label" translatable="yes">Corpus</property>
<property name="angle">90</property>
</widget>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">2</property>
</packing>
</child>
<child>
<widget class="GtkViewport" id="viewport5">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="resize_mode">queue</property>
<property name="shadow_type">none</property>
<child>
<placeholder/>
</child>
</widget>
<packing>
<property name="expand">True</property>
<property name="fill">True</property>
<property name="position">3</property>
</packing>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="position">1</property>
</packing>
</child>
</widget>
<packing>
<property name="resize">False</property>
<property name="shrink">True</property>
</packing>
</child>
<child>
<widget class="GtkHPaned" id="vpaned_left">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="position">30</property>
<property name="position_set">True</property>
<child>
<widget class="GtkHBox" id="hbox2">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<widget class="GtkViewport" id="viewport1">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="resize_mode">queue</property>
<child>
<widget class="GtkVBox" id="vbox2">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<widget class="GtkHBox" id="hbox4">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<widget class="GtkHBox" id="hbox5">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<widget class="GtkLabel" id="label5">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="label" translatable="yes">-</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="padding">5</property>
<property name="position">0</property>
</packing>
</child>
<child>
<widget class="GtkHScale" id="grs_zoom">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="adjustment">80 30 310 1 10 10</property>
<property name="round_digits">0</property>
<property name="digits">0</property>
<property name="value_pos">right</property>
</widget>
<packing>
<property name="expand">True</property>
<property name="fill">True</property>
<property name="position">1</property>
</packing>
</child>
<child>
<widget class="GtkLabel" id="label7">
<property name="visible">True</property>
<property name="can_focus">False</property>
<property name="label" translatable="yes">+</property>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">False</property>
<property name="padding">5</property>
<property name="position">2</property>
</packing>
</child>
</widget>
<packing>
<property name="expand">True</property>
<property name="fill">True</property>
<property name="position">0</property>
</packing>
</child>
</widget>
<packing>
<property name="expand">False</property>
<property name="fill">True</property>
<property name="position">0</property>
</packing>
</child>
<child>
<widget class="GtkHBox" id="hbox8">
<property name="visible">True</property>
<property name="can_focus">False</property>
<child>
<widget class="GtkScrolledWindow" id="grs_view">
<property name="visible">True</property>
<property name="can_focus">True</property>
<property name="hscrollbar_policy">automatic</property>