class type gui =
object
method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
- method newRecordDialog: unit -> MatitaGeneratedGui.recordChoiceDialog
method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog
method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog
end
GtkThread.main ();
(match !result with None -> raise MatitaTypes.Cancel | Some r -> r)
-let ask_record_choice ~(gui:#gui) ?(title= "") ?(message = "")
- ~fields ~records ()
-=
- let fields = Array.of_list fields in
- let fields_no = Array.length fields in
- assert (fields_no > 0);
- let dialog = gui#newRecordDialog () in
- dialog#recordChoiceDialog#set_title title;
- dialog#recordChoiceDialogLabel#set_label message;
- let model = new recordModel dialog#recordChoiceTreeView in
- dialog#recordChoiceTreeView#set_headers_visible true;
- let combos =
- Array.init fields_no
- (fun _ -> GTree.store_of_list Gobject.Data.string ["a"; "b"; "c"])
- in
- let (store, col) = combos.(0) in
- store#set ~row:(store#append ()) ~column:col "uno";
- store#set ~row:(store#append ()) ~column:col "due";
- let toggles = Array.init fields_no (fun _ -> false) in
- Array.iteri
- (fun i f -> model#easy_append f i toggles.(i))
- fields;
- let record_no = ref None in
- let return _ =
- dialog#recordChoiceDialog#destroy ();
- GMain.Main.quit ()
- in
- let fail _ = record_no := None; return () in
- ignore (dialog#recordChoiceDialog#event#connect#delete (fun _ -> true));
- connect_button dialog#recordChoiceOkButton (fun _ ->
- match !record_no with None -> () | Some _ -> return ());
- connect_button dialog#recordChoiceCancelButton fail;
-(* ignore (dialog#recordChoiceTreeView#connect#row_activated (fun path _ ->
- interp_no := Some (model#get_interp_no path);
- return ()));
- let selection = dialog#recordChoiceTreeView#selection in
- ignore (selection#connect#changed (fun _ ->
- match selection#get_selected_rows with
- | [path] -> interp_no := Some (model#get_interp_no path)
- | _ -> assert false)); *)
- dialog#recordChoiceDialog#show ();
- GtkThread.main ();
- (match !record_no with Some n -> n | _ -> raise MatitaTypes.Cancel)
-
+let utf8_parsed_text s floc =
+ let start, stop = HExtlib.loc_of_floc floc in
+ let start_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:start in
+ let stop_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:stop in
+ assert(stop_bytes >= start_bytes);
+ let bytes = stop_bytes - start_bytes in
+ try
+ String.sub s start_bytes bytes, bytes
+ with Invalid_argument _ ->
+ Printf.eprintf "%s/%d/%d\n" s start_bytes bytes;
+ assert false
+
+
+let utf8_string_length s =
+ if BuildTimeConf.debug then
+ assert(Glib.Utf8.validate s);
+ Glib.Utf8.length s
+
+let new_search_win title text =
+ let w = new MatitaGeneratedGui.searchWin () in
+ let t =
+ GSourceView.source_view ~auto_indent:false ~editable:false ()
+ in
+ t#source_buffer#insert text;
+ w#toplevel#set_title title;
+ w#scrolledwinContent#add (t :> GObj.widget);
+ ignore(w#buttonSearch#connect#clicked ~callback:( fun () ->
+ let text = w#entrySearch#text in
+ let highlight start end_ =
+ t#source_buffer#move_mark `INSERT ~where:start;
+ t#source_buffer#move_mark `SEL_BOUND ~where:end_;
+ t#scroll_mark_onscreen `INSERT
+ in
+ let iter = t#source_buffer#get_iter `SEL_BOUND in
+ match iter#forward_search text with
+ | None ->
+ (match t#source_buffer#start_iter#forward_search text with
+ | None -> ()
+ | Some (start,end_) -> highlight start end_)
+ | Some (start,end_) -> highlight start end_));
+ ignore(w#buttonClose#connect#clicked ~callback:(fun () ->
+ w#toplevel#misc#hide (); w#toplevel#destroy ()));
+ w
+;;