X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2FgTopLevel.ml;h=49510a9dde1dc7f9a2480df7d7a7afc11caf686f;hb=185fc93ada03ee7e736c90adf165a4f396fb2eba;hp=905de741041dc586772fbac7fa5f6c5224a53031;hpb=7b7d26322d3bd9be8d6cdde79c74ff38e921290b;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 905de7410..49510a9dd 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -151,7 +151,7 @@ let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
(*CSC: We save the innertypes to disk so that we can retrieve them in the *)
(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
(*CSC: local. *)
- Xml.pp xmlinnertypes (Some "/public/sacerdot/innertypes") ;
+ Xml.pp xmlinnertypes (Some "/public/fguidi/innertypes") ;
let output = applyStylesheets input mml_styles mml_args in
output
;;
@@ -780,6 +780,29 @@ let check rendering_window scratch_window () =
("
" ^ Printexc.to_string e ^ "
") ;
;;
+let locate rendering_window () =
+ let inputt = (rendering_window#inputt : GEdit.text) in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen in
+ try
+ output_html outputhtml (Mquery.locate input) ;
+ inputt#delete_text 0 inputlen
+ with
+ e ->
+ output_html outputhtml
+ ("" ^ Printexc.to_string e ^ "
")
+;;
+
+let backward rendering_window () =
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let result =
+ match !ProofEngine.goal with
+ | None -> ""
+ | Some (_, (_, t)) -> (Mquery.backward t)
+ in
+ output_html outputhtml result
+
let choose_selection
(mmlwidget : GMathView.math_view) (element : Gdome.element option)
=
@@ -1007,6 +1030,12 @@ class rendering_window output proofw (label : GMisc.label) =
let checkb =
GButton.button ~label:"Check"
~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let locateb =
+ GButton.button ~label:"Locate"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let backwardb =
+ GButton.button ~label:"Backward"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
~packing:(vbox#pack ~padding:5) () in
let vbox1 =
@@ -1082,6 +1111,8 @@ object(self)
ignore(stateb#connect#clicked (state self)) ;
ignore(openb#connect#clicked (open_ self)) ;
ignore(checkb#connect#clicked (check self scratch_window)) ;
+ ignore(locateb#connect#clicked (locate self)) ;
+ ignore(backwardb#connect#clicked (backward self)) ;
ignore(exactb#connect#clicked (exact self)) ;
ignore(applyb#connect#clicked (apply self)) ;
ignore(elimintrosb#connect#clicked (elimintros self)) ;