exception NoCurrentUri;;
exception NoNextOrPrevUri;;
-exception GtkInterfaceInternalError;;
let theory_get_current_uri () =
match !theory_visited_uris with
;;
(* called when an hyperlink is clicked *)
-let jump rendering_window s =
- let uri = UriManager.uri_of_string s in
- rendering_window#show () ;
- rendering_window#prevb#misc#set_sensitive true ;
- rendering_window#nextb#misc#set_sensitive false ;
- visited_uris := uri::!visited_uris ;
- to_visit_uris := [] ;
- annotated_obj := None ;
- update_output rendering_window uri
+let jump rendering_window (node : Ominidom.o_mDOMNode) =
+ let module O = Ominidom in
+ match (node#get_attribute (O.o_mDOMString_of_string "href")) with
+ Some str ->
+ let s = str#get_string in
+ let uri = UriManager.uri_of_string s in
+ rendering_window#show () ;
+ rendering_window#prevb#misc#set_sensitive true ;
+ rendering_window#nextb#misc#set_sensitive false ;
+ visited_uris := uri::!visited_uris ;
+ to_visit_uris := [] ;
+ annotated_obj := None ;
+ update_output rendering_window uri
+ | None -> assert false
;;
-let changefont rendering_window () =
- rendering_window#output#set_font_size rendering_window#spinb#value_as_int
+let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) =
+ let module O = Ominidom in
+ let rec aux node =
+ match node#get_attribute (O.o_mDOMString_of_string "xref") with
+ Some _ -> rendering_window#output#set_selection (Some node)
+ | None -> aux (node#get_parent)
+ in
+ match node with
+ Some x -> aux x
+ | None -> rendering_window#output#set_selection None
;;
;;
let annotateb_pressed rendering_window annotation_window () =
- let xpath = (rendering_window#output#get_selection : string option) in
- match xpath with
- None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
+ let module O = Ominidom in
+ match rendering_window#output#get_selection with
+ | Some node ->
+ begin
+ match (node#get_attribute (O.o_mDOMString_of_string "xref")) with
| Some xpath ->
- try
let annobj = get_annotated_obj ()
(* next "cast" can't got rid of, but I don't know why *)
and annotation = (annotation_window#annotation : GEdit.text) in
- ann := CicXPath.get_annotation annobj xpath ;
- CicAnnotationHinter.create_hints annotation_window annobj xpath ;
+ ann := CicXPath.get_annotation annobj (xpath#get_string) ;
+ CicAnnotationHinter.create_hints annotation_window annobj (xpath#get_string) ;
annotation#delete_text 0 annotation#length ;
begin
match !(!ann) with
end ;
GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
annotation_window#show () ;
- with
- e ->
+ | None ->
(* next "cast" can't got rid of, but I don't know why *)
let errors = (rendering_window#errors : GEdit.text) in
- errors#insert ("\n" ^ Printexc.to_string e ^ "\n")
+ errors#insert ("\nNo xref found\n")
+ end
+ | None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
;;
(* called when the annotation is confirmed *)
else
!ann := None ;
match !annotated_obj with
- None -> raise GtkInterfaceInternalError
+ None -> assert false
| Some (annobj,_) ->
let uri = get_current_uri () in
let annxml = Annotation2Xml.pp_annotation annobj uri in
ignore(treeitem2#connect#select
(selection_changed rendering_window uri)) ;
aux treeitem2 ti
- ) !content
+ ) (List.sort compare !content)
| _ -> ()
in
aux
;;
+(* Stuff for the widget settings *)
+
+let export_to_postscript (output : GMathView.math_view) () =
+ output#export_to_postscript ~filename:"output.ps" ();
+;;
+
+let activate_t1 output button_set_anti_aliasing button_set_kerning
+ button_export_to_postscript button_t1 ()
+=
+ let is_set = button_t1#active in
+ output#set_font_manager_type
+ (if is_set then `font_manager_t1 else `font_manager_gtk) ;
+ if is_set then
+ begin
+ button_set_anti_aliasing#misc#set_sensitive true ;
+ button_set_kerning#misc#set_sensitive true ;
+ button_export_to_postscript#misc#set_sensitive true ;
+ end
+ else
+ begin
+ button_set_anti_aliasing#misc#set_sensitive false ;
+ button_set_kerning#misc#set_sensitive false ;
+ button_export_to_postscript#misc#set_sensitive false ;
+ end
+;;
+
+let set_anti_aliasing output button_set_anti_aliasing () =
+ output#set_anti_aliasing button_set_anti_aliasing#active
+;;
+
+let set_kerning output button_set_kerning () =
+ output#set_kerning button_set_kerning#active
+;;
+
+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 button_export_to_postscript jump_callback
+ selection_changed_callback
+=
+ let settings_window = GWindow.window ~title:"GtkMathView settings" () in
+ let vbox =
+ GPack.vbox ~packing:settings_window#add () in
+ let table =
+ GPack.table
+ ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
+ ~border_width:5 ~packing:vbox#add () in
+ let button_t1 =
+ GButton.toggle_button ~label:"activate t1 fonts"
+ ~packing:(table#attach ~left:0 ~top:0) () in
+ let button_set_anti_aliasing =
+ GButton.toggle_button ~label:"set_anti_aliasing"
+ ~packing:(table#attach ~left:1 ~top:0) () in
+ let button_set_kerning =
+ GButton.toggle_button ~label:"set_kerning"
+ ~packing:(table#attach ~left:2 ~top:0) () in
+ let table =
+ GPack.table
+ ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
+ ~border_width:5 ~packing:vbox#add () in
+ let font_size_label =
+ GMisc.label ~text:"font size:"
+ ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () 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:1 ~top:0 ~fill:`NONE) () in
+ let log_verbosity_label =
+ GMisc.label ~text:"log verbosity:"
+ ~packing:(table#attach ~left:0 ~top:1) () 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:1 ~top:1) () in
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let closeb =
+ GButton.button ~label:"Close"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+object(self)
+ method show = settings_window#show
+ initializer
+ button_set_anti_aliasing#misc#set_sensitive false ;
+ button_set_kerning#misc#set_sensitive false ;
+ (* Signals connection *)
+ ignore(button_t1#connect#clicked
+ (activate_t1 output button_set_anti_aliasing button_set_kerning
+ button_export_to_postscript button_t1)) ;
+ ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
+ ignore(button_set_anti_aliasing#connect#toggled
+ (set_anti_aliasing output button_set_anti_aliasing));
+ ignore(button_set_kerning#connect#toggled
+ (set_kerning output button_set_kerning)) ;
+ ignore(log_verbosity_spinb#connect#changed
+ (set_log_verbosity output log_verbosity_spinb)) ;
+ ignore(closeb#connect#clicked settings_window#misc#hide)
+end;;
+
+(* Main windows *)
+
class annotation_window output label =
let window_to_annotate =
GWindow.window ~title:"Annotating environment" ~border_width:2 () in
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
+ output#load mmlfile
)) ;
ignore (abortb#connect#clicked
(fun () ->
GPack.vbox ~packing:window#add () in
let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
let paned =
- GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in
+ GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
let scrolled_window0 =
GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
let _ = scrolled_window0#add output#coerce 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 errors = errors
method show () = window#show ()
initializer
nextb#misc#set_sensitive false ;
prevb#misc#set_sensitive false ;
+ button_export_to_postscript#misc#set_sensitive false ;
(* signal handlers here *)
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
+ button_export_to_postscript (jump self) (choose_selection self) 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;;
GMisc.label ~text:"???"
~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
let paned =
- GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in
+ GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
let scrolled_window0 =
GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
let output =
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 label = label
method output = (output : GMathView.math_view)
method errors = errors
- method spinb = spinb
method show () = window#show ()
initializer
nextb#misc#set_sensitive false ;
prevb#misc#set_sensitive false ;
+ button_export_to_postscript#misc#set_sensitive false ;
(* signal handlers here *)
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
+ button_export_to_postscript (jump rendering_window)(choose_selection self) 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;;
projects / helm.git / blobdiff