matitaDisambiguator.cmo \
matitaEngine.cmo \
matitacLib.cmo \
+ matitamakeLib.cmo \
matitaScript.cmo \
matitaGeneratedGui.cmo \
matitaGtkMisc.cmo \
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image351">
+ <widget class="GtkImage" id="image384">
<property name="visible">True</property>
<property name="stock">gtk-new</property>
<property name="icon_size">1</property>
<accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image352">
+ <widget class="GtkImage" id="image385">
<property name="visible">True</property>
<property name="stock">gtk-open</property>
<property name="icon_size">1</property>
<accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image353">
+ <widget class="GtkImage" id="image386">
<property name="visible">True</property>
<property name="stock">gtk-save</property>
<property name="icon_size">1</property>
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image354">
+ <widget class="GtkImage" id="image387">
<property name="visible">True</property>
<property name="stock">gtk-save-as</property>
<property name="icon_size">1</property>
</child>
<child>
- <widget class="GtkSeparatorMenuItem" id="separatormenuitem3">
+ <widget class="GtkImageMenuItem" id="developmentsMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Developments...</property>
+ <property name="use_underline">True</property>
+ <accelerator key="d" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image388">
+ <property name="visible">True</property>
+ <property name="stock">gtk-execute</property>
+ <property name="icon_size">1</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkSeparatorMenuItem" id="separator2">
<property name="visible">True</property>
</widget>
</child>
<accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image355">
+ <widget class="GtkImage" id="image389">
<property name="visible">True</property>
<property name="stock">gtk-quit</property>
<property name="icon_size">1</property>
<accelerator key="f" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image356">
+ <widget class="GtkImage" id="image390">
<property name="visible">True</property>
<property name="stock">gtk-find-and-replace</property>
<property name="icon_size">1</property>
</child>
</widget>
+<widget class="GtkWindow" id="newDevelopmentWin">
+ <property name="title" translatable="yes">Create development</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_CENTER_ALWAYS</property>
+ <property name="modal">True</property>
+ <property name="resizable">False</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_UTILITY</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+
+ <child>
+ <widget class="GtkVBox" id="vbox10">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkTable" id="table2">
+ <property name="border_width">3</property>
+ <property name="visible">True</property>
+ <property name="n_rows">2</property>
+ <property name="n_columns">3</property>
+ <property name="homogeneous">False</property>
+ <property name="row_spacing">5</property>
+ <property name="column_spacing">5</property>
+
+ <child>
+ <widget class="GtkLabel" id="label20">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Name</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="left_attach">0</property>
+ <property name="right_attach">1</property>
+ <property name="top_attach">0</property>
+ <property name="bottom_attach">1</property>
+ <property name="x_options">fill</property>
+ <property name="y_options"></property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label21">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Root directory</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="left_attach">0</property>
+ <property name="right_attach">1</property>
+ <property name="top_attach">1</property>
+ <property name="bottom_attach">2</property>
+ <property name="x_options">fill</property>
+ <property name="y_options"></property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkEntry" id="nameEntry">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="editable">True</property>
+ <property name="visibility">True</property>
+ <property name="max_length">0</property>
+ <property name="text" translatable="yes"></property>
+ <property name="has_frame">True</property>
+ <property name="invisible_char">*</property>
+ <property name="activates_default">False</property>
+ </widget>
+ <packing>
+ <property name="left_attach">1</property>
+ <property name="right_attach">2</property>
+ <property name="top_attach">0</property>
+ <property name="bottom_attach">1</property>
+ <property name="y_options"></property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkEntry" id="rootEntry">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="editable">True</property>
+ <property name="visibility">True</property>
+ <property name="max_length">0</property>
+ <property name="text" translatable="yes"></property>
+ <property name="has_frame">True</property>
+ <property name="invisible_char">*</property>
+ <property name="activates_default">False</property>
+ </widget>
+ <packing>
+ <property name="left_attach">1</property>
+ <property name="right_attach">2</property>
+ <property name="top_attach">1</property>
+ <property name="bottom_attach">2</property>
+ <property name="y_options"></property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="chooseRootButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">...</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ <packing>
+ <property name="left_attach">2</property>
+ <property name="right_attach">3</property>
+ <property name="top_attach">1</property>
+ <property name="bottom_attach">2</property>
+ <property name="x_options">fill</property>
+ <property name="y_options"></property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkHSeparator" id="hseparator1">
+ <property name="visible">True</property>
+ </widget>
+ <packing>
+ <property name="padding">2</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkHBox" id="hbox21">
+ <property name="border_width">3</property>
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">5</property>
+
+ <child>
+ <widget class="GtkVBox" id="vbox11">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <placeholder/>
+ </child>
+
+ <child>
+ <placeholder/>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="addButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-add</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="cancelButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-cancel</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkWindow" id="develListWin">
+ <property name="title" translatable="yes">Developments</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_CENTER</property>
+ <property name="modal">False</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+
+ <child>
+ <widget class="GtkVBox" id="vbox12">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="scrolledwindow10">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="vscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+ <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+ <child>
+ <widget class="GtkTreeView" id="developmentsTreeview">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="headers_visible">False</property>
+ <property name="rules_hint">False</property>
+ <property name="reorderable">False</property>
+ <property name="enable_search">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkHSeparator" id="hseparator2">
+ <property name="visible">True</property>
+ </widget>
+ <packing>
+ <property name="padding">2</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkHBox" id="hbox22">
+ <property name="border_width">3</property>
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">4</property>
+
+ <child>
+ <widget class="GtkVBox" id="vbox13">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <placeholder/>
+ </child>
+
+ <child>
+ <placeholder/>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="newButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-new</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="deleteButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-delete</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="buildButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkAlignment" id="alignment14">
+ <property name="visible">True</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xscale">0</property>
+ <property name="yscale">0</property>
+ <property name="top_padding">0</property>
+ <property name="bottom_padding">0</property>
+ <property name="left_padding">0</property>
+ <property name="right_padding">0</property>
+
+ <child>
+ <widget class="GtkHBox" id="hbox23">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
+
+ <child>
+ <widget class="GtkImage" id="image358">
+ <property name="visible">True</property>
+ <property name="stock">gtk-execute</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label22">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Build</property>
+ <property name="use_underline">True</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="cleanButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+
+ <child>
+ <widget class="GtkAlignment" id="alignment15">
+ <property name="visible">True</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xscale">0</property>
+ <property name="yscale">0</property>
+ <property name="top_padding">0</property>
+ <property name="bottom_padding">0</property>
+ <property name="left_padding">0</property>
+ <property name="right_padding">0</property>
+
+ <child>
+ <widget class="GtkHBox" id="hbox24">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
+
+ <child>
+ <widget class="GtkImage" id="image359">
+ <property name="visible">True</property>
+ <property name="stock">gtk-clear</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label23">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">C_lean</property>
+ <property name="use_underline">True</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="closeButton">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-close</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="focus_on_click">True</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
</glade-interface>
Http_getter.init ();
MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
MatitaDb.create_owner_environment ();
+ MatitamakeLib.initialize ();
GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
ignore (GMain.Main.init ());
(fun ~title ~message ->
MatitaGtkMisc.ask_confirmation ~title ~message
~parent:gui#main#toplevel ())
+ ~develcreator:gui#createDevelopment
()
(* math viewers *)
open MatitaTypes
exception Drop;;
+exception UnableToInclude of string;;
let debug = false ;;
let debug_print = if debug then prerr_endline else ignore ;;
with Sys_error _ as exc ->
MatitaLog.error ("Unable to read " ^ path);
MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths);
+ MatitaLog.error ("current working directory is " ^ Unix.getcwd ());
raise exc
;;
(TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
| TacticAst.Include (loc, path) ->
let path = MatitaMisc.obj_file_of_script path in
- let stream = Stream.of_channel (try_open_in opts.include_paths path) in
+ let stream =
+ try
+ Stream.of_channel (try_open_in opts.include_paths path)
+ with Sys_error _ -> raise (UnableToInclude path)
+ in
let status = ref status in
!eval_from_stream_ref status stream (fun _ _ -> ());
!status
*)
exception Drop
+exception UnableToInclude of string
(* heavy checks slow down the compilation process but give you some interesting
* infos like if the theorem is a duplicate *)
false
| _ -> false))
-class stringListModel (tree_view: GTree.view) =
+class multiStringListModel ~cols (tree_view: GTree.view) =
let column_list = new GTree.column_list in
- let text_column = column_list#add Gobject.Data.string in
+ let text_columns =
+ let rec aux = function
+ | 0 -> []
+ | n -> column_list#add Gobject.Data.string :: aux (n - 1)
+ in
+ aux cols
+ in
let list_store = GTree.list_store column_list in
- let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in
- let view_column = GTree.view_column ~renderer () in
+ let renderers =
+ List.map
+ (fun text_column ->
+ (GTree.cell_renderer_text [], ["text", text_column]))
+ text_columns
+ in
+ let view_columns =
+ List.map
+ (fun renderer -> GTree.view_column ~renderer ())
+ renderers
+ in
object (self)
+ val text_columns = text_columns
+
initializer
tree_view#set_model (Some (list_store :> GTree.model));
- ignore (tree_view#append_column view_column)
+ List.iter
+ (fun view_column -> ignore (tree_view#append_column view_column))
+ view_columns
method list_store = list_store
- method easy_append s =
+ method easy_mappend slist =
let tree_iter = list_store#append () in
- list_store#set ~row:tree_iter ~column:text_column s
+ List.iter2
+ (fun s text_column ->
+ list_store#set ~row:tree_iter ~column:text_column s)
+ slist text_columns
- method easy_insert pos s =
+ method easy_minsert pos s =
let tree_iter = list_store#insert pos in
- list_store#set ~row:tree_iter ~column:text_column s
+ List.iter2
+ (fun s text_column ->
+ list_store#set ~row:tree_iter ~column:text_column s)
+ s text_columns
- method easy_selection () =
+ method easy_mselection () =
List.map
(fun tree_path ->
let iter = list_store#get_iter tree_path in
- list_store#get ~row:iter ~column:text_column)
+ List.map
+ (fun text_column ->
+ list_store#get ~row:iter ~column:text_column)
+ text_columns)
+ tree_view#selection#get_selected_rows
+ end
+
+class stringListModel (tree_view: GTree.view) =
+ object (self)
+ inherit multiStringListModel ~cols:1 tree_view as multi
+
+ method list_store = multi#list_store
+
+ method easy_append s =
+ multi#easy_mappend [s]
+
+ method easy_insert pos s =
+ multi#easy_minsert pos [s]
+
+ method easy_selection () =
+ let m = List.map
+ (fun tree_path ->
+ let iter = self#list_store#get_iter tree_path in
+ List.map
+ (fun text_column ->
+ self#list_store#get ~row:iter ~column:text_column)
+ text_columns)
tree_view#selection#get_selected_rows
+ in
+ List.map (function [x] -> x | _ -> assert false) m
end
+
class taggedStringListModel ~(tags:(string * GdkPixbuf.pixbuf) list)
(tree_view: GTree.view)
=
(unit -> unit) -> (* callback *)
unit
+ (** n-ary string column list *)
+class multiStringListModel:
+ cols:int ->
+ GTree.view ->
+ object
+ method list_store: GTree.list_store (** list_store forwarding *)
+
+ method easy_mappend: string list -> unit (** append + set *)
+ method easy_minsert: int -> string list -> unit (** insert + set *)
+ method easy_mselection: unit -> string list list
+ end
+
(** single string column list *)
class stringListModel:
GTree.view ->
object
- method list_store: GTree.list_store (** list_store forwarding *)
+ inherit multiStringListModel
method easy_append: string -> unit (** append + set *)
method easy_insert: int -> string -> unit (** insert + set *)
method easy_selection: unit -> string list
end
+
(** as above with Pixbuf associated to each row. Each time an insert is
* performed a string tag should be specified, the corresponding pixbuf in the
let about = new aboutWin () in
let fileSel = new fileSelectionWin () in
let findRepl = new findReplWin () in
+ let develList = new develListWin () in
+ let newDevel = new newDevelopmentWin () in
let keyBindingBoxes = (* event boxes which should receive global key events *)
[ main#mainWinEventBox ]
in
object (self)
val mutable chosen_file = None
val mutable _ok_not_exists = false
+ val mutable _only_directory = false
val mutable script_fname = None
val mutable font_size = default_font_size
+ val mutable next_devel_must_contain = None
initializer
(* glade's check widgets *)
ignore(self#main#findReplMenuItem#connect#activate
~callback:show_find_Repl);
ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
+ (* developments win *)
+ let model =
+ new MatitaGtkMisc.multiStringListModel
+ ~cols:2 develList#developmentsTreeview
+ in
+ let refresh_devels_win () =
+ model#list_store#clear ();
+ List.iter
+ (fun (name, root) -> model#easy_mappend [name;root])
+ (MatitamakeLib.list_known_developments ())
+ in
+ let get_devel_selected () =
+ match model#easy_mselection () with
+ | [[name;_]] -> MatitamakeLib.development_for_name name
+ | _ -> assert false
+ in
+ connect_button develList#newButton
+ (fun () ->
+ next_devel_must_contain <- None;
+ newDevel#toplevel#misc#show());
+ connect_button develList#deleteButton
+ (fun () ->
+ (match get_devel_selected () with
+ | None -> ()
+ | Some d -> MatitamakeLib.destroy_development d);
+ refresh_devels_win ());
+ connect_button develList#buildButton
+ (fun () ->
+ match get_devel_selected () with
+ | None -> ()
+ | Some d -> ignore(MatitamakeLib.build_development d));
+ connect_button develList#cleanButton
+ (fun () ->
+ match get_devel_selected () with
+ | None -> ()
+ | Some d -> ignore(MatitamakeLib.clean_development d));
+ connect_button develList#closeButton
+ (fun () -> develList#toplevel#misc#hide());
+ ignore(develList#toplevel#event#connect#delete
+ (fun _ -> develList#toplevel#misc#hide();true));
+ let selected_devel = ref None in
+ connect_menu_item self#main#developmentsMenuItem
+ (fun () -> refresh_devels_win ();develList#toplevel#misc#show ());
+
+ (* add development win *)
+ let check_if_root_contains root =
+ match next_devel_must_contain with
+ | None -> true
+ | Some path ->
+ let is_prefix_of d1 d2 =
+ let len1 = String.length d1 in
+ let len2 = String.length d2 in
+ if len2 < len1 then
+ false
+ else
+ let pref = String.sub d2 0 len1 in
+ pref = d1
+ in
+ is_prefix_of root path
+ in
+ connect_button newDevel#addButton
+ (fun () ->
+ let name = newDevel#nameEntry#text in
+ let root = newDevel#rootEntry#text in
+ if check_if_root_contains root then
+ begin
+ ignore (MatitamakeLib.initialize_development name root);
+ refresh_devels_win ();
+ newDevel#nameEntry#set_text "";
+ newDevel#rootEntry#set_text "";
+ newDevel#toplevel#misc#hide()
+ end
+ else
+ MatitaLog.error ("The selected root does not contain " ^
+ match next_devel_must_contain with
+ | Some x -> x
+ | _ -> assert false));
+ connect_button newDevel#chooseRootButton
+ (fun () ->
+ let path = self#chooseDir () in
+ match path with
+ | Some path -> newDevel#rootEntry#set_text path
+ | None -> ());
+ connect_button newDevel#cancelButton
+ (fun () -> newDevel#toplevel#misc#hide ());
+ ignore(newDevel#toplevel#event#connect#delete
+ (fun _ -> newDevel#toplevel#misc#hide();true));
+
(* file selection win *)
ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true));
ignore (fileSel#fileSelectionWin#connect#response (fun event ->
| `OK ->
let fname = fileSel#fileSelectionWin#filename in
if Sys.file_exists fname then
- (if is_regular fname then return (Some fname))
+ begin
+ if is_regular fname && not(_only_directory) then
+ return (Some fname)
+ else if _only_directory && is_dir fname then
+ return (Some fname)
+ end
else
- (if _ok_not_exists then return (Some fname))
+ begin
+ if _ok_not_exists then
+ return (Some fname)
+ end
| `CANCEL -> return None
| `HELP -> ()
| `DELETE_EVENT -> return None));
main#helpMenu#set_right_justified true;
(* console *)
let adj = main#logScrolledWin#vadjustment in
- ignore (adj#connect#changed
+ ignore (adj#connect#changed
(fun _ -> adj#set_value (adj#upper -. adj#page_size)));
console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
(* toolbar *)
method fileSel = fileSel
method findRepl = findRepl
method main = main
+ method develList = develList
+ method newDevel = newDevel
method newBrowserWin () =
object (self)
method chooseFile ?(ok_not_exists = false) () =
_ok_not_exists <- ok_not_exists;
+ _only_directory <- false;
+ fileSel#fileSelectionWin#show ();
+ GtkThread.main ();
+ chosen_file
+
+ method private chooseDir ?(ok_not_exists = false) () =
+ _ok_not_exists <- ok_not_exists;
+ _only_directory <- true;
fileSel#fileSelectionWin#show ();
GtkThread.main ();
+ (* we should check that this is a directory *)
chosen_file
+
+ method createDevelopment ~containing =
+ next_devel_must_contain <- containing;
+ newDevel#toplevel#misc#show()
method askText ?(title = "") ?(msg = "") () =
let dialog = new textDialog () in
method fileSel : MatitaGeneratedGui.fileSelectionWin
method main : MatitaGeneratedGui.mainWin
method findRepl : MatitaGeneratedGui.findReplWin
+ method develList: MatitaGeneratedGui.develListWin
+ method newDevel: MatitaGeneratedGui.newDevelopmentWin
(* method toolbar : MatitaGeneratedGui.toolBarWin *)
method console: console
* @param ok_not_exists if set to true returns also non existent files
* (useful for save). Defaults to false *)
method chooseFile: ?ok_not_exists:bool -> unit -> string option
+ method createDevelopment: containing:string option -> unit
(** prompt the user for a (multiline) text entry *)
method askText: ?title:string -> ?msg:string -> unit -> string option
output_string oc data;
close_out oc
+
+let absolute_path file =
+ if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
+
let is_proof_script fname = true (** TODO Zack *)
let is_proof_object fname = true (** TODO Zack *)
val input_file: string -> string (** read all the contents of file to string *)
val output_file: string -> string -> unit (** write string to file *)
+val absolute_path: string -> string
+
(** @return true if file is a (textual) proof script *)
val is_proof_script: string -> bool
let loc = CicAst.dummy_floc in
A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n))))
-let eval_with_engine status user_goal parsed_text st =
+type guistuff = {
+ mathviewer:MatitaTypes.mathViewer;
+ urichooser: UriManager.uri list -> UriManager.uri list;
+ ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
+ develcreator: containing:string option -> unit;
+ mutable filenamedata: string option * MatitamakeLib.development option
+}
+
+let eval_with_engine guistuff status user_goal parsed_text st =
let module TA = TacticAst in
let module TAPp = TacticAstPp in
+ let include_ =
+ match guistuff.filenamedata with
+ | _,None -> []
+ | None,Some devel -> [MatitamakeLib.root_for_development devel ]
+ | Some f,_ ->
+ match MatitamakeLib.development_for_dir (Filename.dirname f) with
+ | None -> []
+ | Some devel -> [MatitamakeLib.root_for_development devel ]
+ in
let parsed_text_length = String.length parsed_text in
let loc, ex =
match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false
match status.proof_status with
| Incomplete_proof (_, goal) when goal <> user_goal ->
goal_changed := true;
- MatitaEngine.eval_ast
+ MatitaEngine.eval_ast ~include_paths:include_
~do_heavy_checks:true status (goal_ast user_goal)
| _ -> status
in
- let new_status = MatitaEngine.eval_ast ~do_heavy_checks:true status st in
+ let new_status =
+ MatitaEngine.eval_ast
+ ~include_paths:include_ ~do_heavy_checks:true status st
+ in
let new_aliases =
match ex with
| TA.Command (_, TA.Alias _)
in
[ new_status, new_text ], parsed_text_length
+let eval_with_engine guistuff status user_goal parsed_text st =
+ try
+ eval_with_engine guistuff status user_goal parsed_text st
+ with
+ MatitaEngine.UnableToInclude what as exc ->
+ let compile_needed_and_go_on d =
+ let root = MatitamakeLib.root_for_development d in
+ let target = root ^ "/" ^ what in
+ if not(MatitamakeLib.build_development ~target d) then
+ raise exc
+ else
+ eval_with_engine guistuff status user_goal parsed_text st
+ in
+ let do_nothing () = [], 0 in
+ let handle_with_devel d =
+ let name = MatitamakeLib.name_for_development d in
+ let title = "Unable to include " ^ what in
+ let message =
+ what ^ " is handled by development <b>" ^ name ^ "</b>.\n\n" ^
+ "<i>Should I compile it and Its dependencies?</i>"
+ in
+ (match guistuff.ask_confirmation ~title ~message with
+ | `YES -> compile_needed_and_go_on d
+ | `NO -> raise exc
+ | `CANCEL -> do_nothing ())
+ in
+ let handle_withoud_devel filename =
+ let title = "Unable to include " ^ what in
+ let message =
+ what ^ " is <b>not</b> handled by a development.\n" ^
+ "All dependencies are authomatically solved for a development.\n\n" ^
+ "<i>Do you want to set up a development?</i>"
+ in
+ (match guistuff.ask_confirmation ~title ~message with
+ | `YES ->
+ (match filename with
+ | Some f ->
+ guistuff.develcreator ~containing:(Some (Filename.dirname f))
+ | None -> guistuff.develcreator ~containing:None);
+ do_nothing ()
+ | `NO -> raise exc
+ | `CANCEL -> do_nothing())
+ in
+ match guistuff.filenamedata with
+ | None,None -> handle_withoud_devel None
+ | None,Some d -> handle_with_devel d
+ | Some f,_ ->
+ match MatitamakeLib.development_for_dir (Filename.dirname f) with
+ | None -> handle_withoud_devel (Some f)
+ | Some d -> handle_with_devel d
+;;
+
let disambiguate term status =
let module MD = MatitaDisambiguator in
let dbd = MatitaDb.instance () in
| [_,_,x,_] -> x
| _ -> assert false
-let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser
- parsed_text script mac
+let eval_macro guistuff status parsed_text script mac
=
let module TA = TacticAst in
let module TAPp = TacticAstPp in
let term = disambiguate term status in
let l = MQ.match_term ~dbd term in
let entry = `Whelp (TAPp.pp_macro_cic (TA.WMatch (loc, term)), l) in
- mathviewer#show_uri_list ~reuse:true ~entry l;
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
| TA.WInstance (loc, term) ->
let term = disambiguate term status in
let l = MQ.instance ~dbd term in
let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
- mathviewer#show_uri_list ~reuse:true ~entry l;
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
| TA.WLocate (loc, s) ->
let l = MQ.locate ~dbd s in
let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
- mathviewer#show_uri_list ~reuse:true ~entry l;
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
| TA.WElim (loc, term) ->
let term = disambiguate term status in
in
let l = MQ.elim ~dbd uri in
let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
- mathviewer#show_uri_list ~reuse:true ~entry l;
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
| TA.WHint (loc, term) ->
let term = disambiguate term status in
let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
let l = List.map fst (MQ.experimental_hint ~dbd s) in
let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in
- mathviewer#show_uri_list ~reuse:true ~entry l;
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
(* REAL macro *)
| TA.Hint loc ->
let s = MatitaMisc.get_proof_status status in
let l = List.map fst (MQ.experimental_hint ~dbd s) in
- let selected = urichooser l in
+ let selected = guistuff.urichooser l in
(match selected with
| [] -> [], parsed_text_length
| [uri] ->
in
let ty,_ = CTC.type_of_aux' metasenv context term ugraph in
let t_and_ty = Cic.Cast (term,ty) in
- mathviewer#show_entry (`Cic (t_and_ty,metasenv));
+ guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
[], parsed_text_length
(* | TA.Abort _ ->
let rec go_back () =
| TA.Search_term (_, search_kind, term) -> failwith "not implemented"
-let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser
-ask_confirmation user_goal parsed_text script ex =
+let eval_executable guistuff status user_goal parsed_text script ex =
let module TA = TacticAst in
let module TAPp = TacticAstPp in
let module MD = MatitaDisambiguator in
| Some u ->
if not (MatitacleanLib.is_empty u) then
match
- ask_confirmation
+ guistuff.ask_confirmation
~title:"Baseuri redefinition"
~message:(
"Baseuri " ^ u ^ " already exists.\n" ^
| `YES -> MatitacleanLib.clean_baseuris [u]
| `NO -> ()
| `CANCEL -> raise MatitaTypes.Cancel);
- eval_with_engine status user_goal parsed_text (TA.Executable (loc, ex))
+ eval_with_engine
+ guistuff status user_goal parsed_text (TA.Executable (loc, ex))
with MatitaTypes.Cancel -> [], 0)
| TA.Macro (_,mac) ->
- eval_macro status mathviewer urichooser parsed_text script mac
+ eval_macro guistuff status parsed_text script mac
-let rec eval_statement status (mathviewer:MatitaTypes.mathViewer) urichooser
-ask_confirmation user_goal script s =
+let rec eval_statement guistuff status user_goal script s =
if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
let st = CicTextualParser2.parse_statement (Stream.of_string s) in
let text_of_loc loc =
let remain_len = String.length s - parsed_text_length in
let s = String.sub s parsed_text_length remain_len in
let s,len =
- eval_statement status
- mathviewer urichooser ask_confirmation user_goal script s
+ eval_statement guistuff status user_goal script s
in
(match s with
| (status, text) :: tl ->
| [] -> [], 0)
| TacticAst.Executable (loc, ex) ->
let parsed_text, parsed_text_length = text_of_loc loc in
- eval_executable
- status mathviewer urichooser ask_confirmation
- user_goal parsed_text script ex
+ eval_executable guistuff status user_goal parsed_text script ex
let fresh_script_id =
let i = ref 0 in
~(mathviewer: MatitaTypes.mathViewer)
~set_star
~ask_confirmation
- ~urichooser () =
+ ~urichooser
+ ~develcreator
+ () =
object (self)
- val mutable filename = None
val scriptId = fresh_script_id ()
+
+ val guistuff = {
+ mathviewer = mathviewer;
+ urichooser = urichooser;
+ ask_confirmation = ask_confirmation;
+ develcreator = develcreator;
+ filenamedata = (None, None)}
+
method private getFilename =
- match filename with Some f -> f | _ -> assert false
+ match guistuff.filenamedata with Some f,_ -> f | _ -> assert false
+
method private ppFilename =
- match filename with Some f -> f | None -> sprintf ".unnamed%d.ma" scriptId
+ match guistuff.filenamedata with
+ | Some f,_ -> f
+ | None,_ -> sprintf ".unnamed%d.ma" scriptId
initializer
ignore(GMain.Timeout.add ~ms:300000
let s = match statement with Some s -> s | None -> self#getFuture in
MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
let (entries, parsed_len) =
- eval_statement self#status
- mathviewer urichooser ask_confirmation userGoal self s
+ eval_statement guistuff self#status userGoal self s
in
let (new_statuses, new_statements) = List.split entries in
(*
buffer#set_modified false
method assignFileName file =
- filename <- Some file;
+ let abspath = MatitaMisc.absolute_path file in
+ let devel = MatitamakeLib.development_for_dir (Filename.dirname abspath) in
+ guistuff.filenamedata <- Some abspath, devel
method saveToFile () =
let oc = open_out self#getFilename in
method template () =
let template = MatitaMisc.input_file BuildTimeConf.script_template in
buffer#insert ~iter:(buffer#get_iter `START) template;
- filename <- None;
+ guistuff.filenamedata <-
+ (None,MatitamakeLib.development_for_dir (Unix.getcwd ()));
buffer#set_modified false;
set_star self#ppFilename false
MatitaLog.debug (sprintf "%d statements:" (List.length statements));
List.iter MatitaLog.debug statements;
MatitaLog.debug ("Current file name: " ^
- (match filename with None -> "[ no name ]" | Some f -> f));
+ (match guistuff.filenamedata with
+ |None,_ -> "[ no name ]"
+ | Some f,_ -> f));
end
let _script = ref None
-let script ~buffer ~init ~mathviewer ~urichooser ~ask_confirmation ~set_star ()
+let script ~buffer ~init ~mathviewer ~urichooser ~develcreator ~ask_confirmation ~set_star ()
=
let s = new script
- ~buffer ~init ~mathviewer ~ask_confirmation ~urichooser ~set_star ()
+ ~buffer ~init ~mathviewer ~ask_confirmation ~urichooser ~develcreator ~set_star ()
in
_script := Some s;
s
init:MatitaTypes.status ->
mathviewer: MatitaTypes.mathViewer->
urichooser: (UriManager.uri list -> UriManager.uri list) ->
+ develcreator: (containing:string option -> unit) ->
ask_confirmation:
(title:string -> message:string -> [`YES | `NO | `CANCEL]) ->
set_star: (string -> bool -> unit) ->
| None ->
dump_development dev;
rebuild_makefile dev;
+ developments := dev :: !developments;
Some dev
let make chdir args =
let old = Unix.getcwd () in
- Unix.chdir chdir;
-(* prerr_endline (String.concat " " ("make"::args));*)
- let rc = Unix.system (String.concat " " ("make"::args)) in
- Unix.chdir old;
- match rc with
- | Unix.WEXITED 0 -> true
- | Unix.WEXITED i -> logger `Error ("make returned " ^ string_of_int i);false
- | _ -> logger `Error "make STOPPED or SIGNALED!";false
+ try
+ Unix.chdir chdir;
+ let rc = Unix.system (String.concat " " ("make"::args)) in
+ Unix.chdir old;
+ match rc with
+ | Unix.WEXITED 0 -> true
+ | Unix.WEXITED i -> logger `Error ("make returned " ^ string_of_int i);false
+ | _ -> logger `Error "make STOPPED or SIGNALED!";false
+ with Unix.Unix_error (_,cmd,err) ->
+ logger `Warning ("Unix Error: " ^ cmd ^ ": " ^ err);
+ false
let call_make development target =
rebuild_makefile development;
unlink (pool () ^ development.name ^ rootfile);
unlink (pool () ^ development.name ^ "/depend");
unlink (pool () ^ development.name ^ "/depend.short");
- rmdir (pool () ^ development.name)
+ rmdir (pool () ^ development.name);
+ developments :=
+ List.filter (fun d -> d.name <> development.name) !developments
in
if not(clean_development development) then
begin
end;
delete_development development
-
+let root_for_development development = development.root
+let name_for_development development = development.name
+
val destroy_development: development -> unit
(* initiale internal data structures *)
val initialize : unit -> unit
-
+(* gives back the root *)
+val root_for_development : development -> string
+(* gives back the name *)
+val name_for_development : development -> string
projects / helm.git / commitdiff