let blank_uri = "about:blank";;
let current_proof_uri = "about:current_proof";;
let default_script_font = "Monospace 10";;
+let images_dir = "@IMAGES_DIR@";;
fi
MATITA_GTKRC="matita.gtkrc"
+IMAGES_DIR="icons"
AC_SUBST(CAMLP4O)
AC_SUBST(DEBUG)
AC_SUBST(LABLGLADECC)
AC_SUBST(OCAMLFIND)
AC_SUBST(MATITA_GTKRC)
+AC_SUBST(IMAGES_DIR)
AC_OUTPUT([
buildTimeConf.ml
if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *)
Helm_registry.set "matita.mode" "cicbrowser";
let browser = MatitaMathView.cicBrowser () in
- try
- browser#load (`Uri Sys.argv.(1))
- with Invalid_argument _ -> ()
+ let entry =
+ try
+ `Uri Sys.argv.(1)
+ with Invalid_argument _ -> `Dir "cic:/"
+ in
+ browser#load entry
end else begin (* matita *)
Helm_registry.set "matita.mode" "matita";
gui#main#mainWin#show ();
let column_list = new GTree.column_list in
let text_column = column_list#add Gobject.Data.string 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
object (self)
-
initializer
- let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in
- let view_column = GTree.view_column ~renderer () in
tree_view#set_model (Some (list_store :> GTree.model));
ignore (tree_view#append_column view_column)
let iter = list_store#get_iter tree_path in
list_store#get ~row:iter ~column:text_column)
tree_view#selection#get_selected_rows
+ end
+
+class taggedStringListModel ~(tags:(string * GdkPixbuf.pixbuf) list)
+ (tree_view: GTree.view)
+=
+ let column_list = new GTree.column_list in
+ let tag_column = column_list#add Gobject.Data.gobject in
+ let text_column = column_list#add Gobject.Data.string in
+ let list_store = GTree.list_store column_list in
+ let text_renderer = (GTree.cell_renderer_text [], ["text", text_column]) in
+ let tag_renderer = (GTree.cell_renderer_pixbuf [], ["pixbuf", tag_column]) in
+ let text_vcolumn = GTree.view_column ~renderer:text_renderer () in
+ let tag_vcolumn = GTree.view_column ~renderer:tag_renderer () in
+ let lookup_pixbuf tag =
+ try List.assoc tag tags with Not_found -> assert false
+ in
+ object (self)
+ initializer
+ tree_view#set_model (Some (list_store :> GTree.model));
+ ignore (tree_view#append_column tag_vcolumn);
+ ignore (tree_view#append_column text_vcolumn)
+ method list_store = list_store
+
+ method easy_append ~tag s =
+ let tree_iter = list_store#append () in
+ list_store#set ~row:tree_iter ~column:text_column s;
+ list_store#set ~row:tree_iter ~column:tag_column (lookup_pixbuf tag)
+
+ method easy_insert pos ~tag s =
+ let tree_iter = list_store#insert pos in
+ list_store#set ~row:tree_iter ~column:text_column s;
+ list_store#set ~row:tree_iter ~column:tag_column (lookup_pixbuf tag)
+
+ method easy_selection () =
+ List.map
+ (fun tree_path ->
+ let iter = list_store#get_iter tree_path in
+ list_store#get ~row:iter ~column:text_column)
+ tree_view#selection#get_selected_rows
end
class type gui =
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
+ * tags associative list will be shown on the left of the inserted row *)
+class taggedStringListModel:
+ tags:((string * GdkPixbuf.pixbuf) list) ->
+ GTree.view ->
+ object
+ method list_store: GTree.list_store (** list_store forwarding *)
+
+ method easy_append: tag:string -> string -> unit
+ method easy_insert: int -> tag:string -> string -> unit
+ method easy_selection: unit -> string list
+ end
+
(** {2 Matita GUI components} *)
class type gui =
(* debug menu *)
self#main#debugMenu#misc#hide ();
(* status bar *)
- self#main#hintLowImage#set_file "icons/matita-bulb-low.png";
- self#main#hintMediumImage#set_file "icons/matita-bulb-medium.png";
- self#main#hintHighImage#set_file "icons/matita-bulb-high.png";
+ self#main#hintLowImage#set_file (image_path "matita-bulb-low.png");
+ self#main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
+ self#main#hintHighImage#set_file (image_path "matita-bulb-high.png");
(* focus *)
self#main#scriptTextView#misc#grab_focus ();
(* main win dimension *)
ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ())
~title:"Cic browser" ~msg ~cancel:false ());
in
+ let tags =
+ [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png");
+ "obj", GdkPixbuf.from_file (MatitaMisc.image_path "matita-object.png") ]
+ in
let handle_error f =
try
f ()
val mutable current_infos = None
val mutable current_mathml = None
- val model = new MatitaGtkMisc.stringListModel win#whelpResultTreeview
+(* val model = new MatitaGtkMisc.stringListModel win#whelpResultTreeview *)
+ val model =
+ new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview
method private _getWhelpResultTreeviewSelection () =
match model#easy_selection () with
| `Uri uri -> self#_loadUriManagerUri (UriManager.uri_of_string uri)
| `Whelp (query, results) ->
set_whelp_query query;
- self#_loadList results);
+ self#_loadList (List.map (fun r -> "dir", r) results));
self#setEntry entry
end
with
method private _loadDir dir =
let content = Http_getter.ls dir in
let l = List.map (function
- | Http_getter_types.Ls_section sec -> sec
- | Http_getter_types.Ls_object obj -> obj.Http_getter_types.uri
+ | Http_getter_types.Ls_section sec -> "dir", sec
+ | Http_getter_types.Ls_object obj -> "obj", obj.Http_getter_types.uri
) content
in
self#_loadList l
method private _loadList l =
model#list_store#clear ();
- List.iter model#easy_append l;
+ List.iter (fun (tag, s) -> model#easy_append ~tag s) l;
self#_showList
(** { public methods, all must call _load!! } *)
let unopt = function None -> failwith "unopt: None" | Some v -> v
+let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n
+
val get_proof_context: MatitaTypes.status -> Cic.context
val get_proof_aliases: MatitaTypes.status -> DisambiguateTypes.environment
+ (** given the base name of an image, returns its full path *)
+val image_path: string -> string
+
projects / helm.git / commitdiff
