Experimental commit: definitions are now allowed in contexts. As a consequence,

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 905de741041dc586772fbac7fa5f6c5224a53031..47c416d8b60b9ad472098d883f4cacf2f2026345 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
 ;;
@@ -582,7 +582,10 @@ let save rendering_window () =
  match !ProofEngine.proof with
     None -> assert false
   | Some (uri,[],bo,ty) ->
-     if CicReduction.are_convertible (CicTypeChecker.type_of_aux' [] [] bo) ty then
+     if
+      CicReduction.are_convertible []
+       (CicTypeChecker.type_of_aux' [] [] bo) ty
+     then
       begin
        (*CSC: Wrong: [] is just plainly wrong *)
        let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
@@ -780,6 +783,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 +1033,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 +1114,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)) ;