in
lazy
(let mmlwidget =
- GMathView.math_view
+ GMathViewAux.single_selection_math_view
~packing:scrolled_window#add ~width:400 ~height:280 () in
let expr =
let term =
in
try
let mml = !mml_of_cic_term_ref 111 expr in
- mmlwidget#load_tree ~dom:mml
+ mmlwidget#load_doc ~dom:mml
with
e ->
output_html outputhtml
exception RefreshSequentException of exn;;
exception RefreshProofException of exn;;
-let refresh_proof (output : GMathView.math_view) =
+let refresh_proof (output : GMathViewAux.single_selection_math_view) =
try
let uri,currentproof =
match !ProofEngine.proof with
mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts
ids_to_inner_types
in
- output#load_tree mml ;
+ output#load_doc ~dom:mml ;
current_cic_infos :=
Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
with
applyStylesheets sequent_doc sequent_styles sequent_args
in
notebook#set_current_page ~may_skip_switch_page_event:true metano;
- notebook#proofw#load_tree ~dom:sequent_mml
+ notebook#proofw#load_doc ~dom:sequent_mml
end ;
current_goal_infos :=
Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
ids_to_inner_types
in
- ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
+ ((rendering_window ())#output : GMathViewAux.single_selection_math_view)#load_doc mml ;
!qed_set_sensitive false ;
(* let's save the theorem and register it to the getter *)
let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
let load () =
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let output = ((rendering_window ())#output : GMathView.math_view) in
+ let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let notebook = (rendering_window ())#notebook in
try
match
let scrolled_window =
GBin.scrolled_window ~border_width:10 ~packing:window#add () in
let mmlwidget =
- GMathView.math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
+ GMathViewAux.single_selection_math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
let href = Gdome.domString "href" in
let show_in_show_window_obj uri obj =
in
window#set_title (UriManager.string_of_uri uri) ;
window#misc#hide () ; window#show () ;
- mmlwidget#load_tree mml ;
+ mmlwidget#load_doc mml ;
with
e ->
output_html outputhtml
let obj = CicEnvironment.get_obj uri in
show_in_show_window_obj uri obj
in
- let show_in_show_window_callback mmlwidget (n : Gdome.element) =
+ let show_in_show_window_callback mmlwidget (n : Gdome.element) _ =
if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
let uri =
(n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
in
show_in_show_window_uri (UriManager.uri_of_string uri)
else
+ prerr_endline
+ "'get_action' and 'action_toggle' not yet implemented in lablgtkmathview 0.3.99"
+(* TODO commented out because not yet implemented in lablgtkmathview 0.3.99 *)
+(*
if mmlwidget#get_action <> None then
mmlwidget#action_toggle
+*)
in
let _ =
- mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget)
+ mmlwidget#connect#click (show_in_show_window_callback mmlwidget)
in
show_in_show_window_obj, show_in_show_window_uri,
show_in_show_window_callback
let new_inductive () =
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let output = ((rendering_window ())#output : GMathView.math_view) in
+ let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let notebook = (rendering_window ())#notebook in
let chosen = ref false in
let new_proof () =
let inputt = ((rendering_window ())#inputt : term_editor) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let output = ((rendering_window ())#output : GMathView.math_view) in
+ let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let notebook = (rendering_window ())#notebook in
let chosen = ref false in
let ty = CicTypeChecker.type_of_aux' metasenv context expr in
let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
scratch_window#show () ;
- scratch_window#mmlwidget#load_tree ~dom:mml
+ scratch_window#mmlwidget#load_doc ~dom:mml
with
e ->
print_endline ("? " ^ CicPp.ppterm expr) ;
let call_tactic tactic () =
let notebook = (rendering_window ())#notebook in
- let output = ((rendering_window ())#output : GMathView.math_view) in
+ let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let savedproof = !ProofEngine.proof in
let savedgoal = !ProofEngine.goal in
let call_tactic_with_input tactic () =
let notebook = (rendering_window ())#notebook in
- let output = ((rendering_window ())#output : GMathView.math_view) in
+ let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let inputt = ((rendering_window ())#inputt : term_editor) in
let savedproof = !ProofEngine.proof in
let module L = LogicalOperations in
let module G = Gdome in
let notebook = (rendering_window ())#notebook in
- let output = ((rendering_window ())#output : GMathView.math_view) in
+ let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let savedproof = !ProofEngine.proof in
let savedgoal = !ProofEngine.goal in
let module L = LogicalOperations in
let module G = Gdome in
let notebook = (rendering_window ())#notebook in
- let output = ((rendering_window ())#output : GMathView.math_view) in
+ let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let inputt = ((rendering_window ())#inputt : term_editor) in
let savedproof = !ProofEngine.proof in
let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
let module L = LogicalOperations in
let module G = Gdome in
- let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
+ let mmlwidget = (scratch_window#mmlwidget : GMathViewAux.single_selection_math_view) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let savedproof = !ProofEngine.proof in
let savedgoal = !ProofEngine.goal in
let expr = tactic term (Hashtbl.find ids_to_terms id) in
let mml = mml_of_cic_term 111 expr in
scratch_window#show () ;
- scratch_window#mmlwidget#load_tree ~dom:mml
+ scratch_window#mmlwidget#load_doc ~dom:mml
| None -> assert false (* "ERROR: No current term!!!" *)
with
e ->
let module L = LogicalOperations in
let module G = Gdome in
let notebook = (rendering_window ())#notebook in
- let output = ((rendering_window ())#output : GMathView.math_view) in
+ let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
let savedproof = !ProofEngine.proof in
let savedgoal = !ProofEngine.goal in
let open_ () =
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let output = ((rendering_window ())#output : GMathView.math_view) in
+ let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
let notebook = (rendering_window ())#notebook in
try
let uri = input_or_locate_uri ~title:"Open" in
;;
let choose_selection
- (mmlwidget : GMathView.math_view) (element : Gdome.element option)
+ (mmlwidget : GMathViewAux.single_selection_math_view) (element : Gdome.element option)
=
let module G = Gdome in
let rec aux element =
then
mmlwidget#set_selection (Some element)
else
+ try
match element#get_parentNode with
None -> assert false
(*CSC: OCAML DIVERGES!
| Some p -> aux (new G.element_of_node p)
*)
| Some p -> aux (new Gdome.element_of_node p)
+ with
+ GdomeInit.DOMCastException _ ->
+ Printf.printf "******* trying to select above the document root ********\n" ; flush stdout
+
in
match element with
Some x -> aux x
(* Stuff for the widget settings *)
-let export_to_postscript (output : GMathView.math_view) =
+let export_to_postscript (output : GMathViewAux.single_selection_math_view) =
let lastdir = ref (Unix.getcwd ()) in
function () ->
match
output#export_to_postscript ~filename:filename ();
;;
-let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
- button_set_kerning button_set_transparency export_to_postscript_menu_item
+let activate_t1 (output : GMathViewAux.single_selection_math_view) button_set_anti_aliasing
+ button_set_transparency export_to_postscript_menu_item
button_t1 ()
=
let is_set = button_t1#active in
if is_set then
begin
button_set_anti_aliasing#misc#set_sensitive true ;
- button_set_kerning#misc#set_sensitive true ;
button_set_transparency#misc#set_sensitive true ;
export_to_postscript_menu_item#misc#set_sensitive true ;
end
else
begin
button_set_anti_aliasing#misc#set_sensitive false ;
- button_set_kerning#misc#set_sensitive false ;
button_set_transparency#misc#set_sensitive false ;
export_to_postscript_menu_item#misc#set_sensitive false ;
end
output#set_anti_aliasing button_set_anti_aliasing#active
;;
-let set_kerning output button_set_kerning () =
- output#set_kerning button_set_kerning#active
-;;
-
let set_transparency output button_set_transparency () =
output#set_transparency button_set_transparency#active
;;
output#set_log_verbosity log_verbosity_spinb#value_as_int
;;
-class settings_window (output : GMathView.math_view) sw
+class settings_window (output : GMathViewAux.single_selection_math_view) sw
export_to_postscript_menu_item selection_changed_callback
=
let settings_window = GWindow.window ~title:"GtkMathView settings" () in
let button_set_anti_aliasing =
GButton.toggle_button ~label:"set_anti_aliasing"
~packing:(table#attach ~left:0 ~top:1) () in
- let button_set_kerning =
- GButton.toggle_button ~label:"set_kerning"
- ~packing:(table#attach ~left:1 ~top:1) () in
let button_set_transparency =
GButton.toggle_button ~label:"set_transparency"
~packing:(table#attach ~left:2 ~top:1) () in
method show = settings_window#show
initializer
button_set_anti_aliasing#misc#set_sensitive false ;
- button_set_kerning#misc#set_sensitive false ;
button_set_transparency#misc#set_sensitive false ;
(* Signals connection *)
ignore(button_t1#connect#clicked
- (activate_t1 output button_set_anti_aliasing button_set_kerning
+ (activate_t1 output button_set_anti_aliasing
button_set_transparency export_to_postscript_menu_item 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(button_set_transparency#connect#toggled
(set_transparency output button_set_transparency)) ;
ignore(log_verbosity_spinb#connect#changed
GBin.scrolled_window ~border_width:10
~packing:(vbox#pack ~expand:true ~padding:5) () in
let mmlwidget =
- GMathView.math_view
+ GMathViewAux.single_selection_math_view
~packing:(scrolled_window#add) ~width:400 ~height:280 () in
object(self)
method mmlwidget = mmlwidget
GBin.scrolled_window ~border_width:10
~packing:(vbox1#pack ~expand:true ~padding:5) () in
let proofw =
- GMathView.math_view ~width:400 ~height:275
+ GMathViewAux.single_selection_math_view ~width:400 ~height:275
~packing:(scrolled_window1#add) () in
let _ = proofw_ref <- Some proofw in
let hbox3 =
GBin.scrolled_window ~border_width:10
~packing:(vbox1#pack ~expand:true ~padding:5) () in
let proofw =
- GMathView.math_view ~width:400 ~height:275
+ GMathViewAux.single_selection_math_view ~width:400 ~height:275
~packing:(scrolled_window1#add) () in
object(self)
- method proofw = (assert false : GMathView.math_view)
+ method proofw = (assert false : GMathViewAux.single_selection_math_view)
method content = vbox1
method compute = (assert false : unit)
end
object
method outputhtml = outputhtml
method inputt = inputt
- method output = (output : GMathView.math_view)
+ method output = (output : GMathViewAux.single_selection_math_view)
method notebook = notebook
method show = window#show
initializer
choose_selection output elem ;
!focus_and_proveit_set_sensitive true
)) ;
- ignore (output#connect#clicked (show_in_show_window_callback output)) ;
+ ignore (output#connect#click (show_in_show_window_callback output)) ;
let settings_window = new settings_window output scrolled_window0
export_to_postscript_menu_item (choose_selection output) in
set_settings_window settings_window ;
let initialize_everything () =
let module U = Unix in
- let output = GMathView.math_view ~width:350 ~height:280 () in
+ let output = GMathViewAux.single_selection_math_view ~width:350 ~height:280 () in
let notebook = new notebook in
let rendering_window' = new rendering_window output notebook in
set_rendering_window rendering_window' ;
projects / helm.git / commitdiff