let uritree = ref []
let theoryuritree = ref []
+(* Brutti, per via del widget che non e' imperativo *)
+let loaded_uri = ref "";;
+let theory_loaded_uri = ref "";;
+
let get_name =
function
Dir (name,_) -> name
rendering_window#label#set_text (UriManager.string_of_uri uri) ;
ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ;
let mmlfile = XsltProcessor.process uri true "theory" in
- rendering_window#output#load mmlfile
+ theory_loaded_uri := mmlfile ;
+ !(rendering_window#output)#load mmlfile
;;
let update_output rendering_window uri =
rendering_window#label#set_text (UriManager.string_of_uri uri) ;
ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ;
let mmlfile = XsltProcessor.process uri true "cic" in
- rendering_window#output#load mmlfile
+ loaded_uri := mmlfile ;
+ !(rendering_window#output)#load mmlfile
;;
let theory_next rendering_window () =
let choose_selection rendering_window node =
let module M = Minidom in
- let rec aux ~first_time node =
+ let rec aux node =
match M.node_get_attribute node (M.mDOMString_of_string "xref") with
None ->
let parent =
None -> assert false
| Some parent -> parent
in
- aux ~first_time:false parent
- | Some s ->
- if not first_time then
- rendering_window#output#set_selection (Some node)
+ aux parent
+ | Some s -> !(rendering_window#output)#set_selection (Some node)
in
match node with
- None -> () (* No element selected *)
- | Some node -> aux ~first_time:true node
-;;
-
-let changefont rendering_window () =
- rendering_window#output#set_font_size rendering_window#spinb#value_as_int
+ None -> !(rendering_window#output)#set_selection None
+ | Some node -> aux node
;;
let annotateb_pressed rendering_window annotation_window () =
let module M = Minidom in
- match rendering_window#output#get_selection with
+ match !(rendering_window#output)#get_selection with
None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
| Some node ->
let xpath =
aux
;;
+(* Stuff for the widget settings *)
+
+let export_to_postscript output () =
+ !output#export_to_postscript "output.ps" ;
+;;
+
+let activate_t1 output sw is_set jump_callback selection_changed_callback
+ last_uri ()
+=
+ is_set := not !is_set ;
+ sw#remove !output#coerce ;
+ output :=
+ (GMathView.math_view ~packing:sw#add ~width:400 ~height:380
+ ~use_t1_lib:!is_set ()) ;
+ !output#load !last_uri ;
+ ignore(!output#connect#jump jump_callback) ;
+ ignore(!output#connect#selection_changed selection_changed_callback) ;
+;;
+
+let set_anti_aliasing output is_set () =
+ is_set := not !is_set ;
+ !output#set_anti_aliasing !is_set
+;;
+
+let set_kerning output is_set () =
+ is_set := not !is_set ;
+ !output#set_kerning !is_set
+;;
+
+let changefont output font_size_spinb () =
+ !output#set_font_size font_size_spinb#value_as_int
+;;
+
+let set_log_verbosity output log_verbosity_spinb () =
+ !output#set_log_verbosity log_verbosity_spinb#value_as_int
+;;
+
+class settings_window output sw jump_callback selection_changed_callback
+ last_uri
+=
+ let settings_window = GWindow.window ~title:"GtkMathView settings" () in
+ let table = GPack.table ~rows:5 ~columns:5 ~packing:settings_window#add () in
+ let button_t1 =
+ GButton.toggle_button ~label:"activate t1 fonts"
+ ~packing:(table#attach ~left:0 ~top:0) () in
+ let font_size_spinb =
+ let sadj =
+ GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
+ in
+ GEdit.spin_button
+ ~adjustment:sadj ~packing:(table#attach ~left:4 ~top:2) () in
+ let button_set_anti_aliasing = GButton.toggle_button ~label:"set_anti_aliasing" ~packing:(table#attach ~left:1 ~top:3) () in
+ let button_set_kerning =
+ GButton.toggle_button ~label:"set_kerning"
+ ~packing:(table#attach ~left:3 ~top:3) () in
+ let log_verbosity_spinb =
+ let sadj =
+ GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
+ in
+ GEdit.spin_button
+ ~adjustment:sadj ~packing:(table#attach ~left:2 ~top:2) () in
+object(self)
+ method show = settings_window#show
+ initializer
+ (* Signals connection *)
+ let is_set_use_t1_lib = ref false in
+ ignore(button_t1#connect#clicked
+ (activate_t1 output sw is_set_use_t1_lib jump_callback
+ selection_changed_callback last_uri)) ;
+ ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
+ let is_set_anti_aliasing = ref false in
+ ignore(button_set_anti_aliasing#connect#toggled
+ (set_anti_aliasing output is_set_anti_aliasing));
+ let is_set_kerning = ref false in
+ ignore(button_set_kerning#connect#toggled
+ (set_kerning output is_set_kerning)) ;
+ ignore(log_verbosity_spinb#connect#changed
+ (set_log_verbosity output log_verbosity_spinb))
+end;;
+
+(* Main windows *)
+
class annotation_window output label =
let window_to_annotate =
GWindow.window ~title:"Annotating environment" ~border_width:2 () in
method radio_some = radio_some
method radio_none = radio_none
method annotation_hints = annotation_hints
- method output = (output : GMathView.math_view)
+ method output = (output : GMathView.math_view ref)
method show () = window_to_annotate#show ()
initializer
(* signal handlers here *)
in
visited_uris := new_current_uri::(List.tl !visited_uris) ;
label#set_text (UriManager.string_of_uri new_current_uri) ;
- output#load (parse_no_cache new_current_uri)
+ let mmlfile = parse_no_cache new_current_uri in
+ loaded_uri := mmlfile ;
+ !output#load mmlfile
)) ;
ignore (abortb#connect#clicked
(fun () ->
GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in
let scrolled_window0 =
GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
- let _ = scrolled_window0#add output#coerce in
+ let _ = scrolled_window0#add !output#coerce in
let scrolled_window =
GBin.scrolled_window
~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
let annotateb =
GButton.button ~label:"Annotate"
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let spinb =
- let sadj =
- GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
- in
- GEdit.spin_button
- ~adjustment:sadj ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5)
- () in
+ let settingsb =
+ GButton.button ~label:"Settings"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let button_export_to_postscript =
+ GButton.button ~label:"export_to_postscript"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
let closeb =
GButton.button ~label:"Close"
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
method nextb = nextb
method prevb = prevb
method label = label
- method spinb = spinb
- method output = (output : GMathView.math_view)
+ method output = (output : GMathView.math_view ref)
method errors = errors
method show () = window#show ()
initializer
prevb#misc#set_sensitive false ;
(* signal handlers here *)
- ignore(output#connect#jump (jump self)) ;
- ignore(output#connect#selection_changed (choose_selection self)) ;
+ ignore(!output#connect#jump (jump self)) ;
+ ignore(!output#connect#selection_changed (choose_selection self)) ;
ignore(nextb#connect#clicked (next self)) ;
ignore(prevb#connect#clicked (prev self)) ;
ignore(checkb#connect#clicked (check self)) ;
- ignore(spinb#connect#changed (changefont self)) ;
ignore(closeb#connect#clicked window#misc#hide) ;
ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ;
+ let settings_window = new settings_window output scrolled_window0
+ (jump self) (choose_selection self) loaded_uri in
+ ignore(settingsb#connect#clicked settings_window#show) ;
+ ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
end;;
let scrolled_window0 =
GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
let output =
- GMathView.math_view ~width:400 ~height:380 ~packing:scrolled_window0#add () in
+ ref (GMathView.math_view ~use_t1_lib:false ~width:400 ~height:380
+ ~packing:scrolled_window0#add ()) in
let scrolled_window =
GBin.scrolled_window
~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in
let checkb =
GButton.button ~label:"Check"
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let spinb =
- let sadj =
- GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
- in
- GEdit.spin_button
- ~adjustment:sadj ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5)
- () in
+ let settingsb =
+ GButton.button ~label:"Settings"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let button_export_to_postscript =
+ GButton.button ~label:"export_to_postscript"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
let closeb =
GButton.button ~label:"Close"
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
method nextb = nextb
method prevb = prevb
method label = label
- method output = (output : GMathView.math_view)
+ method output = (output : GMathView.math_view ref)
method errors = errors
- method spinb = spinb
method show () = window#show ()
initializer
nextb#misc#set_sensitive false ;
prevb#misc#set_sensitive false ;
(* signal handlers here *)
- ignore(output#connect#jump (jump rendering_window)) ;
- ignore(output#connect#selection_changed (choose_selection self)) ;
+ ignore(!output#connect#jump (jump rendering_window)) ;
+ ignore(!output#connect#selection_changed (choose_selection self)) ;
ignore(nextb#connect#clicked (theory_next self)) ;
ignore(prevb#connect#clicked (theory_prev self)) ;
ignore(checkb#connect#clicked (theory_check self)) ;
- ignore(spinb#connect#changed (changefont self)) ;
+ let settings_window = new settings_window output scrolled_window0
+ (jump rendering_window) (choose_selection self) theory_loaded_uri in
+ ignore(settingsb#connect#clicked settings_window#show) ;
+ ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
ignore(closeb#connect#clicked window#misc#hide) ;
ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
end;;
let _ =
build_uri_tree () ;
- let output = GMathView.math_view ~width:400 ~height:380 ()
+ let output =
+ ref (GMathView.math_view ~use_t1_lib:false ~width:400 ~height:380 ())
and label = GMisc.label ~text:"???" () in
let annotation_window = new annotation_window output label in
let rendering_window = new rendering_window annotation_window output label in
projects / helm.git / blobdiff