?copy_cb ()
~id uris
=
- let gui = MatitaMisc.get_gui () in
if (selection_mode <> `SINGLE) &&
(Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation")
then
uris
else begin
- let dialog = gui#newUriDialog () in
+ let dialog = new uriChoiceDialog () in
if hide_uri_entry then
dialog#uriEntryHBox#misc#hide ();
if hide_try then
(offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
| _::_ ->
let dialog = new disambiguationErrors () in
- dialog#check_widgets ();
if all_passes then
dialog#disambiguationErrorsMoreErrors#misc#set_sensitive false;
let model = new interpErrorModel dialog#treeview choices in
initializer
let s () = MatitaScript.current () in
- (* glade's check widgets *)
- List.iter (fun w -> w#check_widgets ())
- (let c w = (w :> <check_widgets: unit -> unit>) in
- [ c fileSel; c main; c findRepl]);
(* key bindings *)
List.iter (* global key bindings *)
(fun (key, callback) -> self#addKeyBinding key callback)
let image =
GMisc.image ~stock:`CLOSE ~icon_size:`MENU () in
closebutton#set_image image#coerce;
- let script =
- MatitaScript.script
- ~urichooser:(fun source_view uris ->
- try
- interactive_uri_choice ~selection_mode:`SINGLE
- ~title:"Matita: URI chooser"
- ~msg:"Select the URI" ~hide_uri_entry:true
- ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
- ~copy_cb:(fun s -> source_view#buffer#insert ("\n"^s^"\n"))
- () ~id:"boh?" uris
- with MatitaTypes.Cancel -> [])
- ~ask_confirmation:
- (fun ~title ~message ->
- MatitaGtkMisc.ask_confirmation ~title ~message
- ~parent:(MatitaMisc.get_gui ())#main#toplevel ())
- ~parent:scrolledWindow ~tab_label ()
- in
+ let script = MatitaScript.script ~parent:scrolledWindow ~tab_label () in
ignore (main#scriptNotebook#prepend_page ~tab_label:hbox#coerce
scrolledWindow#coerce);
ignore (closebutton#connect#clicked (fun () ->
inherit browserWin ()
val combo = GEdit.entry ()
initializer
- self#check_widgets ();
let combo_widget = combo#coerce in
uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget;
combo#misc#grab_focus ()
method browserUri = combo
end
- method newUriDialog () =
- let dialog = new uriChoiceDialog () in
- dialog#check_widgets ();
- dialog
-
- method private newConfirmationDialog () =
- let dialog = new confirmationDialog () in
- dialog#check_widgets ();
- dialog
-
- method newEmptyDialog () =
- let dialog = new emptyDialog () in
- dialog#check_widgets ();
- dialog
-
method private addKeyBinding key callback =
List.iter (fun evbox -> add_key_binding key callback evbox)
keyBindingBoxes
let interactive_string_choice
text prefix_len ?(title = "") ?(msg = "") () ~id locs uris
=
- let gui = instance () in
- let dialog = gui#newUriDialog () in
- dialog#uriEntryHBox#misc#hide ();
- dialog#uriChoiceSelectedButton#misc#hide ();
- dialog#uriChoiceAutoButton#misc#hide ();
- dialog#uriChoiceConstantsButton#misc#hide ();
- dialog#uriChoiceTreeView#selection#set_mode
- (`SINGLE :> Gtk.Tags.selection_mode);
- let model = new stringListModel dialog#uriChoiceTreeView in
- let choices = ref None in
- dialog#uriChoiceDialog#set_title title;
- let hack_len = MatitaGtkMisc.utf8_string_length text in
- let rec colorize acc_len = function
- | [] ->
- let floc = HExtlib.floc_of_loc (acc_len,hack_len) in
- escape_pango_markup (fst(MatitaGtkMisc.utf8_parsed_text text floc))
- | he::tl ->
- let start, stop = HExtlib.loc_of_floc he in
- let floc1 = HExtlib.floc_of_loc (acc_len,start) in
- let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in
- let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in
- escape_pango_markup str1 ^ "<b>" ^
- escape_pango_markup str2 ^ "</b>" ^
- colorize stop tl
- in
+ let dialog = new uriChoiceDialog () in
+ dialog#uriEntryHBox#misc#hide ();
+ dialog#uriChoiceSelectedButton#misc#hide ();
+ dialog#uriChoiceAutoButton#misc#hide ();
+ dialog#uriChoiceConstantsButton#misc#hide ();
+ dialog#uriChoiceTreeView#selection#set_mode
+ (`SINGLE :> Gtk.Tags.selection_mode);
+ let model = new stringListModel dialog#uriChoiceTreeView in
+ let choices = ref None in
+ dialog#uriChoiceDialog#set_title title;
+ let hack_len = MatitaGtkMisc.utf8_string_length text in
+ let rec colorize acc_len = function
+ | [] ->
+ let floc = HExtlib.floc_of_loc (acc_len,hack_len) in
+ escape_pango_markup (fst(MatitaGtkMisc.utf8_parsed_text text floc))
+ | he::tl ->
+ let start, stop = HExtlib.loc_of_floc he in
+ let floc1 = HExtlib.floc_of_loc (acc_len,start) in
+ let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in
+ let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in
+ escape_pango_markup str1 ^ "<b>" ^
+ escape_pango_markup str2 ^ "</b>" ^
+ colorize stop tl
+ in
(* List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
- Printf.eprintf "(%d,%d)" start stop) locs; *)
- let locs =
- List.sort
- (fun loc1 loc2 ->
- fst (HExtlib.loc_of_floc loc1) - fst (HExtlib.loc_of_floc loc2))
- locs
- in
+ Printf.eprintf "(%d,%d)" start stop) locs; *)
+ let locs =
+ List.sort
+ (fun loc1 loc2 ->
+ fst (HExtlib.loc_of_floc loc1) - fst (HExtlib.loc_of_floc loc2))
+ locs
+ in
(* prerr_endline "XXXXXXXXXXXXXXXXXXXX";
- List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
- Printf.eprintf "(%d,%d)" start stop) locs;
- prerr_endline "XXXXXXXXXXXXXXXXXXXX2"; *)
- dialog#uriChoiceLabel#set_use_markup true;
- let txt = colorize 0 locs in
- let txt,_ = MatitaGtkMisc.utf8_parsed_text txt
- (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt))
- in
- dialog#uriChoiceLabel#set_label txt;
- List.iter model#easy_append uris;
- let return v =
- choices := v;
- dialog#uriChoiceDialog#destroy ();
- GMain.Main.quit ()
- in
- ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
- connect_button dialog#uriChoiceForwardButton (fun _ ->
- match model#easy_selection () with
- | [] -> ()
- | uris -> return (Some uris));
- connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
- dialog#uriChoiceDialog#show ();
- GtkThread.main ();
- (match !choices with
- | None -> raise MatitaTypes.Cancel
- | Some uris -> uris)
+ List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
+ Printf.eprintf "(%d,%d)" start stop) locs;
+ prerr_endline "XXXXXXXXXXXXXXXXXXXX2"; *)
+ dialog#uriChoiceLabel#set_use_markup true;
+ let txt = colorize 0 locs in
+ let txt,_ = MatitaGtkMisc.utf8_parsed_text txt
+ (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt))
+ in
+ dialog#uriChoiceLabel#set_label txt;
+ List.iter model#easy_append uris;
+ let return v =
+ choices := v;
+ dialog#uriChoiceDialog#destroy ();
+ GMain.Main.quit ()
+ in
+ ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
+ connect_button dialog#uriChoiceForwardButton (fun _ ->
+ match model#easy_selection () with
+ | [] -> ()
+ | uris -> return (Some uris));
+ connect_button dialog#uriChoiceAbortButton (fun _ -> return None);
+ dialog#uriChoiceDialog#show ();
+ GtkThread.main ();
+ (match !choices with
+ | None -> raise MatitaTypes.Cancel
+ | Some uris -> uris)
let interactive_interp_choice () text prefix_len choices =
(*List.iter (fun l -> prerr_endline "==="; List.iter (fun (_,id,dsc) -> prerr_endline (id ^ " = " ^ dsc)) l) choices;*)
String.sub s 0 nl_pos
with Not_found -> s
-type guistuff = {
- urichooser: NReference.reference list -> NReference.reference list;
- ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
-}
-
-let eval_with_engine include_paths guistuff status skipped_txt nonskipped_txt st
+let eval_with_engine include_paths status skipped_txt nonskipped_txt st
=
let parsed_text_length =
String.length skipped_txt + String.length nonskipped_txt
let pp_eager_statement_ast = GrafiteAstPp.pp_statement
-let eval_nmacro include_paths (buffer : GText.buffer) guistuff status unparsed_text parsed_text script mac =
+let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parsed_text script mac =
let parsed_text_length = String.length parsed_text in
match mac with
| TA.Screenshot (_,name) ->
[s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length
| TA.NAutoInteractive (_, (Some _,_)) -> assert false
-let rec eval_executable include_paths (buffer : GText.buffer) guistuff
+let rec eval_executable include_paths (buffer : GText.buffer)
status unparsed_text skipped_txt nonskipped_txt script ex loc
=
try
ignore (buffer#move_mark (`NAME "beginning_of_statement")
~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars
(Glib.Utf8.length skipped_txt))) ;
- eval_with_engine include_paths guistuff status skipped_txt nonskipped_txt
+ eval_with_engine include_paths status skipped_txt nonskipped_txt
(TA.Executable (loc, ex))
with
MatitaTypes.Cancel -> [], "", 0
| GrafiteEngine.NMacro (_loc,macro) ->
- eval_nmacro include_paths buffer guistuff status
+ eval_nmacro include_paths buffer status
unparsed_text (skipped_txt ^ nonskipped_txt) script macro
-and eval_statement include_paths (buffer : GText.buffer) guistuff status script
+and eval_statement include_paths (buffer : GText.buffer) status script
statement
=
let st,unparsed_text =
match st with
| GrafiteAst.Executable (loc, ex) ->
let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in
- eval_executable include_paths buffer guistuff status unparsed_text
+ eval_executable include_paths buffer status unparsed_text
skipped nonskipped script ex loc
| GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))
when Helm_registry.get_bool "matita.execcomments" ->
let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in
- eval_executable include_paths buffer guistuff status unparsed_text
+ eval_executable include_paths buffer status unparsed_text
skipped nonskipped script ex loc
| GrafiteAst.Comment (loc, _) ->
let parsed_text, _, _, parsed_text_length = text_of_loc loc in
let s = String.sub unparsed_text parsed_text_length remain_len in
let s,text,len =
try
- eval_statement include_paths buffer guistuff status script (`Raw s)
+ eval_statement include_paths buffer status script (`Raw s)
with
HExtlib.Localized (floc, exn) ->
HExtlib.raise_localized_exception
* "TERM" and "PATTERN", in the future other targets like "MATHMLCONTENT" may
* be added
*)
-class script ~ask_confirmation ~urichooser ~(parent:GBin.scrolled_window) ~tab_label () =
+class script ~(parent:GBin.scrolled_window) ~tab_label () =
let source_view =
GSourceView2.source_view
~auto_indent:true
val scriptId = fresh_script_id ()
- val guistuff = {
- urichooser = urichooser source_view;
- ask_confirmation = ask_confirmation;
- }
-
val mutable filename_ = (None : string option)
method has_name = filename_ <> None
let time1 = Unix.gettimeofday () in
let entries, newtext, parsed_len =
try
- eval_statement self#include_paths buffer guistuff self#status self (`Raw s)
+ eval_statement self#include_paths buffer self#status self (`Raw s)
with End_of_file -> raise Margin
in
let time2 = Unix.gettimeofday () in
let _script = ref []
-let script ~urichooser ~ask_confirmation ~parent ~tab_label ()
+let script ~parent ~tab_label ()
=
- let s = new script ~ask_confirmation ~urichooser ~parent ~tab_label () in
+ let s = new script ~parent ~tab_label () in
_script := s::!_script;
s
projects / helm.git / commitdiff