basic MathQL support

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 905de741041dc586772fbac7fa5f6c5224a53031..49510a9dde1dc7f9a2480df7d7a7afc11caf686f 100644 (file)
--- 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 () =
         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
+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
+      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+
+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)) ;