open Printf
-open GrafiteTypes
-open MatitaGtkMisc
open MatitaGuiTypes
-open GtkSourceView2
+open GtkSourceView3
-type document_element = string
+let matita_script_current = ref (fun _ -> (assert false : < advance: ?statement:string -> unit -> unit; status: GrafiteTypes.status >));;
+let register_matita_script_current f = matita_script_current := f;;
+let get_matita_script_current () = !matita_script_current ();;
+
+type document_element = (int * int * string) list * string (* hyperlinks,text *)
class type cicMathView =
object
inherit GObj.widget
- method set_font_size: int -> unit
- method update_font_size: unit
-
method load_root : root:document_element -> unit
- method action_toggle: document_element -> bool
method remove_selections: unit
method set_selection: document_element option -> unit
method get_selections: document_element list
- method has_selection: bool
(** @raise Failure "no selection" *)
method strings_of_selection: (MatitaGuiTypes.paste_kind * string) list
(** Gdome.element of a MathML document whose rendering should be blank. Used
* by cicBrowser to render "about:blank" document *)
-let empty_mathml = lazy ""
+let empty_mathml = lazy ([],"")
(** shown for goals closed by side effects *)
-let closed_goal_mathml = lazy "chiuso per side effect..."
+let closed_goal_mathml = lazy ([],"chiuso per side effect...")
(*
let rec has_maction (elt :Gdome.element) =
*)
class clickableMathView obj =
-let text_width = 80 in
+(*let text_width = 80 in*)
object (self)
- inherit GSourceView2.source_view obj
+ inherit GSourceView3.source_view obj
- method has_selection = (assert false : bool)
method strings_of_selection = (assert false : (paste_kind * string) list)
- method update_font_size =
- self#misc#modify_font_by_name
- (sprintf "%s %d" BuildTimeConf.script_font (MatitaMisc.get_current_font_size ()))
- method set_href_callback = (function _ -> () : (string -> unit) option -> unit)
+
+ val mutable href_callback: (string -> unit) option = None
+ method set_href_callback f = href_callback <- f
+
+ val mutable href_statusbar_msg:
+ (GMisc.statusbar_context * Gtk.statusbar_message) option = None
+ (* <statusbar ctxt, statusbar msg> *)
+
method private set_cic_info = (function _ -> () : unit (*(Cic.conjecture option * (Cic.id, Cic.term) Hashtbl.t *
(Cic.id, Cic.hypothesis) Hashtbl.t *
(Cic.id, Cic.id option) Hashtbl.t * ('a, 'b) Hashtbl.t * 'c option)*) option -> unit)
(* dal widget di Luca *)
- method load_root ~root =
- self#buffer#delete ~start:(self#buffer#get_iter `START)
- ~stop:(self#buffer#get_iter `END);
- self#buffer#insert root
+ method load_root ~root:(hyperlinks,text) =
+ self#buffer#set_text text;
+ let all_tag = self#buffer#create_tag [] in
+ self#buffer#apply_tag all_tag ~start:(self#buffer#get_iter `START)
+ ~stop:(self#buffer#get_iter `END);
+ ignore(all_tag#connect#event
+ ~callback:(fun ~origin:_ event _pos ->
+ match GdkEvent.get_type event with
+ | `MOTION_NOTIFY ->
+ Gdk.Window.set_cursor
+ (match self#get_window `TEXT with None -> assert false | Some x -> x)
+ (Gdk.Cursor.create `ARROW);
+ HExtlib.iter_option (fun (ctxt, msg) -> ctxt#remove msg)
+ href_statusbar_msg;
+ false
+ | _ -> false));
+ let hyperlink_tag = self#buffer#create_tag [] in
+ ignore(hyperlink_tag#connect#event
+ ~callback:(fun ~origin:_ event pos ->
+ let offset = (new GText.iter pos)#offset in
+ let _,_,href =
+ try
+ List.find
+ (fun (start,stop,_href) -> start <= offset && offset <= stop
+ ) hyperlinks
+ with
+ Not_found -> assert false
+ in
+ match GdkEvent.get_type event with
+ `BUTTON_PRESS ->
+ (match href_callback with
+ None -> ()
+ | Some f -> f href);
+ true
+ | `MOTION_NOTIFY ->
+ Gdk.Window.set_cursor
+ (match self#get_window `TEXT with None -> assert false | Some x -> x)
+ (Gdk.Cursor.create `HAND1);
+ let ctxt = (MatitaMisc.get_gui ())#main#statusBar#new_context ~name:"href" in
+ let msg = ctxt#push href in
+ href_statusbar_msg <- Some (ctxt, msg);
+ false
+ | _ -> false));
+ List.iter
+ ( fun (start,stop,(_href : string)) ->
+ self#buffer#apply_tag hyperlink_tag
+ ~start:(self#buffer#get_iter_at_char start)
+ ~stop:(self#buffer#get_iter_at_char (stop+1));
+ ) hyperlinks
+
+
method action_toggle = (fun _ -> assert false : document_element -> bool)
method remove_selections = (() : unit)
method set_selection = (fun _ -> () : document_element option -> unit)
method get_selections = (assert false : document_element list)
- method set_font_size font_size =
- self#misc#modify_font_by_name
- (sprintf "%s %d" BuildTimeConf.script_font font_size)
initializer
- self#set_font_size (MatitaMisc.get_current_font_size ());
self#source_buffer#set_language (Some MatitaGtkMisc.matita_lang);
self#source_buffer#set_highlight_syntax true;
- self#set_editable false
+ self#set_editable false;
+ MatitaMisc.observe_font_size
+ (fun size ->
+ self#misc#modify_font_by_name
+ (sprintf "%s %d" BuildTimeConf.script_font size))
-(* MATITA1.0
+(* MATITA 1.0
inherit GMathViewAux.multi_selection_math_view obj
val mutable href_callback: (string -> unit) option = None
val maction_cursor = Gdk.Cursor.create `QUESTION_ARROW
initializer
- self#set_font_size (MatitaMisc.get_current_font_size ());
ignore (self#connect#selection_changed self#choose_selection_cb);
ignore (self#event#connect#button_press self#button_press_cb);
ignore (self#event#connect#button_release self#button_release_cb);
(GrafiteAst.Tactic (loc,
Some (GrafiteAst.Reduce (loc, kind, pat)),
GrafiteAst.Semicolon loc)) in
- (MatitaScript.current ())#advance ~statement () in
+ (get_matita_script_current ())#advance ~statement () in
connect_menu_item copy gui#copy;
connect_menu_item normalize (reduction_action `Normalize);
connect_menu_item simplify (reduction_action `Simpl);
| None -> self#set_selection None);
selection_changed <- true
- method update_font_size = self#set_font_size (MatitaMisc.get_current_font_size ())
-
(** find a term by id from stored CIC infos @return either `Hyp if the id
* correspond to an hypothesis or `Term (cic, hyp) if the id correspond to a
* term. In the latter case hyp is either None (if the term is a subterm of
else string_of_dom_node node
method private string_of_cic_sequent ~output_type cic_sequent =
- let script = MatitaScript.current () in
+ let script = get_matita_script_current () in
let metasenv =
if script#onGoingProof () then script#proofMetasenv else [] in
let map_unicode_to_tex =
| [] -> None
| node :: _ -> Some (self#string_of_node ~paste_kind node)
- method has_selection = self#get_selections <> []
-
(** @return an associative list format -> string with all possible selection
* formats. Rationale: in order to convert the selection to TERM or PATTERN
* format we need the sequent, the metasenv, ... keeping all of them in a
let sequent = List.assoc metano metasenv in
let txt =
ApplyTransformation.ntxt_of_cic_sequent
- ~map_unicode_to_tex:false 80 status metasenv subst (metano,sequent)
+ ~map_unicode_to_tex:false 80 status ~metasenv ~subst (metano,sequent)
in
(* MATITA 1.0 if BuildTimeConf.debug then begin
let name =
self#thaw
| _ ->
*)
- (* MATITA1.0 if BuildTimeConf.debug then begin
+ (* MATITA 1.0 if BuildTimeConf.debug then begin
let name =
"/tmp/cic_browser_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in
HLog.debug ("cic_browser: dumping MathML to ./" ^ name);
let obj = SourceView.new_ () in
Gobject.set_params (Gobject.try_cast obj "GtkSourceView") pl;
new _cicMathView obj)(*)) ?auto_indent ?highlight_current_line ?indent_on_tab ?indent_width ?insert_spaces_instead_of_tabs ?right_margin_position ?show_line_marks ?show_line_numbers ?show_right_margin ?smart_home_end ?tab_width ?editable ?cursor_visible ?justification ?wrap_mode ?accepts_tab ?border_width*) [] ?width ?height ?packing ?show () :> cicMathView)
+
+let screenshot _status _sequents _metasenv _subst (_filename (*as ofn*)) =
+ () (*MATITA 1.0
+ let w = GWindow.window ~title:"screenshot" () in
+ let width = 500 in
+ let height = 2000 in
+ let m = GMathView.math_view
+ ~font_size:(MatitaMisc.get_current_font_size ()) ~width ~height
+ ~packing:w#add
+ ~show:true ()
+ in
+ w#show ();
+ let filenames =
+ HExtlib.list_mapi
+ (fun (mno,_ as sequent) i ->
+ let mathml =
+ ApplyTransformation.nmml_of_cic_sequent
+ status metasenv subst sequent
+ in
+ m#load_root ~root:mathml#get_documentElement;
+ let pixmap = m#get_buffer in
+ let pixbuf = GdkPixbuf.create ~width ~height () in
+ GdkPixbuf.get_from_drawable ~dest:pixbuf pixmap;
+ let filename =
+ filename ^ "-raw" ^ string_of_int i ^ ".png"
+ in
+ GdkPixbuf.save ~filename ~typ:"png" pixbuf;
+ filename,mno)
+ sequents
+ in
+ let items =
+ List.map (fun (x,mno) ->
+ ignore(Sys.command
+ (Printf.sprintf
+ ("convert "^^
+ " '(' -gravity west -bordercolor grey -border 1 label:%d ')' "^^
+ " '(' -trim -bordercolor white -border 5 "^^
+ " -bordercolor grey -border 1 %s ')' -append %s ")
+ mno
+ (Filename.quote x)
+ (Filename.quote (x ^ ".label.png"))));
+ x ^ ".label.png")
+ filenames
+ in
+ let rec div2 = function
+ | [] -> []
+ | [x] -> [[x]]
+ | x::y::tl -> [x;y] :: div2 tl
+ in
+ let items = div2 items in
+ ignore(Sys.command (Printf.sprintf
+ "convert %s -append %s"
+ (String.concat ""
+ (List.map (fun items ->
+ Printf.sprintf " '(' %s +append ')' "
+ (String.concat
+ (" '(' -gravity center -size 10x10 xc: ')' ") items)) items))
+ (Filename.quote (ofn ^ ".png"))));
+ List.iter (fun x,_ -> Sys.remove x) filenames;
+ List.iter Sys.remove (List.flatten items);
+ w#destroy ()*)
projects / helm.git / blobdiff