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
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
matitaInit.mli \
matitaGtkMisc.mli \
virtuals.mli \
+ cicMathView.mli \
matitaScript.mli \
predefined_virtuals.mli \
- cicMathView.mli \
matitaMathView.mli \
matitaGui.mli \
$(NULL)
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 =
(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);
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 =
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 ()*)
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
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 () =
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
* 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
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
projects / helm.git / commitdiff