From ba53effd71fdfdc046dc39ea9dd7f07cf823a1b6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 19 Dec 2010 19:52:37 +0000 Subject: [PATCH] 1. Method screenshot moved to CicMathView where it belongs to. 2. the mutual dependency between MatitaScript and CicMathView/MatitaMathView needs to be solved differently (it used to be solved using guistuff, which I do not consider any longer a good solution). To be done. With this commit, anything related to MathML vs Textual is now in cicMathView.ml. --- matita/matita/.depend | 4 +- matita/matita/.depend.opt | 4 +- matita/matita/Makefile | 2 +- matita/matita/cicMathView.ml | 68 ++++++++++++++++++++++++++++++++- matita/matita/cicMathView.mli | 6 +++ matita/matita/matitaMathView.ml | 61 ----------------------------- matita/matita/matitaScript.ml | 2 +- matita/matita/matitaTypes.ml | 3 -- matita/matita/matitaTypes.mli | 3 -- 9 files changed, 78 insertions(+), 75 deletions(-) diff --git a/matita/matita/.depend b/matita/matita/.depend index ee1e8e14b..d7b9a80a1 100644 --- a/matita/matita/.depend +++ b/matita/matita/.depend @@ -47,9 +47,9 @@ matita.cmx: predefined_virtuals.cmx matitaTypes.cmx matitaScript.cmx \ matitaMathView.cmx matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx \ buildTimeConf.cmx matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaGtkMisc.cmi \ - matitaEngine.cmi buildTimeConf.cmo matitaScript.cmi + matitaEngine.cmi cicMathView.cmi buildTimeConf.cmo matitaScript.cmi matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaGtkMisc.cmx \ - matitaEngine.cmx buildTimeConf.cmx matitaScript.cmi + matitaEngine.cmx cicMathView.cmx buildTimeConf.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi diff --git a/matita/matita/.depend.opt b/matita/matita/.depend.opt index 5b87b1e69..42bbf72a0 100644 --- a/matita/matita/.depend.opt +++ b/matita/matita/.depend.opt @@ -47,9 +47,9 @@ matita.cmx: predefined_virtuals.cmx matitaTypes.cmx matitaScript.cmx \ matitaMathView.cmx matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx \ buildTimeConf.cmx matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaGtkMisc.cmi \ - matitaEngine.cmi buildTimeConf.cmx matitaScript.cmi + matitaEngine.cmi cicMathView.cmi buildTimeConf.cmx matitaScript.cmi matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaGtkMisc.cmx \ - matitaEngine.cmx buildTimeConf.cmx matitaScript.cmi + matitaEngine.cmx cicMathView.cmx buildTimeConf.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi diff --git a/matita/matita/Makefile b/matita/matita/Makefile index 06dde1085..2d1fae4bf 100644 --- a/matita/matita/Makefile +++ b/matita/matita/Makefile @@ -43,9 +43,9 @@ MLI = \ matitaInit.mli \ matitaGtkMisc.mli \ virtuals.mli \ + cicMathView.mli \ matitaScript.mli \ predefined_virtuals.mli \ - cicMathView.mli \ matitaMathView.mli \ matitaGui.mli \ $(NULL) diff --git a/matita/matita/cicMathView.ml b/matita/matita/cicMathView.ml index 43cedcec6..f7e5b667a 100644 --- a/matita/matita/cicMathView.ml +++ b/matita/matita/cicMathView.ml @@ -30,6 +30,9 @@ open MatitaGtkMisc open MatitaGuiTypes open GtkSourceView2 +let matita_script_current = ref (fun _ -> assert false);; +let register_matita_script_current f = matita_script_current := f;; + type document_element = string class type cicMathView = @@ -368,7 +371,7 @@ object (self) (GrafiteAst.Tactic (loc, Some (GrafiteAst.Reduce (loc, kind, pat)), GrafiteAst.Semicolon loc)) in - (MatitaScript.current ())#advance ~statement () in + (!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); @@ -503,7 +506,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 = !matita_script_current () in let metasenv = if script#onGoingProof () then script#proofMetasenv else [] in let map_unicode_to_tex = @@ -640,3 +643,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 ()*) diff --git a/matita/matita/cicMathView.mli b/matita/matita/cicMathView.mli index 260452bd5..80e6bc886 100644 --- a/matita/matita/cicMathView.mli +++ b/matita/matita/cicMathView.mli @@ -59,3 +59,9 @@ val cicMathView : val empty_mathml: document_element Lazy.t val closed_goal_mathml: document_element Lazy.t + +val screenshot: + GrafiteTypes.status -> NCic.metasenv -> NCic.metasenv -> + NCic.substitution -> string -> unit + +val register_matita_script_current: (unit -> < advance: unit; onGoingProf: bool; metasenv: NCic.metasenv >) -> unit diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 1b8d608c2..4b5a9fc1d 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -702,67 +702,6 @@ let mathViewer () = method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t - method 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 (); - *) end let refresh_all_browsers () = diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index b84180037..c50b4b571 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -112,7 +112,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us let selected = Continuationals.Stack.head_goals status#stack in List.filter (fun x,_ -> List.mem x selected) menv in - guistuff.mathviewer#screenshot status sequents menv subst name; + CicMathView.screenshot status sequents menv subst name; [status, parsed_text], "", parsed_text_length | TA.NCheck (_,t) -> let status = script#grafite_status in diff --git a/matita/matita/matitaTypes.ml b/matita/matita/matitaTypes.ml index e5b80d0e8..6ead6da47 100644 --- a/matita/matita/matitaTypes.ml +++ b/matita/matita/matitaTypes.ml @@ -82,7 +82,4 @@ class type mathViewer = * opens a new one. default is false *) method show_entry: ?reuse:bool -> mathViewer_entry -> unit - method screenshot: - GrafiteTypes.status -> NCic.metasenv -> NCic.metasenv -> - NCic.substitution -> string -> unit end diff --git a/matita/matita/matitaTypes.mli b/matita/matita/matitaTypes.mli index c1d19ee7e..651294e96 100644 --- a/matita/matita/matitaTypes.mli +++ b/matita/matita/matitaTypes.mli @@ -42,7 +42,4 @@ val entry_of_string : string -> mathViewer_entry class type mathViewer = object method show_entry : ?reuse:bool -> mathViewer_entry -> unit - method screenshot: - GrafiteTypes.status -> NCic.metasenv -> NCic.metasenv -> - NCic.substitution -> string -> unit end -- 2.39.2