X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FcicMathView.ml;h=ec42ee8df543f0fd7db44d8372a96874cbc244e0;hb=f8b4eb67c2437f7b5174d7dca46e102e0ac0d19d;hp=60d3b69cfab196d77c4057f989332e1dd2806350;hpb=ad3546bfc633935891d8c69ea704c86207c83f57;p=helm.git diff --git a/matita/matita/cicMathView.ml b/matita/matita/cicMathView.ml index 60d3b69cf..ec42ee8df 100644 --- a/matita/matita/cicMathView.ml +++ b/matita/matita/cicMathView.ml @@ -25,26 +25,23 @@ 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 @@ -68,10 +65,10 @@ let xref_ds = Gdome.domString "xref" (** 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) = @@ -175,39 +172,89 @@ let string_of_dom_node node = *) 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 + (* *) + 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 @@ -222,7 +269,6 @@ object (self) 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); @@ -371,7 +417,7 @@ object (self) (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); @@ -447,8 +493,6 @@ object (self) | 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 @@ -506,7 +550,7 @@ object (self) 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 = @@ -566,8 +610,6 @@ IDIOTA: PRIMA SI FA LA LOCATE, POI LA PATTERN_OF. MEGLIO UN'UNICA pattern_of CHE | [] -> 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 @@ -601,7 +643,7 @@ object (self) 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 = @@ -626,7 +668,7 @@ object (self) 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); @@ -645,3 +687,64 @@ let cicMathView (*?auto_indent ?highlight_current_line ?indent_on_tab ?indent_wi 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 ()*)